Déduction formelle
Bonjour j’ai trois formules F,G et H sur un langage. J’aimerais montrer que $\{(F \rightarrow G), (G\rightarrow H) \} \vdash (F\rightarrow H)$. Merci bien. Et si il y a une règle à suivre j’aimerais bien volontier qu’on m’explique. Merci
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
On a $$\Gamma \vdash G \rightarrow H$$ $$\Gamma \vdash (G \rightarrow H) \rightarrow (F \rightarrow (G \rightarrow H)) \quad \text{(règle du calcul propositionnel)}$$ $$\Gamma \vdash F \rightarrow (G \rightarrow H) \quad \text{(modus ponens)}$$ $$\Gamma \vdash (F \rightarrow (G \rightarrow H)) \rightarrow ((F \rightarrow G) \rightarrow (F \rightarrow H)) \quad \text{(règle du calcul propositionnel)}$$ $$\Gamma \vdash (F \rightarrow G) \rightarrow (F \rightarrow H) \quad \text{(modus ponens)}$$ $$\Gamma \vdash F \rightarrow G$$ $$\Gamma \vdash F \rightarrow H \quad \text{(modus ponens)}.$$
La, il t'est demandé de prouver que si A=>B et B=>C alors A=>C
La première chose à faire est de te demander si tu es d'accord que c'est sûr, et pourquoi tu en es sûr. La preuve sera généralement une traduction de cette certitude en langage écrit.
"A l'école", on dira très informellement l'a chose suivante:
1/ Supposons A, A=>B, B=>C.
2/ Du fait que A et (A=>B), on déduit B.
3/ Du fait que maintenant on est sûr de B et qu'on a B=>C, on déduite C
4/ On a donc prouvé, sans supposer A, que A=>C
5/ On a donc prouvé, sans supposer [(A=>B) et (B=>C)] que [(A=>B) et (B=>C)]=>(A=>C)
Je ne sais pas faire en latex les séquents proprement, mais de toute façon, je peux te proposer une suite formelle:
(A=>B) => (A=>B)
[(A=>B) et A] => B
[(A=>B) et A] => [B et ((B=>C)=>(B=>C))]
[(A=>B) et A] => [B et ([(B=>C) et B]=>C )]
[(A=>B) et A] => [B et ([B et (B=>C) ]=>C )]
[(A=>B) et A] => [B et (B=>[(B=>C) =>C] )]
[(A=>B) et A] =>[(B=>C) =>C]
[(A=>B) et A et (B=>C)] =>C
[(A=>B) et (B=>C) et A] =>C
[(A=>B) et (B=>C)] =>(A =>C)
Il n'y a pas de réponse connue à cette question et 1000000 dollars, même, pour payer une preuve que c'est ainsi. Tu demandes comment être inspiré. Par contre, pratique, patience, familiarité t'aideront avec le temps.
L'important est de psychanalyser tes certitudes et non pas de chercher à réciter des élucubrations.
Bien sûr ce n'est pas honnête intellectuellement mais comme il s'agit d'un exercice de base, on peut se douter que ce genre de raisonnement devrait fonctionner.
Apparemment au stade où tu en es, le route inévitable semble être:
1/ Tu psychanalyses si tu es sûr ou pas du truc à prouver
2/ Tu rédiges une preuve comme si tu voulais convaincre un camarade sceptique payé pour ne pas te croire sauf quand il est forcé
3/ Tu traduis (cette étape est juste du secrétariat un peu chiant)
et si je fais la psychanalyse à ta place, ça donne:
supposons A=>(B=>C)
Alors (A et B ) =>C
Alors (B et A) => C
Alors B=>(A=>C)
Sans autre information de ta part sur les exigences et les contraintes de produit fini en système formel, il serait idiot de t'en donner plus. Par exemple le système de Poirot (S,K) est totalement artificiel et produit la logique intuitionniste de manière viceuse en "embeddant" dans S deux axiomes puissants et n'ayant rien à voir et enlaissant un K à peu innocent trainer.
Dans la plupart des systèmes, ce que tu appelles ton exo2 est un axiome (il exprime la commutativité, iele droit de ne pas considérer que l'ordre dans lequel on fait des hypothèses compte. Tu le vois très bien avec la formulation si alors:
Si A alors si B alors C
veut dire pour tout le monde
Si (A et alors C
avec un "et" commutatif.
Je veux bien me tartiner un exposé sur le calcul des séquents, mais vu les efforts latex imbitables que ça me donnerait, j'attends que tu précises sous quelle forme sont attendues tes solutions. Car, l'utilisation de $\vdash$ est juste ment faite pour qu'on n'ait pas à évoquer des axiomes stricto sensu, donc ni ceux utiliser par Poirot, ni les tiens.
\begin{align*}
~&\frac{([A\to (B\to C) ; (A\to ; A \vdash (A\to ] + [A\to (B\to C) ; (A\to ; A \vdash A] }{A\to (B\to C) ; (A\to ; A \vdash B} \\
&\frac{([A\to (B\to C) ; (A\to ; A \vdash (A\to (B\to C))] + [A\to (B\to C) ; (A\to ; A \vdash A] }{A\to (B\to C) ; (A\to ; A \vdash (B\to C)} \\
&\frac{ [ (B\to C); B \vdash (B\to C)] + [ (B\to C); B \vdash B] } { (B\to C); B \vdash C}
\end{align*} Tu as donc finalement déduit : $$
A\to (B\to C) ; (A\to ; A \vdash C.
$$ Tu peux continuer comme suit :
\begin{align*}
~& A\to (B\to C) ; (A\to ; \vdash A \to C \\
& A\to (B\to C) \vdash (A\to \to (A \to C) \\
& \vdash A\to (B\to C) \to ((A\to \to (A \to C))
\end{align*} Et encore, je n'ai pas fait l'arbre attendu pour des raisons latex.
Pour tous énoncés $X,Y,Z$, on note $\mathbf S_{X;Y;Z}$ une preuve de l'énoncé $(X \to Y \to Z) \to (X \to Y) \to X \to Z$.
Pour tous énoncés $T,U$, on note $\mathbf K_{T;U}$ une preuve de l'énoncé $T \to U \to T$.
Déclarer des énoncés comme axiomes (i.e. les supposer) revient à dire qu'on fait comme si on avait déjà leurs preuves (à la manière de la déclaration de variables pour un programme).
Idée: si $p$ est une preuve de l'énoncé $A\to B$, $p$ est vue comme une fonction de l'ensemble des preuves de $A$ dans celui des preuves de $B$. Si $q$ est une preuve de $A$, $p(q)$ en est alors une de $B$. Le modus ponens est alors l'application d'une fonction à un argument.
Soit $\text{x}:= F \to G \to H$ (on le suppose). Alors:
$$\begin{align}
1° ) & [G \to (F \to G) \to F \to H] \to (G \to F \to G) \to G \to F \to H \tag{$\mathbf S_{G;F\to G;F \to H}$} \\
2° ) & [(F \to G) \to F \to H] \to G \to (F \to G) \to F \to H \tag{$\mathbf K_{(F \to G) \to F \to H;G}$ } \\
3° ) & (F \to G \to H) \to (F \to G) \to F \to H\tag{$\mathbf S_{F;G;H}$} \\
4° ) & F \to G \to H \tag{x} \\
5° ) & (F \to G) \to F \to H\tag{modus ponens 3,4} \\
6° ) & G \to (F \to G) \to (F \to H)\tag{modus ponens 2,5} \\
7° ) & (G \to F \to G) \to G \to F \to H \tag{modus ponens 1,6} \\
8° ) & G \to F \to G \tag{$\mathbf K_{G;F}$ } \\
9° ) & G \to F \to H\tag{modus ponens 7,8}
\end{align}$$
$\newcommand{\K}[2]{#1 \to #2 \to #1}$
Résumé du théorème de déduction: soient $\mathcal H$ un ensemble d'énoncés, $P,Q$ des énoncés et $R_1,...,R_m=Q$ une preuve de $Q$ dans un système de Hilbert (i.e. chaque terme de la suite est un axiome, ou est obtenu à l'aide des précédents par modus ponens) avec comme axiomes les énoncés de la forme $\S A B C$ ($\sigma$)ou $\K A B$ ($\kappa$)(avec $A,B,C$ énoncés), ou un énoncé de $\mathcal H \cup \{P\}$ (i.e. $Q$ est prouvé en rajoutant $P$ aux hypothèses $\mathcal H$).
Alors l'algorithme suivant fournit une preuve de $P\to Q$ sous les seules hypothèses $\mathcal H$ (et les énoncés logiques évoqués de type $\sigma,\kappa$ plus haut). "$++$" abrège la concaténation de deux suites.
1°)$L_0$:= liste vide
2°)Pour $m\leq n$, si la liste d'énoncés $L_{n-1}$ est définie, poser $L_n := L_{n-1} ++ \mathcal X$ avec :
(i) si $R_n$ est dans $\mathcal H$ ou est un énoncé de type $\sigma$ ou $\kappa$,
prendre $\mathcal X:= \left [\K {R_n} P;R_n, R_n \to P \right ]$
(ii) si $R_n = P$, prendre $\mathcal X:= [\S P {(P \to P)} P; \K P {(P\to P)}; \left ( \K P P\right ) \to P \to P; \K P P; P\to P]$
(iii) si $R_n$ est obtenu par modus ponens (i.e. $R_i = R_j \to R_n$ avec $i,j < n$) alors
$\mathcal X := \left [\S P {R_j}{R_n}; \left (P \to R_j \right )\to \left (P \to R_n \right ); P \to R_n \right ]$. On construit ainsi une liste où aparaissent tous les $P \to R_i$ et qui est une preuve de $P\to R_n=P\to Q$.
Donc pour obtenir $G\to F \to H$ sous l'hypothèse $F\to G \to H$, on peut d'abord obtenir $H$ sous $G,F,G\to F \to H$ (facile) puis appliquer la procédure précédente deux fois de suite avec $F$ puis $G$.
L'inconvénient est que les preuves obtenues comme ça peuvent être longues et illisibles...
1/ Il a été découvert( ça porte le nom de correspondance de Curry Howard) que toute preuve de maths est une fonction (est le nom d'une fonction plus correctement).
2/ Par exemple l'identité est le nom d'une des preuves de $A\to A$ qui est la fonction allant de $A$ dans $A$, définie sur $A$ et codable par $x\mapsto x$.
3/ Dans la suite, je note $A\to B$ l'ensemble des applications de $A$ dans $B$.
4/ Chaque fois que tu peux construire un élément d'un ensemble à partir de son nom, sans connaître ses feuilles, tu disposes d'une preuve de cet ensemble à la condition de lire son nom comme une phrase. Exemple:
4.1/ Tu peux construire un élément de $(A\to (B\to C))\to (B\to (A\to C))$ sans avoir besoin de connaître quoique ce soit sur $A,B,C$. Par exemple, la fonction $G:=[f\mapsto (x\mapsto (y\mapsto f(y)(x)))]$ (mais aussi tout plein d'autres, éventuellement égales à elle, mais définies autrement)
4.2/ Cela te donne une preuve de $(A\to (B\to C))\to (B\to (A\to C))$
C'est une sorte de réciproque de (1). En fait, mais c'est HS, on peut prouver que toute fonction est une preuve (n'en déplaise à certaines écoles de pensée qui ont choisi le déni, mais c'est un autre débat).
5/ Comme la notion de fonction a été très mal introduite dans les études (en particulier l'erreur consistant à donner des ensembles de départ et d'arrivée), les gens ont mis beaucoup de temps à prendre conscience de "cette évidence". Par exemple, les définitions étant maladroites, et victimes de l'histoire, la plupart des gens ne perçoivent pas que la fonction dans l'exemple ci-dessus est en fait un élément de TOUS LES ENSEMBLES $(A\to (B\to C))\to (B\to (A\to C))$
6/ Il serait de corriger le tir, je vais donc raccourcir drastiquement. Au lieu de "est un élément de", je vais utiliser l'expression "garantit".
7/ Par exemple la fonction $G$ ci-dessus garantit toutes les $(A\to (B\to C))\to (B\to (A\to C))$ quand $A,B,C$ varient.
8/ De même que $x\mapsto x$ garantit toutes les $A\to A$ (elle garantit même toutes les $A\to B$ telles que $A\subset B$. Idem pour $G$, on pourrait faire ce petit saut généralisant.
9/ Foys s'est intéressé à ça il y a quelques années et il s'est "pris d'amour" pour cette passerelle, ce qui lui fait connaître "d'un coup" comment prouver une phrase prouvable dans un système de Hilbert (c'est ce que tu demandais pour des cas particuliers, lui, comme moi, pouvons le faire de manière dite "systématique" et sans besoin d'inspiration grâce à cette passerelle).
10/ Maintenant le problème est que tu ne nous a toujours pas dit s'il fallait te répondre dans un système de Hilbert ou dans le calcul des séquents ce qui fait que les réponses que tu as reçues sont pour l'heure très risquées d'être hors sujet.
11/ Qu'a fait Foys et pourquoi observe-t-on chez lui une prédominance de l'admission de l'axiome $(A\to (B\to C))\to ((A\to \to (A\to C))$ ?
11.1/ Et bien c'est simple : tu as la fonction $S$ qui garantit toutes les $(A\to (B\to C))\to ((A\to \to (A\to C))$. De même tu as la fonction $K$ qui garantit toutes les $A\to (B\to A)$
11.2/ Leurs définitions sont
\begin{align*}
S&:=[x\mapsto (y\mapsto (z\mapsto [x(z)(y(z))]))] \\
K&:=[x\mapsto (y\mapsto x)]
\end{align*} et ce qu'a fait foys est tout bêtement de construire la fonction $G$ avec elles.
Pourquoi, historiquement, ce système, bien que complètement délirant, a été retenu. Et bien parce qu'il n'a pas été découvert comme ça. Mais avec des phrases. Or comme manipuler des phrases donne des textes très longs, les gens étaient noyés.
12/ LA PROPRIÉTÉ qui fait tout est la suivante : on peut OBTENIR le mécanisme (x\mapsto ) sans rajouter de signe une fois qu'on a $S,K$.
13/ Je te le prouve :
13.1/ supposons que tu saches obtenir $x\mapsto mot_1$ (qui donnera une fonction $f$ et $x\mapsto mot_2$ qui donnera une fonction $g$. Comment obtenir $x\mapsto mot_1(mot_2)$? Et bien c'est tout simplement $S(f)(g)$.
13.2/ Initialisation: $x\mapsto motSansLaLettrex$ est $K(motSansLaLettrex)$
14/ Or une fois ça capté, Foys n'a plus besoin d'avoir d'idée puisque $G$ a été définie plus haut avec des $\mapsto $ qu'il retire à coup de $S,K$, ce qui lui donne une preuve AVEC LE MODUS PONENS SEUL, pourvu qu'on a aussi compris que si $f$ garantit $X\to Y$ et $g$ garantit $X$ alors $f(g)$ garantit $Y$, ce qui est évident mais est mieux en le disant que sans le dire.
15/ Pour exemple, je t'explique ce qu'il s'est passé ensuite dans le cerveau de Foys, qu'il a pu opérer en mangeant des cacahuètes et visionner BFMTV en même temps.
Wanted f(x)(y)(z) = x(z)(y). Dorénavant, les parenthèses sont sous-entendues comme suit : abc veut dire (ab)c, et a(b) s'écrit ab. Les espaces sont pédagogiques
xzy =
xz(Kyz)) =
Sx(Ky) z =
S(Kxy)(Ky) z =
S(Kx) K y z =
S(Kx) (KKx) y z =
S K (KK) x y z ................. Euréka, il sait qu'il vient de construire $G:= S K (KK) $
Ensuite il n'a plus qu'à te le traduire sous la forme d'une preuve sans le système de Hilbert, qui sera d'une forme très simple, mais longue à cause des phrases puisqu'elle dira :
(1) J'ai S, j'ai K
(2) J'en déduis SK
(3) J'ai K, et j'ai K
(4) J'en déduis KK
(5) J'ai SK par (2) et KK par (4), j'en déduis SK(KK)
CQFD
Voili voilà, c'est tout.
Mais une fois de plus, cet algorithme sans faille et automatique n'est absolument pas à ton programme puisque de toute façon, ce qu'il permet de faire c'est traduire une preuve NATURELLE en preuve n'utilisant QUE le modus ponens et des axiomes. Il est assez rare que les profs de M1,2 demandent ça (et encore moins Li). Ce serait comme demander, au moment du chapitre sur la multiplication posée de mettre 13206584 à la puissance 7 à la main en gros.
Tu demandais la fonction $Desir:=[f \mapsto (g\mapsto (x\mapsto [f(g(x) ) ]))]$.
f (g x) =
(K f x) (g x) =
S (K f) g x =
Remarque: si tu es flemmard, tu remarques que tu as déjà fait tout le taf ici, puisque tu auras dans le cas particulier $(f,g):=(S,K)$:
S (K f) =
S (K S) K f
Tu peux donc écrire directement: f (g x) = S (K S) K f g x
et dire que Desir = S (K S) K
J'ignore si c'est ce qu'a fait Poirot.
Vérification: S (K S) K f g x = (K S) f (K f) g x = S (K f) g x = (K f g) (g x) = f (g x)
http://www.les-mathematiques.net/phorum/read.php?16,1918784,1918968#msg-1918968
Tu as utilisé S (K X) Y
X,Y étant tes hypothèses.
C'est la syntaxe ( (X=>Y) * X ) = Y itérée, c'edt très simple.
Traduction: la règle en question (qui est une simple phrase) est garantie par $S$.
Poirottraduit dit donc: je cherchais $u,v$ de manière à obtenir que $Suv$ garantisse $F \rightarrow H$
Poirot: J'ai déjà à disposition $F \rightarrow G$, et il me reste donc à savoir comment obtenir $F \rightarrow (G \rightarrow H)$
Traduction: j'avais $v$. Il me restait à trouver $u$.
Poirot: ce qui est facile car je dispose aussi de $G \rightarrow H$.
Traduction: je dispose d'un truc $u$ tel que $Ku$ le garantit.
Finalement j'obiens que $S(Ku)v$ garantit $F\to H$ quand $v$ garantit $F\to G$ et $u$ garantit $G\to H$
En fait l'algo est le suivant (la raison de la préférence de (S,K) dans les livres et sur internet provient probablement de la facilité à le définir avec ce système)
Soit $\alpha$ est une lettre; si $E$ ne possède aucune occurrence de $\alpha$ on pose $\lambda \alpha. E:= KE$ et $\lambda \alpha.E\alpha := E$. Sinon, on pose $\lambda \alpha .\alpha := SKK$ et $\lambda \alpha.MN:= S (\lambda \alpha.M) (\lambda \alpha.N)$.
Alors $\lambda y.\lambda z.xzy = \lambda y. S(\lambda z.xz)(\lambda z.y)=\lambda y .Sx (Ky) = S(\lambda y.Sx) (\lambda y.Ky) = S(K(Sx))K$.
Noter que ce terme apparaît explicitement dans ma preuve écrit de haut en bas (avec notation polonaise inverse et les bons types des occurrences de S et K).
En appliquant encore l'algo avec $x$ on trouverait $\lambda x.S(K(Sx))K = S(S(KS) (S(KK)S))(KK)$. Je ne pense pas qu'un permuteur de variables (c'est ce que fait ce combinateur) avec moins de constantes S,K existe.
(le fait que $\lambda u.$ retire toutes les occurrences de la lettre $u$ d'un terme est clair vu l'algo; pour l'autre propriété, tout se fait par induction sur la taille du terme en question. Commencer avec le cas où $n=1$ puis $n\geq 1$ et $v_i = x_i$ pour tout $i$ -i.e. montrer l'égalité$ (\lambda x1.\lambda x_2....\lambda x_n T)x_1 x_2 ... x_n = T$. Puis conclure avec le cas général en remarquant que les règles de simplification donnant les égalités commutent aux opérations de substitution de variables $[\vec x = ...]$).
J'en ai donné au moins 10 différents sur le forum avec les axiomes réalisés associés.
Le problème de S est qu'il embouteille à lui seul W et les composeurs.
Avec le jeu T, J, W , K tu obtiens même tout d'un coup et rien qu'avec T,J à la fois abstraction et pouvoir de mettre tout SANS PARENTHESE (S,K ne le permet pas).
En appelant T le combi suivant:
T uvxy := uy(vx)
Pour une puissance équivalente il faut deux composeurs au moins en plus de B où je note
Bxy := yx
L'élimination des parenthèses permet de coder toute preuve par un simple entier.