Équivalence syntaxique
Bonjour,
je lis la méthode de Herbrand dans le Cori-Lascar (tome 1, page 245). Il est dit qu'on peut prouver que toute formule est syntaxiquement équivalente à une formule sous forme prénexe.
Par exemple, j'aimerais prouver que la formule $F=\exists x P(x) \rightarrow \exists y Q(y)$ est syntaxiquement équivalente à la formule $G=\forall x \exists y \neg P(x) \vee Q(y)$.
Si j'ai bien compris jusque là, le fait que ces deux formules soient logiquement équivalentes (tout modèle de l'une est un modèle de l'autre et réciproquement), permet d'affirmer qu'elles sont aussi syntaxiquement équivalentes. J'ai essayé de trouver une démonstration directe de $F \leftrightarrow G$. En utilisant les tautologies $A\rightarrow (B \rightarrow (A\land
)$ et $((A\rightarrow \land (B\rightarrow A))\rightarrow (A\leftrightarrow $, j'ai obtenu :
\begin{align*}
(\exists x P(x) \rightarrow \exists y Q(y))&\leftrightarrow \neg(\exists x P(x)) \vee \exists y Q(y)\\
\exists x P(x) &\leftrightarrow \neg \forall x \neg P(x)\\
\neg (\exists x P(x))&\leftrightarrow \neg \neg \forall x \neg P(x)\\
\neg \neg \forall x \neg P(x)&\leftrightarrow \forall x \neg P(x)\\
\neg (\exists x P(x))&\leftrightarrow \forall x \neg P(x)
\end{align*} Le nombre d'étapes avant de parvenir au résultat semble important. Est-ce la bonne démarche ? Sinon comment doit-on s'y prendre ? Merci beaucoup pour votre aide.
je lis la méthode de Herbrand dans le Cori-Lascar (tome 1, page 245). Il est dit qu'on peut prouver que toute formule est syntaxiquement équivalente à une formule sous forme prénexe.
Par exemple, j'aimerais prouver que la formule $F=\exists x P(x) \rightarrow \exists y Q(y)$ est syntaxiquement équivalente à la formule $G=\forall x \exists y \neg P(x) \vee Q(y)$.
Si j'ai bien compris jusque là, le fait que ces deux formules soient logiquement équivalentes (tout modèle de l'une est un modèle de l'autre et réciproquement), permet d'affirmer qu'elles sont aussi syntaxiquement équivalentes. J'ai essayé de trouver une démonstration directe de $F \leftrightarrow G$. En utilisant les tautologies $A\rightarrow (B \rightarrow (A\land
)$ et $((A\rightarrow \land (B\rightarrow A))\rightarrow (A\leftrightarrow $, j'ai obtenu :\begin{align*}
(\exists x P(x) \rightarrow \exists y Q(y))&\leftrightarrow \neg(\exists x P(x)) \vee \exists y Q(y)\\
\exists x P(x) &\leftrightarrow \neg \forall x \neg P(x)\\
\neg (\exists x P(x))&\leftrightarrow \neg \neg \forall x \neg P(x)\\
\neg \neg \forall x \neg P(x)&\leftrightarrow \forall x \neg P(x)\\
\neg (\exists x P(x))&\leftrightarrow \forall x \neg P(x)
\end{align*} Le nombre d'étapes avant de parvenir au résultat semble important. Est-ce la bonne démarche ? Sinon comment doit-on s'y prendre ? Merci beaucoup pour votre aide.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
C'est pour ça qu'on n'en fait pas sauf quand on les considère comme objets d'étude :-D
$((\exists xB)\to A)\iff (\forall x(B\to A))$
$((\forall xB)\to A)\iff (\exists x(B\to A))$
$(A\to (Qx))\iff (Qx(A\to
Je bloque toujours sur le même problème (a priori pourtant simple d'après le livre).
Si deux formules $F$ et $G$ ne diffèrent que par le nom des variables qui y sont liées, comment montre-t-on que $\vdash F \Leftrightarrow G$, mais sans utiliser le théorème de complétude.
Dans le même ordre d'idée, il est dit dans la méthode de Herbrand, que toute formule peut se ramener à une formule $F$ de la forme $F=\forall v_{1}\exists v_{2}..\forall v_{2k-1}\exists v_{2k}B[v_{1},v_{2},...,v_{2k-1},v_{2k}]$, en ajoutant des quantificateurs portant sur des variables libres qui n'apparaissent pas dans $F$ et en montrant que la formule obtenue est syntaxiquement équivalente à celle dont on est parti. J'ai du mal avec ce passage. Part-on d'une formule déjà sous forme prénexe ou quelconque ? Et si l'on part d'une formule quelconque, comment prouve-t-on qu'elle est syntaxiquement équivalente à une forme prénexe (toujours sans utiliser le théorème de complétude, mais avec une démonstration formelle) ?
Auriez-vous des pistes à me suggérer ?
Par avance merci.
Cette histoire de Herbrand me parait fausse citée comme ça. Exemple: $\forall x\forall y : R(x,y)$. Comment tu fais sauter un quelque soit?
Dans l'esprit elle est vraie, mais "au sens figuré" en ajoutant des "conforts". Par exemple: $\forall x\forall y : R(x,y)$ peut s'écrire
$$ \forall (x,y) : R(x,y)$$
ce que tu me demandes de démontrer est un axiome, non ? Si $y$ est une variable qui n'apparaît pas dans $R$, $\forall x R(x) \rightarrow R_{y/x}$.
Je ne sais pas ce que que Christophe cherche à te faire démontrer. Peut-être que dans sa tête il part d'un autre système d'axiomes, dont ce truc est une conséquence.
Je vais tenter de prouver les autres lemmes.
j'ai prouvé les lemmes 16 et 18 1)
Je sèche sur le lemme 17 : Soient $F$ et $G$ des formules, $x$ une variable, montrer que : $\vdash \forall x (F\Rightarrow G)\Rightarrow (\forall x F \Rightarrow \forall x G)$.
comment prouve-t-on le lemme 17, ainsi que la proposition 17 ? Auriez-vous un ouvrage à me conseiller ou des pistes à me donner ?
Merci d'avance.
supposons $\forall x(A_x\to B_x)$ ainsi que $\forall xA_x$. Prouvons que $B_y$.
On a supposé $(A_y\to B_y)$ et $A_y$. Donc $B_y$.
Ca te donne $\forall x(A_x\to B_x) + \forall xA_x\vdash B_y$
Finalement $\forall x(A_x\to B_x) + \forall xA_x\vdash \forall yB_y$ (la variable $y$ n'est pas contrainte dans les hypothèses, on l'a choisie pour)
$\exists v F \Leftrightarrow \neg \forall v \neg F$
$\forall v (F\Rightarrow G)\Rightarrow (F\Rightarrow \forall v G)$, où $v$ est une variable sans occurrence libre dans $F$
$\forall v F \Rightarrow F_{t/v}$, où aucune occurrence libre de $v$ ne se trouve sous le champ d'un quantificateur liant une variable du terme $t$.
Par exemple, pour démontrer le lemme 18 1), j'ai écrit :
\begin{align*}
&\forall v (F \Rightarrow G)\Rightarrow (F \Rightarrow \forall v G)&\text{(axiome b)}
\end{align*}
\begin{align*}
&\forall v ((F \Rightarrow \forall v G)\Rightarrow (F \Rightarrow G))\Rightarrow ((F \Rightarrow \forall v G)\Rightarrow \forall v (F \Rightarrow G))&\text{(axiome b)}\\
&\forall v G \Rightarrow G&\text{(axiome c)}\\
&(\forall v G \Rightarrow G)\Rightarrow ((F \Rightarrow \forall v G)\Rightarrow (F \Rightarrow G))&\text{(tautologie)}\\
&(F \Rightarrow \forall v G)\Rightarrow (F \Rightarrow G)&\text{(par modus ponens)}\\
&\forall v ((F \Rightarrow \forall v G)\Rightarrow (F \Rightarrow G))&\text{(généralisation)}\\
&(F \Rightarrow \forall v G)\Rightarrow \forall v (F \Rightarrow G)&\text{(axiome b)}\\
\end{align*}
Je m'y prends peut-être très mal. Par ailleurs, pour la proposition 17, peut-on faire un raisonnement par récurrence en supposant que toute formule ayant au plus $n$ quantificateurs est syntaxiquement équivalente à une forme prénexe ?
Ne t'inquiète surtout pas et ne le fais pas.
1/ Logique combinatoire
2/ Lambda-calcul (les bases)
Et les relations entre les deux. Attention, ne perds pas ton temps sur le typage qui n'a rien à voir.
Si tu peux faire ça, tu n'auras plus jamais aucun problème avec ce sujet. En fait, la transformation d'une preuve naturelle (ou séquents) en preuve hilbertienne (modus ponens comme seule règle+axiomes) est très exactement le passage de "terme du lambda calcul" en "terme de la logique combinatoire" (sans variables).
L'algorithme est automatique. Là, ce que tu essaiyais de faire, ce serait comme écrire un terme de la logique combinatoire directement au pied levé. Même moi qui ai des centaines d'heures de vol en caml et obsessionnettes sur ces amusettes je ne suis pas capable de le faire. Quand j'ai envie, je reprogramme l'algo (10mn) et je rentre mon terme du lambda calcul et caml me sort le terme LC.
Ce n'est pas un sujet difficile, ni nécessitant de bases, faut juste s'y mettre.
On aimerait bien que oui (y compris votre serviteur, et alors exit ces problèmes de variables liées) mais stricto sensu, non (mais il y a une application $\theta$ de l'ensemble des formules du premier ordre vers le lambda calcul/ la logique du premier ordre typés et dans le deuxième cas pour que cette application se comporte bien il faut des propriétés supplémentaires sur $\lambda$, par exemple $\lambda x (A[y:=t])=(\lambda x A)[y:=t]$ quand $x\neq y$ et $t$ ne contient pas $x$, ce qui va dépendre de l'implémentation de "$\lambda$". Le bon comportement de $\theta$ s'établit au moyen de résultats de confluence voire du théorème de forte normalisation des termes typables).
D'autres approches existent: indices de Bruijn, liaisons graphiques à la Bourbaki/Quine.
Le lambda calcul et la logique combinatoire sont abordés dans le très bon livre de "Lambda-Calculus and combinators, an introduction" de R.Hindley et J.P.Seldin.