Logique propositionnel et modus ponens

[tsoungui]

Bonjour voila j'ai un probleme jai chercher sur internet mais je ne parviens pas a trouver.
Alors par exemple pour cette exercice il faut demontrer que:
(negation negation A -> A )est bien un theoreme .
Les schemas d'axiome sont les suivants :
SA1 (A-> (B -> A))
SA2 (A->(B->C)) -> ((A->B) ->(A -> C)
SA3 ((neg A -> neg B) -> (B -> A))
regle modus ponens A , A-> B : B
J'ai le corigé mais je ne comprend pas pourquoi on choisis telle ou telle axiome .
Par exemple dans mon corrige il commence par faire une hypothese .
F1 (neg neg A) hyp
F2 (neg(neg A)) -> neg neg neg neg -> neg neg A SA1 A = neg neg A B neg neg neg neg A
Voila deja la je suis perdus pourquoi utilisons nous le SA1 et comment deduire les valeur de A et B . Merci . :cry: Je souhaiterais juste savoir si il y a une methode pour demontrer si une formule est un theoreme ?

[busard_des_roseaux]

Bonjour voila j'ai un probleme jai chercher sur internet mais je ne parviens pas a trouver.
Alors par exemple pour cette exercice il faut demontrer que:
(negation negation A -> A )est bien un theoreme .
Les schemas d'axiome sont les suivants :
SA1 (A-> (B -> A))
SA2 (A->(B->C)) -> ((A->B) ->(A -> C)
SA3 ((neg A -> neg B) -> (B -> A))
regle modus ponens A , A-> B : B
J'ai le corigé mais je ne comprend pas pourquoi on choisis telle ou telle axiome .
Par exemple dans mon corrige il commence par faire une hypothese .
F1 (neg neg A) hyp
F2 (neg(neg A)) -> neg neg neg neg -> neg neg A SA1 A = neg neg A B neg neg neg neg A
Voila deja la je suis perdus pourquoi utilisons nous le SA1 et comment deduire les valeur de A et B . Merci . Je souhaiterais juste savoir si il y a une methode pour demontrer si une formule est un theoreme ?

vous utilisez SA1 car SA1 est une tautologie, toujours vraie:
si A est faux , SA1 est vraie
Si A est vrai , B->A est vraie donc SA1 est vraie.
On peut donc toujours utiliser SA1, car elle est toujours vraie.

Pour les autres, pareils.
SA1,SA2,SA3 sont des tautologies, toujours vraies.
On pourrait par exemple les implémenter dans n'importe quelle
machine "pensante". On voit sur quoi est basé le raisonnement :
une collection abondante de tautologies. :zen:

[tsoungui]

Merci mais par exemple si on me demande de démontrer que négation négation A -> A pourquoi on commence par appliquer l axiome SA1 pourquoi pas SA2 ou SA3 on les choisit au hasard ou il y a une regle,et dans l'exemple que j'ai citer je ne comprend pas le negation negation negation negation A . Par exemple pour demontrer que neg neg A -> neg neg A vous utilisez quelque axiome pour commencer ?

[busard_des_roseaux]

euh, je ne fais pas du tout de logique, donc je ne peux te répondre que naïvement:

moi, je regarderai les tables de vérité de propositions du style
A -> A
A->(B->C)-> ((A->B)->(A->C))

ce sont des tautologies, toujours vraies, que A,B,C aient les valeurs
true T ou false F.

Maintenant, il semble qu'on puisse prendre comme hypothèses des tautologies. On suppose alors le vrai. Par modus ponens,on démontre
d'autres tautologies.

[busard_des_roseaux]

re,

il semble qu'on puisse "remonter" la démonstration à produire
,à l'envers, en partant de la conclusion:

Il faut montrer que neg negA -> A sous l'hypothèse neg neg A

l'axiome 3 permet de simplifier les neg.

[ffpower]

Je trouve bizarre qu il n y ait pas dans le systeme d axiome (A ou A)=>A..Il faudrait au moins qu il y ait l axiome A=>A en tout cas,car sans ca,si on veut prouver un truc du type A=>B,on ne peut normalement pas écrire "Supposons A et prouvons B"...

[busard_des_roseaux]

ffpower,
si on souhaite démontrer neg neg A -> A,

on prend comme hypothèse neg neg A,
on écrit une démonstration ne faisant appel qu'à des modus ponens
de SA1,SA2,SA3

et on doit obtenir en conclusion neg neg A -> A
(sous-entendu "vraie")

[busard_des_roseaux]

re,

Le système d'axiomes SA1,SA2,SA3 peut être considéré comme un programme
informatique qui s'éxécute en mémoire d'ordinateur de la manière suivante:

Il va lire un fichier appelé "base de faits" où sont écrites les propositions vraies.

Avec ses trois lignes de code, SA1,SA2,SA3, il effectue des modus ponens
sur la base de faits et vient enrichir cette base de faits.

Au début, dans la "base de faits", il y a l'hypothèse:
neg neg A

puis
neg neg neg neg A -> neg neg A (par modus ponens de SA1)
neg A -> neg neg neg A (modus ponens de SA3)
neg neg A-> A (modus ponens de SA3)

le programme s'arrête avec la conclusion du théorème écrite dans la base de faits.

le hic, on n'a pas utilisé SA2 :hum:
où le bât blesse, il faut sans doute arriver à écrire "neg neg neg neg A"
dans la base de faits en se servant de SA2.

[ffpower]

Ok,en fait j avais pas vu qu il y avait la regle "modus ponen"..Ce qui explique qu il n y ai pas besoin de mettre mon axiome supplémentaire(qui doit en fait etre équivalant au modus ponen je pense..

[Doraki]

Le corrigé dit de mettre neg neg A en hypothèse ? Mais c'est n'importe quoi xD

Ce système logique fonctionne en écrivant une suite de formules.

On a le droit d'écrire une formule si elle est obtenue à partir d'un schéma d'axiome en remplaçant A,B, et C par des formules quelconques.

On a le droit d'écrire la formule A si on a déjà écrit auparavant la formule B -> A, ainsi que la formule B. (Modus Ponens).

Une preuve d'une formule A consiste en une suite de formules comme je viens de décrire, dont la dernière formule est A.

Il s'avère que via ce procédé on peut prouver toutes les tautologies (n'empêche que je trouve ce truc totalement inutile).

Par exemple, voici une preuve de A -> A :

0. A->(A->A)->A. (SA1 où A=A et B=A->A)
1. (A->(A->A)->A)->(A->A->A)->A->A. (SA2 où A=A, B=A->A, C=A)
2. (A->A->A)->A->A (Modus Ponens avec les formules 0 et 1)
3. A->A->A (SA1 où A=A et B=A)
4. A->A (Modus Ponens avec les formules 2 et 3)

Pour une preuve de neg(neg A) -> A, il y en a une mais j'ai la flemme de la chercher.

[busard_des_roseaux]

Bonjour Doraki :we: ,

Le corrigé dit de mettre neg neg A en hypothèse ? Mais c'est n'importe quoi xD

tu crois ? ça parait naturel décrire neg neg A en hypothèse (disons, en IA, dans la "base de faits") si l'on souhaite démontrer
l'implication neg neg A->A

On a le droit d'écrire une formule si elle est obtenue à partir d'un schéma d'axiome en remplaçant A,B, et C par des formules quelconques.

peux tu préciser ce que tu entends par quelconques ? a-t-on le droit de remplacer B par .F. ,par exemple, ou par A->A.
moi, je pensais me restreindre uniquement à des propositions déja établies
(ie, déja écrites dans la "base de faits"). donc au départ, il n'y a que neg neg A.

3. A->A->A

il faut parenthéser. Quand A=.F.
(A->A)->A = .F.
A->(A->A) = .V.

Cordialement,

[Doraki]

tu crois ? ça parait naturel décrire neg neg A en hypothèse (disons, en IA, dans la "base de faits") si l'on souhaite démontrer
l'implication neg neg A->A

Non ça c'est une règle qu'on trouve habituellement dans d'autres systèmes logiques (style calcul des séquents). Ce qu'on a ici n'a rien à voir.
Et puis si on fait ça, il faut alors démontrer A et pas neg neg A -> A.

Ceci dit on peut montrer que si on a une preuve d'une formule A en prenant une formule B en hypothèse, comme tu dis, et bien on peut construire une vraie preuve de la formule B->A

peux tu préciser ce que tu entends par quelconques ? a-t-on le droit de remplacer B par .F. ,par exemple, ou par A->A.
moi, je pensais me restreindre uniquement à des propositions déja établies
(ie, déja écrites dans la "base de faits"). donc au départ, il n'y a que neg neg A.

Bah une formule quelconque, tu peux mettre tout ce que tu veux, tu peux mettre des trucs qui ne sont pas des tautologies.
(je sais pas ce que tu veux dire par .F., mais si c'est une formule c'est bon)

il faut parenthéser. Quand A=.F.
(A->A)->A = .F.
A->(A->A) = .V.

Euh traditionnellement, -> est associatif à gauche (et puis à force les parenthèses partout, ça devient lourd)
A->B->C = A->(B->C)

D'autre part, on se fiche pas mal de la sémantique des formules, le système est purement syntaxique. (on évalue jamais des formules).
La correspondance "La sémantique de la formule F est une tautologie
La formule F est prouvable dans ce système syntaxique", est justement un théorème à propos de ce système.



En reprenant ta preuve cheatée :
(Je note A* = neg A, c'est plus court)

0. (cheat) : A**
1. (SA1) : A** -> A**** -> A**
2. (MP) : A**** -> A**
3. (SA3) : (A**** -> A**) -> A* -> A***
4. (MP) : A* -> A***
5. (SA3) : (A* -> A***) -> A** -> A
6. (MP) : A** -> A
7. (MP) : A

On peut éliminer l'hypothèse et on a :

0. (SA1) : A** -> A**** -> A**
1. (SA3) : (A**** -> A**) -> A* -> A***
2. (SA1) : ((A**** -> A**) -> A* -> A***) -> A** -> (A**** -> A**) -> A* -> A***
3. (MP:2,1) : A** -> (A**** -> A**) -> A* -> A***
4. (SA2) : (A** -> (A**** -> A**) -> A* -> A***) -> (A** -> A**** -> A**) -> A** -> A* -> A***
5. (MP:4,3) : (A** -> A**** -> A**) -> A** -> A* -> A***
6. (MP:5,0) : A** -> A* -> A***
7. (SA3) : (A* -> A***) -> A** -> A
8. (SA1) : ((A* -> A***) -> A** -> A) -> A** -> (A* -> A***) -> A** -> A
9. (MP:8,7) : A** -> (A* -> A***) -> A** -> A
10. (SA2) : (A** -> (A* -> A***) -> A** -> A) -> (A** -> A* -> A***) -> A** -> A** -> A
11. (MP:10,9) : (A** -> A* -> A***) -> A** -> A** -> A
12. (MP:11,6) : A** -> A** -> A
13. (SA1) : A** -> (A** -> A) -> A**
14. (SA2) : (A** -> (A** -> A) -> A**) -> (A** -> A** -> A) -> A** -> A**
15. (MP:14,13) : (A** -> A** -> A) -> A** -> A**
16. (MP:15,12) : A** -> A**
17. (SA2) : (A** -> A** -> A) -> (A** -> A**) -> A** -> A
18. (MP:17,12) : (A** -> A**) -> A** -> A
19. (MP:18,16) : A** -> A
CQFD

[busard_des_roseaux]

joli.

la preuve cheatée (cheat codes=paramètres optionnels passés à une procédure) est ce que l'on fait habituellement , au collège ?
on pose les hypothèses, on applique les théorèmes, on conclue.

je trouve la preuve non cheatée étonnante à bien des égards:
dans la logique usuelle, il y a une infinité de tautologies du style
B-> (A ou A*)
(A et A*) -> B
A <-> A**
(A -> A*)->A*
etc..

il semble qu'on puisse en choisir certaines pour obtenir formellement
d'autres. On peut donc espérer garder une famille minimale
d'axiomes décrivant l'activité (la pensée) logique. Le souçi, c'est
que le premier théorème d'incomplétude (Gödel) dit que tout système
d'axiomes,avec arithmétique, est incomplet. Comment concilier
cette réduction d'un côté et cette inflation de l'autre.

[ffpower]

Ah ok,modus ponen,ct juste dire que si A et A=>B sont des theoremes,alors B est un theoreme,pas qu on peut supposer et montrer B..donc effectivement le premier raisonnement était foireux.Bon,et j avais tort,on peut en effet prouver A=>A,mais malgré tout ce systeme d axiome ne me semble pas complet.Comment vous prouveriez par exemple la propriété (non A=>A)=>A

Busard:Le systeme logique,tel que décrit ici,n est pas incomplet au sens de Godel(il est bien trop simple).On montre la légitimité des preuves intuitives habituelles("Supposons A etmontrons B",preuves par l absurde,preuves par disjonction de cas..).Et au final,on montre que la démonstration d une formule logique revient juste a regarder sa table de vérité..

[Doraki]

Le formalisme présenté n'a pas de notion de contexte (ce qui impose de faire des trucs horriblement moches et loin des raisonnements humains)

Au collège en géométrie on fait à peu près ça, à part que on suppose qu'on a un contexte C de formules déjà vraies (les conditions du problème), qu'on a le droit d'utiliser quelques postulats, de théorèmes (au fur et à mesure que le cours progresse, le système change !! hahaha) et qu'on a la règle de Modus Ponens.
Et que si au final on a une preuve d'un énoncé F, en fait on a pas prouvé F, mais on a prouvé C -> F.

Et puis après on fait des trucs bien plus compliqués.

Ici, le théorème de Gödel ne s'applique pas parceque la logique propositionnelle d'ordre 0 est loin d'être assez complexe pour contenir l'arithmétique.

Le système permet de démontrer toutes les formules de logique minimale qui sont vraies, avec ces 3 schémas d'axiomes et la règle de MP (les gens aiment bien chercher le système le plus petit possible qui reste complet)
(Je sais pas si j'ai déjà vu la preuve de la complétude mais c'est bien sur un truc difficile à montrer)

Encore que là chuis sceptique sur la prouvabilité de A -> A**.
Mais il ressemble tellement à rien ce système.. il est pas fait pour faire des preuves avec, juste pour impressioner les gens.

[busard_des_roseaux]

merçi beaucoup ,Doraki,

autre question: comment gère-t-on dans ce système SA1,SA2,SA3,
le fait que B est indéterminée ? où va-t-on chercher ses valeurs ?

[busard_des_roseaux]

Le système permet de démontrer toutes les formules de logique minimale qui sont vraies, avec ces 3 schémas d'axiomes et la règle de MP (les gens aiment bien chercher le système le plus petit possible qui reste complet)

si l'on considère la fonction qui, à tout assemblage formé de lettres majuscules A,B,C.. et de connecteurs neg,OU,ET,->
associe la fonction définie par les tables de vérité
de à valeurs dans ,
(0=faux,1=vrai)

est-ce que le système SA1,SA2,SA3 permet de démontrer
toutes les formules telles que soit la fonction constante égale à 1 (vraie) , ie, les tautologies ?

[ffpower]

merçi beaucoup ,Doraki,

autre question: comment gère-t-on dans ce système SA1,SA2,SA3,
le fait que B est indéterminée ? où va-t-on chercher ses valeurs ?

Ce qui est sous entendu c est que c est pour toute formule logique B,autrement B peut etre n importe quelle suite de lettre et de symboles autorisés(ici => et neg et les parantheses) de facon a ce que cette suite de symbole est "un sens logique"(ce qui se définit formellement assez facilement).SA1,SA2,SA ne sont pas en fait vraiment des axiomes mais plutot des familles d axiomes

[ffpower]

si l'on considère la fonction qui, à tout assemblage formé de lettres majuscules A,B,C.. et de connecteurs neg,OU,ET,->
associe la fonction définie par les tables de vérité
de à valeurs dans ,
(0=faux,1=vrai)

est-ce que le système SA1,SA2,SA3 permet de démontrer
toutes les formules telles que soit la fonction constante égale à 1 (vraie) , ie, les tautologies ?

C est justement ce que je disait je crois pas qu on puisse prouver ici (neg A=>A)=>A.par contre si on rajoute cet axiome SA4,oui on peut

[tsoungui]

C est justement ce que je disait je crois pas qu on puisse prouver ici (neg A=>A)=>A.par contre si on rajoute cet axiome SA4,oui on peut

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?