Logique propositionnel et modus ponens

[busard_des_roseaux]

et concernant:

((A->A**) ET (A** ->A))

?

[ffpower]

Le probleme c est que on a pas encore défini le ET ici.On a pour l instant que => et neg..donc on peut définir A ET B comme un raccourci de neg(neg A ou neg B).reste a définir le OU,qu on peut définir en disant que A ou B est un raccourci de neg B=>A.Maintenant,on voit que la définition de ET est un peu longue,et donc pour éviter de sortir une preuve de barbare,il vaudrait mieux arriver a montrer la chose suivante:si A et B sont 2 propositions logiques,si on a réussi a obtenir une preuve une preuve de A et une preuve de B,alors on peut obtenir une preuve de A ET B.Le plus simple pour arriver a ceci serait de prouver la proposition A=>(B=>(A ET B)).Si on arrive a montrer ceci,alors il suffira de donner une preuve du theoreme neg neg A=>A(ce que doraki a fait si il n y pas d erreur,je n ai pas eu le courage de vérifier^^) et du theoreme A=>neg neg A(ce qui découle de neg neg A=>A et de SA3 par modus machin truc).Reste donc a prouver A=>(B=>(A ET B)),je vais y réfléchir(enfin pour l instant,je vais surtout aller bosser parce que bon,la,je glande,je glande..)

[ffpower]

Merci pour toute ses réponses mais en faite moi je comprend pas très bien comment choisir quel axiome a appliquer par exemple pour l'exemple pourquoi choisitons SA1 en premier , pourquoi pas SA2 ou SA3?

Pourquoi utilise t on une proposition plutot qu une autre?ben parce que ca marche.on essaie de trouver quels theoremes utiliser et dans quel ordre pour parvenir au résultat désiré.Pour calculer une integrale,pourquoi utiliser une integration par partie plutot qu un changement de variables,ou l inverse?..C est la meme chose ici..

[Doraki]

et du theoreme A=>neg neg A(ce qui découle de neg neg A=>A et de SA3 par modus machin truc).

Ah ouais, on substitue A par A* pour avoir une preuve de A*** -> A*, et ça donne une preuve de A->A**.

Je pense qu'on devrait pouvoir définir
F := (A->A)*
A et B := (A->B->F)->F
A ou B := (A->F)->(B->F)->F
Montrer que A*->A->F et (A->F)->A*
etc...

Et ptetre un lemme de substitution.

Avec tout ça ça ressemblerait un peu plus à un truc supportable...

[busard_des_roseaux]

Ah ouais, on substitue A par A* pour avoir une preuve de A*** -> A*, et ça donne une preuve de A->A**.

Je pense qu'on devrait pouvoir définir
F := (A->A)*
A et B := (A->B->F)->F
A ou B := (A->F)->(B->F)->F
Montrer que A*->A->F et (A->F)->A*
etc...

Et ptetre un lemme de substitution.

Avec tout ça ça ressemblerait un peu plus à un truc supportable...

oui, mais , ça c'est juste de la nomination. Avant d'exécuter, l'interpréteur
remplace le nom par la chaine qu'il désigne. Et évidemment, ça peut boucler
et/ou produire un overflow: A="non A"