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
175 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
 
 
 
 
 

Équivalence syntaxique

Envoyé par Raskolnikov 
Équivalence syntaxique
23 avril 2021, 07:59
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 B))$ et $((A\rightarrow B)\land (B\rightarrow A))\rightarrow (A\leftrightarrow B)$, 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.



Modifié 1 fois. Dernière modification le 23/04/2021 12:01 par AD.
Re: Equivalence syntaxique
23 avril 2021, 09:07
Tu ne dois pas être surpris que les démonstrations formelles soient longues, c'est à peu près inévitable.

C'est pour ça qu'on n'en fait pas sauf quand on les considère comme objets d'étude grinning smiley

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Equivalence syntaxique
23 avril 2021, 09:34
Merci pour votre réponse.
Re: Équivalence syntaxique
23 avril 2021, 17:04
Tu peux te restreindre au signe "implique" (je vais le noter $\to$) et appliquer les vérités suivantes:

$((\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 B))$ et ce pour chaque $Q\in \{\forall; \exists \}$

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Équivalence syntaxique
27 avril 2021, 16:53
Bonjour et merci pour votre aide.
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.
Re: Équivalence syntaxique
27 avril 2021, 17:24
Prouve que $(\forall xR(x)) \to R(y)$ toi-même, ça te donnera le chemin général.

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)$$

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Équivalence syntaxique
28 avril 2021, 08:01
Bonjour,
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}$.
Re: Équivalence syntaxique
28 avril 2021, 10:22
@Raskolnikov : c'est un peu comme ça que je vois les choses aussi. D'après Cori/Lascar, ce truc est l'un des 3 schémas d'axiomes spécifiques, ou axiomes des quantificateurs.

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.
Re: Équivalence syntaxique
28 avril 2021, 13:42
Non, c'est bien ça. Du coup, tu ne devrais plus avoir de problème?

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Équivalence syntaxique
28 avril 2021, 14:26
J'ai fini par trouver un cours qui traite ces questions, mais les démonstrations n'y sont pas. Effectivement, avec cet axiome (et un autre) on prouve le lemme 16.
Je vais tenter de prouver les autres lemmes.


Re: Équivalence syntaxique
29 avril 2021, 10:12
Bonjour,

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)$.
Re: Équivalence syntaxique
30 avril 2021, 09:26
Bonjour,
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.
Re: Équivalence syntaxique
30 avril 2021, 10:50
Comme suit:

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)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Équivalence syntaxique
30 avril 2021, 10:51
Il est important que tu restes "naturel". La formalisation robotique totale n'est qu'une "légère traduction finale".

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Équivalence syntaxique
30 avril 2021, 11:33
Merci pour ton aide, mais comment écrire cette preuve en utilisant uniquement des tautologies, le modus ponens, la règle de généralisation, ainsi que les trois axiomes suivants :
$\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 ?



Modifié 1 fois. Dernière modification le 30/04/2021 11:34 par Raskolnikov.
Re: Équivalence syntaxique
30 avril 2021, 11:41
Je te ferai un exposé sur les systèmes à la Hilbert. Mais je te rassure personne n'est capable au pied levé de traduire des preuves naturelles ou à séquents en preuves hilbertiennes en moins de plusieurs heures, car ça constitue le nec plus ultra de la torture mentale.

Ne t'inquiète surtout pas et ne le fais pas.

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



Modifié 1 fois. Dernière modification le 30/04/2021 12:33 par christophe c.
Re: Équivalence syntaxique
30 avril 2021, 11:56
Merci beaucoup.
Re: Équivalence syntaxique
30 avril 2021, 12:32
Sinon, à toutes fins utiles, si tu as du temps (j'ignore ton contexte), tu peux acquérir les notions de:

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Équivalence syntaxique
30 avril 2021, 13:45
Merci pour ces explications. Pour l'instant, dès que j'ai un peu de temps (c'est le cas en ce moment), je lis le livre de Cori-Lascar. Je crois qu'il ne traite pas du lambda-calcul.
Re: Équivalence syntaxique
30 avril 2021, 15:09
Une formule logique (du premier ordre ici) est-elle un terme du lambda calcul/ de la logique combinatoire?

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.



Modifié 2 fois. Dernière modification le 30/04/2021 15:11 par Foys.
Re: Équivalence syntaxique
30 avril 2021, 15:13
J'essaierai de faire un pdf concis à l'occasion. C'est un sujet qui s'est développé en tant que sujet de recherche, donc peu soucieux de ménager ses lecteurs occasionnels.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
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: 151 364, Messages: 1 538 731, Utilisateurs: 28 272.
Notre dernier utilisateur inscrit omarprepa.


Ce forum
Discussions: 2 616, Messages: 53 300.

 

 
©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