Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
203 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Démonstration formelle en logique

Envoyé par SylvainK 
Démonstration formelle en logique
il y a neuf années
Je dispose des axiomes (Axx) et théorèmes (Thxx) suivants :

A1 P1 => (P2 => P1)
A2 (P1 => (P2 => P3)) => ((P1 => P2) => (P1 => P3))

A3 P1 => ¬¬P1
A4 ¬¬P1 => P1
A5 (P1 => P2) => (¬P2 => ¬P1)

A6 P1 => (P2 => (P1 /\ P2))
A7 (P1 /\ P2) => P1
A8 (P1 /\ P2) => P2

A9 P1 => (P1 \/ P2)
A10 P2 => (P1 \/ P2)
A11 ¬P1 => ((P1 \/ P2) => P2)

Th1 (P1 \/ P1) => P1
Th2 (P1 => P2) => ((P2 => P3) => (P1 => P3))

J'aimerai en déduire les théorèmes suivants :
P1 \/ ¬P1
(P1 \/ P2)=> ((P1 => P3) => ((P2 => P3) => P3))

J'ajoute que toute la puissance du "Ou" est incluse dans l'axiome A11.
Pour info les axiomes sont ceux que Patrick Dehornoy mentionne dans son cours de logique.
Le contexte est un vérifieur informatique de démonstration de logique.

Toute aide est la bienvenue.



Edité 1 fois. La dernière correction date de il y a neuf années et a été effectuée par SylvainK.
Re: Démonstration formelle en logique
il y a neuf années
Bonjour, SylvainK
Attention, il y a une erreur de saisie au niveau de l'axiome A10.
Re: Démonstration formelle en logique
il y a neuf années
Merci c'est corrigé.
Re: Démonstration formelle en logique
il y a neuf années
avatar
Je suis étonné que CC n'ait pas encore fondu sur ce fil...;)
Re: Démonstration formelle en logique
il y a neuf années
avatar
Ah bah, il n'est pas obligé d'être connecté 24h/24 !


[attachment 21020 CCFondantSurSaProie.png]




Edité 2 fois. La dernière correction date de il y a neuf années et a été effectuée par remarque.


JLT
Re: Démonstration formelle en logique
il y a neuf années
avatar
Son réveil a peut-être fondu.
[attachment 21022 horlogedali.jpg]



Edité 1 fois. La dernière correction date de il y a neuf années et a été effectuée par JLT.


Re: Démonstration formelle en logique
il y a neuf années
Oui après avoir posté, j'ai vu un de ses posts sur la logique combinatoire, ceci dit je ne sais pas faire ça avec des "ou" et des "non", ma correspondance de Curry-Howard s'arrêtant à l'implication simple et le type fonction de base.
Re: Démonstration formelle en logique
il y a neuf années
:)-D non j'étais parti déjeuner avec un grand mathématicien et j'ai fait un saut à la bibli pour emprunter un super livre de géométrie conseillé par Bruno...

Pour l'aide attendue, je t'avoue que je veux bien te mettre un des mes 13646 prouveurs-caml compulsifs automatiques en ligne (je crois que j'en ai deja is plusieurs) , mais j'ai un peu la flemme de me taper toutes les transformations de déductions naturelles en Hilbert-modus-ponens-seul-raisonnements :D

Bon, je vais regarder ça...

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi



Edité 1 fois. La dernière correction date de il y a neuf années et a été effectuée par AD.
Re: Démonstration formelle en logique
il y a neuf années
Citation

ceci dit je ne sais pas faire ça avec des "ou" et des "non", ma correspondance de Curry-Howard s'arrêtant à l'implication simple et le type fonction de base.

C'est largement suffisant, tu ajoutes tout ce que tu veux en "l'admettant" au sens "CuHO", ie comme des "instructions magiques" :D

Bon, non, mais je vais regarder ça, t'inquiète...

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
ev
Spoonerism
il y a neuf années
avatar
Comme dirait Cidrolin, il faut pas confondre Curry-Howard avec Hurry coward !

amicalement,

e.v.
Re: Démonstration formelle en logique
il y a neuf années
En fait, j'ai l'impression que la seule chose qui manque à ton petit système est le "tout". Donc il faut le simuler. Par exemple, tu peux essayer tout:= non(X=>X) . Comme tu as Y=>(X=>X) tu as bien que [non(X=>X)]=>nonY (pour tous les Y que tu auras envie) et donc avec A4 tu peux remplacer Y par non Z. Tu disposes donc bien d'un "tout".

Q:=P ou nonP.

Si nonQ alors en particulier nonP et donc Q, donc tu as bien que (nonQ)=>Q dans ton système (tu Hilbertises tout àa avec A1,A2).

Ensuite avec le "tout" préfabriqué de ci-dessus (c'est pas très joli):

(Q=>tout)=>Q donc (Q=>tout)=>(Q et (Q=>tout)) donc (Q=>tout) =>tout donc non(nonQ) donc Q.

Je te prouve l'équivalence entre non Q et (Q=>tout):

si non Q alors (non(tout))=>(nonQ) donc non(nonQ)=>non(non(tout)) donc Q=>tout
réciproquement: si Q=>tout alors non(tout)=>nonQ et donc non(non(X=>X))=>nonQ et donc nonQ

Tu n'as plus qu'à mettre les étapes faciles et à Hilbertiser :D

Si tu ne sais pas Hilbertiser je te dirai comment faire.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Et si "X=>X" te gêne (vu que c'est pas un axiome), tu peux prendre un axiome de ton systeme et le nier (par exemple non(A1)) en guise de "tout".

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Comme je vais me déco, je te dis comment "Hilbertiser".

A chaque fois que tu dis "supposons A...donc B", tu remplaces le dernier modus ponens [X=>B; X ]---> B par A=>(X=>B) ; A=>X et tu utilises (A2) pour arriver à A=>B.

Tu remontes ainsi dans l'arbre jusqu'à éliminer toutes les suppositions provisoires. Il se peut que certains B ne soient pas dû au A que tu as supposé, et là tu utilises (A1) pour pouvoir obtenir A=>B quand-même.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
X=>X ne me gêne pas je l'ai déja démontré (enfin Patrick Dehornoy l'a fait pour nous...)
Re: Démonstration formelle en logique
il y a neuf années
ma solution te convient tu vois comment la construire ou tu veux plus de détails?

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Bon, évidemment, c'est optimisable :D mais c'est pour te donner un idée de pourquoi je te demandais "tu veux plus de détails" (en fait j'ai passer à peu près le raisonnement précédent à un Hilbertiseur naturel sans optimiser (et encore j'ai retiré quelques redondances qui font que c'est raccourci)) :D


(non(non(p ou nonp)))=>(p ou non p)
((non(p ou nonp))=>(non(a=>a)))=>(((a)=>(a))=>(non(non(p ou nonp))))
((non(p ou nonp))=>(((p)=>(non(a=>a)))=>(non(a=>a))))=>(((non(p ou nonp))=>((p)=>(non(a=>a))))=>((non(p ou nonp))=>(non(a=>a)))) 

...
[200 à 300 lignes illisibles qui de toutes façons n'auraient été lues par personne. AD]
...

(non(p ou nonp))=>(((a)=>(a))=>((non(p ou nonp))=>(nonp)))
(non(p ou nonp))=>(((a)=>(a))=>(nonp))
(non(p ou nonp))=>((p)=>(non(a=>a)))
(non(p ou nonp))=>(non(a=>a))
((a)=>(a))=>(non(non(p ou nonp)))
(a)=>(a)
non(non(p ou nonp))
p ou non p

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi



Edité 2 fois. La dernière correction date de il y a neuf années et a été effectuée par AD.
Re: Démonstration formelle en logique
il y a neuf années
Les 200 à 300 lignes me font un petit peu peur...
Re: Démonstration formelle en logique
il y a neuf années
C'était juste pour te dire qu'il y a une façon automatique (quelques lignes de caml pour obtenir ça) de passer d'une preuve avec des "supposons A... donc B; donc au final, sans supposer A, on a prouvé A=>B" à une preuve n'utilisant que le modus ponens.

Du coup, quel genre de solutions rédigées formellement souhaites-tu à ta demande? Bon après, il y a les concours d'esthétiques, trouver la preuve la plus courte possible avec juste le modus ponens, mais la plupart même des plus courtes preuves sont longues.

Sinon, à mon post précédant la blague des 200 lignes, je t'ai donné essentiellement la solution.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Et bien il me faut juste de quoi donner à manger à mon vérifieur (écrit lui aussi en OCaml).
Je pourrai admettre ces résultats bien connus de logique propositionnelle, mais j'aimerai rester le plus rigoureux (et formel) possible.
Re: Démonstration formelle en logique
il y a neuf années
Pour "a ou non a" je vois l'idée oui, et pour (a oub) =>((a=>c) =>( (b=>c) =>c)) ?
Re: Démonstration formelle en logique
il y a neuf années
bin tu supposes a ou b; puis a=>c ; puis b=>c et tu veux prouver c:

il suffit de prouver non(non c) et par ce qui précède (non c)=>c

donc tu supposes non c: et tu veux prouver c.

de non c tu peux déduire non a (car tu as a=>c) donc b donc c

(Je ne reposte pas le Hilbertisé de ce raisonnement, AD ne serait pas content :D )

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
En petits caractères, un peu nettoyé (pas beaucoup), ça devrait être acceptable pour une lecteure attentive par Sylvain:

En posant z:= "a ou non a"

non tout
(non a)=>(z)
((non a)=>(z))=>((non z)=>(non(non a)))
((non z)=>((non a)=>(z)))=>((non z)=>((non z)=>(non(non a))))
(non z)=>((non z)=>(non(non a)))
((non z)=>(non z))=>((non z)=>(non(non a)))
(non z)=>(non(non a))
(non(non a))=>(a)
((non z)=>(non(non a)))=>((non z)=>(a))
(non z)=>(a)
(a)=>(z)
((a)=>(z))=>((non z)=>(non a))
((non z)=>((a)=>(z)))=>((non z)=>((non z)=>(non a)))
(non z)=>((non z)=>(non a))
((non z)=>(non z))=>((non z)=>(non a))
(non z)=>(non a)
((non a)=>(non a))=>((non z)=>((non a)=>(non a)))
(non z)=>((non a)=>(non a))
(non a)=>((non tout)=>(non a))
((non tout)=>(non a))=>((a)=>(tout))
(((non a)=>(((non tout)=>(non a))=>((a)=>(tout))))=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout)))))=>((non z)=>(((non a)=>(((non tout)=>(non a))=>((a)=>(tout))))=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout))))))
(non z)=>(((non a)=>(((non tout)=>(non a))=>((a)=>(tout))))=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout)))))
((non z)=>((non a)=>(((non tout)=>(non a))=>((a)=>(tout)))))=>((non z)=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout)))))
(non z)=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout))))
((non z)=>((non a)=>((non tout)=>(non a))))=>((non z)=>((non a)=>((a)=>(tout))))
(non z)=>((non a)=>((a)=>(tout)))
((non z)=>(non a))=>((non z)=>((a)=>(tout)))
(non z)=>((a)=>(tout))
((non z)=>(a))=>((non z)=>(tout))
(non z)=>(tout)
((non z)=>(tout))=>((non tout)=>(non(non z)))
(non tout)=>(non(non z))
non(non z)
(non(non z))=>(z)
z

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi



Edité 1 fois. La dernière correction date de il y a neuf années et a été effectuée par christophe chalons.
Re: Démonstration formelle en logique
il y a neuf années
L'autre exo explose littéralement :D désolé ...

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Tu as ausi une autre façon de "jouer" à ça: au lieu de "Hilbertisier" à chaque fois que tu décharges une hypothèse d'un raisonnementnaturel, tu rajoutes "H=>blabla" à chaque ligne comprises entre sa supposition et son déchargement. C'est "moins savant", mais ça ne rajoute que des axiomes inoffensifs (faut une structure de preuve linéaires, des suites de phrases)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Ce qui te donne:

non tout
(non z)=>(non z)
(non z)=>((a)=>(z))
(non z)=>(((a)=>(z))=>((non z)=>(non a)))
(non z)=>((non z)=>(non a))
(non z)=>(non a)
(non z)=>((non a)=>(z))
(non z)=>(z)
(non z)=>((non tout)=>(non z))
(non z)=>(((non tout)=>(non z))=>((z)=>(tout)))
(non z)=>((z)=>(tout))
(non z)=>(tout)
((non z)=>(tout))=>((non tout)=>(non(non z)))
(non tout)=>(non(non z))
(non(non z))=>(z)
non(non z)
z

---------------------------------------------------

(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(non tout)))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(a ou b))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(non c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((a)=>(c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(((a)=>(c))=>((non c)=>(non a))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((non c)=>(non a)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(non a))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((non a)=>((a ou b)=>(b))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((a ou b)=>(b)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(b))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((b)=>(c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((non tout)=>(non c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(((non tout)=>(non c))=>((c)=>(tout))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((c)=>(tout)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(tout))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(((non c)=>(tout))=>((non tout)=>(non(non c))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non tout)=>(non(non c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(non(non c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non(non c))=>(c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(c)))


Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a neuf années
Merci beaucoup :)
Re: Démonstration formelle en logique
il y a neuf années
Vus tes MP je pense que l'exercice suivant t'intéressera: [www.les-mathematiques.net]
démontre le théorème (5.2) que j'y affirme (tu as now tout le matos caml pour le fair en deux coups de cuillere)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Démonstration formelle en logique
il y a quatre mois
Les solutions que j'ai trouvées, je ne sais même plus comment.
A ou non A
(A ou B) => (A =>C) => (B =>C) =>C
Re: Démonstration formelle en logique
il y a quatre mois
Et ça t'a pris 9 ans ? grinning smiley
Re: Démonstration formelle en logique
il y a quatre mois
avatar
Seuls les utilisateurs enregistrés peuvent poster des messages dans ce forum.

Cliquer ici pour vous connecter

Liste des forums - Statistiques du forum

Total
Discussions: 149 229, Messages: 1 507 001, Utilisateurs: 27 661.
Notre dernier utilisateur inscrit ibra.


Ce forum
Discussions: 2 517, Messages: 51 078.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page