Preuves syntaxiques du théorème de Herbrand et de la déskolémisation (sans égalité).

Foys · 22 Apr

Ces résultats ont la réputation injustifiée de dépendre de l'axiome du choix ou même du théorème de complétude. Dans le présent fil on montre comment les déduire du théorème d'élimination des coupures du calcul des séquents de la logique du premier ordre (prérequis de ce fil; voir des ouvrages de théorie de la démonstration. Tout ce qui suit est algorithmique même s'il y a des problèmes de complexité et que les fichiers produits peuvent être énormes).

On ne traite ci-dessous que le cas sans égalité (le cas égalitaire est plus compliqué).

Dans toute la suite on fixe un langage du premier ordre $\mathcal L$.

Dans un premier temps on montre le

I) Théorème de Herbrand:

Soit $P$ une formule à $n$ variables libres $x_1,....,x_n$ sans quantificateurs sur $\mathcal L$. On appelle instance de $\exists x_1 \exists x_2 ... \exists x_n P$ une formule de la forme $P[x_1:= t_1, ... , x_n:= t_n]$ où $t_i$ est un terme du langage $\mathcal L$pour tout $i$.

Le résultat est alors le suivant:

Si $\exists x_1 \exists x_2 ... \exists x_n P$ est démontrable en logique classique du premier ordre alors il existe des instances $A_1,...,A_r$ de $P$ telles que $A_1 \vee ... \vee A_r$ est démontrable en logique propositionnelle (i.e. aucun quantificateur ni aucune règle relative aux quantificateurs n'est utilisée nulle part dans la preuve).

Preuve:
On appelle "instance partielle de $\exists x_1 \exists x_2 ... \exists x_n P$" toute formule de la forme $\exists x_{k+1} \exists x_{k+2} ... \exists x_n P [x_1:= s_1, ... x_k:= s_k]$ où $s_1,s_2,...,s_k$ sont des termes du langage $\mathcal L$. Les instances partielles sans quantificateur sont ce que nous avons appelé "instances" plus haut.

Ci-dessous on dit qu'une preuve (dans le calcul des séquents LK et sans coupure) est "bonne"

lorsque:

(i) les seules formules de $\pi$ qui contiennent des quantificateurs sont des instances partielles de $\exists x_1 \exists x_2 ... \exists x_n P$,
(ii) de telles instances apparaissent à droite des séquents de la preuve, jamais à gauche.

On considère une preuve sans coupure $\pi$ de $\exists x_1 \exists x_2 ... \exists x_n P$ (théorème d'élimination des coupures) dans le calcul des séquents LK. Alors par récurrence sur la longueur de $\pi$ on montre aisément que $\pi$ est "bonne".

D'autre part soit $\theta$ une "bonne preuve". Alors il existe une preuve $\theta'$ ayant le même arbre non décoré que $\theta'$, où aucune règle d'introduction de quantificateur n'est employée et dans laquelle toutes les instances partielles de $\exists x_1 \exists x_2 ... \exists x_n P$ sont remplacées par des listes d'instances sans quantificateurs de $\exists x_1 \exists x_2 ... \exists x_n P$.
(A nouveau ceci est évident par récurrence sur la longueur de $\theta$: regarder les seuls moment où des règles de quantificateurs peuvent être employées dans $\theta$).

En appliquant ce qui précède à $\pi$ on obient une preuve d'un séquent $\vdash A_1, ... , A_r$ sans règle d'introduction de quantificateurs, avec $A_i$ qui est une instance de $\exists x_1 \exists x_2 ... \exists x_n P$ pour tout $i$. Le résultat visé suit immédiatement par application de $r-1$ règles d'introduction à droite de $\vee$

Dans un message ultérieur j'expliquerai comment déduire de ce résultat la "déskolémisation" (qui entraîne que si $(\forall x R(x, f(x))) \Rightarrow S$ est prouvable alors $(\forall x \exists y R(x, y)) \Rightarrow S$ l'est aussi, lorsque $f$ est un symbole de fonction qui n'apparaît ni dans $R$ ni dans $S$)

Cyrano · 22 Apr

Dans ton dernier paragraphe, qu'en est-il si on est uniquement intéressé par le bloc $\forall x R (x,f(x))$ sans l'implication qui suit ?

Foys · 22 Apr

Ce sera traité dans mon paragraphe tout en un qui suit. Il n'y a pas de théorème de Herbrand pour des formules commençant uniquement par des quantificateurs universels sauf si bien sûr elles sont niées puisqu'alors ça devient des formules existentielles déguisées; en fait l'idée est pour des formules prénexes générales -puisqu'on peut toujours se ramener à ce cas - de remplacer toutes les variables issues de quantifications universelles par des symboles de fonction. On applique alors le théorème de Herbrand sous la forme ci-dessus à une nouvelle formule. Ledit remplacement est licite via un résultat un peu long à rédiger qui généralise la skolémisation.

Foys · 22 Apr

Je précise pour les lecteurs impatients que ces résultats sont traités sur un exemple à la page 54 du livre "Mathematical logic" de Joseph Shoenfield (avec une méthode différente basée sur la complétion à la Henkin des théories du premier ordre mais tout de même également algorithmique et de nombreux résultats préliminaires référencés aux pages précédentes dudit livre).

Cyrano · 22 Apr

Une question me taraude dans ce cas. Tu sembles affirmer deux choses :

1) On peut toujours se ramener à des formules sans quantificateurs, traitables par la logique propositionnelle classique.
2) On est pas obligé d'utiliser l'axiome du choix. Autrement dit ce processus est tout à fait "constructible".

Mais alors dans ce cas, pourquoi le calcul des prédicats n'est-il pas décidable ?

Lirone93 · 22 Apr

C'est beau.

Foys · 22 Apr

Cyrano a dit :

Une question me taraude dans ce cas. Tu sembles affirmer deux choses :

1) On peut toujours se ramener à des formules sans quantificateurs, traitables par la logique propositionnelle classique.
2) On est pas obligé d'utiliser l'axiome du choix. Autrement dit ce processus est tout à fait "constructible".

Mais alors dans ce cas, pourquoi le calcul des prédicats n'est-il pas décidable ?

Parce que si la formule à laquelle le procédé est appliqué n'est pas prouvable, il va falloir tester une infinité de disjonctions différentes sans jamais savoir si le programme qui fait ce test s'arrête.
En fait étant donné n'importe quelle formule du 1er ordre $\Phi$ il existe des programmes informatiques agressifs qui trouvent infailliblement une preuve de ladite formule si elle existe et qui bouclent indéfiniment sinon (pour le plus inefficace mais le plus simple à comprendre: pour n entier démarrant à zéro, écrire toutes les preuves de logique à n caractères dans l'ordre alphabétique puis renvoyer ladite preuve si celle-ci se termine par $\Phi$ sinon continuer).

Et comme on ne sait pas décider si un programme (en particulier un comme celui-ci) s'arrête, on n'a rien résolu.

Foys · 23 Apr

Ci-dessous on déduit du théorème précédent un résultat d'élimination des symboles de fonctions pour des formules prénexes quelconques.

Soit $H$ une formule du premier ordre sans quantificateurs sur $\mathcal L$, dont les variables libres appartiennent à la liste de lettres deux à deux distinctes $\left [\left (x_j^i \right)_{1 \leq j \leq p_i}; \left (y_j^i \right)_{1 \leq j \leq q_i} \right]_{1\leq i \leq n}$

Soit $\left [ \left ( f_j^i \right)_{1\leq j \leq q_i}\right]_{1 \leq i \leq n}$ une famille de symboles de fonctions distincts n'apparaissant pas dans $\mathcal L$ et tels que pour tout $i\in \{1,...,n\}$ et tout $j\in \{1,...,q_i\}$, $f^i_j$ soit d'arité $\sum_{k=1}^i p_k$ (l'arité est le nombre d'arguments d'un symbole de fonction). Soit $\mathcal L'$ le langage obtenu en ajoutant ces symboles de fonction à $\mathcal L$. On définit deux formules:

$$\begin{align}A:= & \exists x_1^1 \exists x_2^1 ... \exists x_{p_1}^1 \forall y_1^1 \forall y_2^1... \forall y_{q_1}^1 ... \exists x_1^n \exists x_2^n ... \exists x_{p_n}^n \forall y_1^n \forall y_2^n... \forall y_{q_n}^n H \\
B:= & \exists x_1^1 \exists x_2^1 ... \exists x_{p_1}^1... \exists x_1^n \exists x_2^n ... \exists x_{p_n}^n H\left [y_j^i := f^i_j (x_1^1,x_2^1 ... x_{p_1}^1,...,x_1^i,x_2^i...,x_{p_i}^i); 1 \leq i \leq n; 1 \leq j \leq q_i \right ] \end{align}$$

II) Théorème d'élimination des symboles de fonction:

$A$ est démontrable (dans le langage $\mathcal L$) si et seulement si $B$ l'est (dans le langage $\mathcal L'$).

######################################

Démontrable veut bien sûr dire ici "en logique classique du premier ordre" (ou ce qui revient au même: en calcul des séquents LK sans coupures).
Le sens $\Longrightarrow$ est trivial par induction sur $n$ ($B$ est en fait un cas particulier de $A$).
On traite le sens non trivial et intéressant $\Longleftarrow$ ci-dessous.

On applique le théorème de Herbrand à $B$: On pose $K:= H\left [y_j^i := f^i_j (x_1^1,x_2^1 ... x_{p_1}^1,...,x_1^i,x_2^i...,x_{p_i}^i); 1 \leq i \leq n; 1 \leq j \leq q_i \right ]$. Il existe des instances $C_1,...C_r$ de $K$ telles que $C_1 \vee ... \vee C_r$ est un théorème propositionnel. En fait d'après la fin de la preuve du théorème de Herbrand ci-dessus, on peut même supposer qu'on a une preuve $\pi$ propositionnelle (aucun quantificateur n'y apparaît nulle part) et sans coupure du séquent $\vdash C_1,...,C_r$.

0°) Noter que pour tout $k\in \{1,...,r\}$, $C_k$ est de la forme $$H\left [x_h^i:= t_h^i; y_j^i := f^i_j (t_1^1,t_2^1 ... t_{p_1}^1,...,t_1^i,t_2^i...,t_{p_i}^i); 1 \leq i \leq n; 1\leq h \leq p_i; 1 \leq j \leq q_i \right ]$$ où les $\left (t_j^i \right)_{1\leq i \leq n; 1\leq j \leq p_i}$ sont des termes du langage $\mathcal L'$.

L'idée clé: remplacer dans la preuve $\pi$ toutes les occurrences de termes de la forme $f^i_j(...)$ par des variables (ce qui n'altère pas le caractère de preuve de $\pi$ puisqu'elle ne contient aucun quantificateur), de façon à appliquer ultérieurement des règles d'introduction de $\forall$ à droite pour retrouver une preuve de $A$.

Celarevient à traiter les termes introduits par des nouveaux symboles de fonction comme si c'était de nouvelles variables; Il n'est pas évident a priori que ce soit possible. On donne le détail de cette construction ci-dessous.

1°) soit $g$ un symbole de fonction d'arité $k$ dans $\mathcal L$, $b_1,...,b_k$ des termes et $a$ une lettre.
On définit par induction pour tout terme $T$ de $\mathcal L'$, $T \langle g(b_1,...,b_k):= a\rangle$ de la façon suivante:
(i) si $T$ est une lettre ou une constante, si $T = g(b_1,...,b_k)$ (ce qui n'arrive que si $k=0$ et $T=g$) alors $T \langle g(b_1,...,b_k):= a \rangle := a$; sinon $T \langle g(b_1,...,b_k):= a \rangle := T$

(ii) si $T$ est de la forme $h(U_1,...,U_m)$ et si $h=g$, $k=r$ et $U_i = b_i$ pour tout $i$ (bref $T = g(b_1,...,b_k)$) alors $T \langle g(b_1,...,b_k):= a \rangle := a$, sinon $T \langle g(b_1,...,b_k):= a \rangle := h \left ( U_1 \langle g(b_1,...,b_k):= a \rangle, ..., U_r \langle g(b_1,...,b_k):= a \rangle \right)$

2°) On étend la définition précédente à toutes les formules propositionnelles (qu'on suppose écrites avec les seuls connecteurs $\vee, \neg$ pour aller plus vite) en posant:
$R(T_1,...T_m) \langle g(b_1,...,b_k):= a \rangle := R\left (T \langle g(b_1,...,b_k):= a \rangle, ..., T_m \langle g(b_1,...,b_k):= a \rangle \right)$ pour tout symbole de prédicat $R$ et tous termes $T_1,...,T_m$, et pour toutes formules $F,G$ on pose $(F \vee G) \langle g(b_1,...,b_k):= a \rangle:= \left (F \langle g(b_1,...,b_k):= a \rangle \right) \vee \left (G \langle g(b_1,...,b_k):= a \rangle \right)$ et $(\neg F) \langle g(b_1,...,b_k):= a \rangle := \neg \left (F \langle g(b_1,...,b_k):= a \rangle \right )$.

3°) Pour toute preuve propositionnelle (dans laquelle aucun quantificateur n'apparaît) $\theta$ on note $\theta \langle g(b_1,...,b_k):= a \rangle$ l'arbre décoré obtenu en remplaçant toutes les formules $F$ de $\theta$ par $F \langle g(b_1,...,b_k):= a \rangle$. Alors $\theta \langle g(b_1,...,b_k):= a \rangle$ est encore une preuve propositionnelle (évident par induction sur la longueur de la preuve).

4°) Soit $\mathcal L''$ un second langage étendant strictement $\mathcal L$ et tel que $g \in \mathcal L'' \backslash \mathcal L $. on garde les notations de 1°) On suppose que $v_1,...,v_d$ sont des termes de $\mathcal L''$ et que $T$ est un terme de $\mathcal L$ dont les variables libres sont parmi $x_1,...,x_d$. Alors $\left (T[x_i:= v_i; 1 \leq i \leq d] \right ) \langle g(b_1,...,b_k):= a \rangle = T \left [x_i:= v_i \langle g(b_1,...,b_k):= a \rangle; 1 \leq i \leq d \right ]$
Preuve: évident par induction sur la taille du terme; en effet dans la définition 1°) la seule situation qui peut poser problème est celle où $T$ est de la forme $g(\_)$, ce qui n'est jamais le cas puisqu'on a supposé que $T$ est un terme de $\mathcal L$ et que $g\notin \mathcal L$.

5°) Désormais on qualifiera de "pur" un terme qui ne contient aucune occurrence des symboles de fonctions $(f^i_j)_{1\leq i \leq n; 1 \leq j \leq q_i}$ rajoutés à $\mathcal L$ en préambule. Bien sûr les termes de $\mathcal L$ sont eux-mêmes purs mais il y en aura d'autres. On définit une suite par récurrence en posant $\mathcal L_0:= \mathcal L'$ et $\mathcal L_{m+1}:= $ le langage obtenu en ajoutant à $\mathcal L_m$, pour tout $i\leq n$, tout $j \leq q_i$, et (en posant $r:= \sum_{k=1}^i p_k$) tout $r$-uplet $\vec a = (a_1,..,a_r)$ de termes purs de $\mathcal L_m$, une nouvelle lettre $\gamma^i_{j, \vec a}$ qui ne figurait pas dans $\mathcal L_m$, de telles nouvelles lettres étant deux à deux distinctes. On pose alors $\mathcal L_{\infty}:= \bigcup_{m=0}^{+\infty} \mathcal L_m$

6°) On dit qu'une famille $\left ( \left (t^i_j \right)_{1\leq j \leq p_i}; \left (e^i_j \right) _{1 \leq j \leq q_i}\right )_{1 \leq i \leq n}$ de termes de $\mathcal L_{\infty}$ est convenable si pour tout $i\in \{1,...,n\}$ et tout $j\in \{1,...,q_i\}$, l'un des deux cas suivants se produit:
(i): $e^i_j = f^i_j (t^1_1,...,t^1_{p_1}, ... ,t^i_1, ..., t^i_{p_i})$
(ii) $e^i_j = \gamma^i_{j; t^1_1,...,t^1_{p_1}, ... ,t^i_1, ..., t^i_{p_i}}$ et de plus pour tout $k\leq i$ et tout $\ell \leq p_k$, le terme $t^k_{\ell}$ est pur.

7°) Soient $\left ( \left (t^i_j \right)_{1\leq j \leq p_i}; \left (e^i_j \right) _{1 \leq j \leq q_i}\right )_{1 \leq i \leq n}$ une famille convenable, $k\leq n$, $\ell \leq q_k$, $\vec b:=\left ( b^1_1, ..., b^1_{p_k}, ... b^k_1, ... b^k_{p_k}\right)$ un uplet de termes tous purs. Alors $\left ( \left (t^i_j \langle f^k_{\ell} (\vec b) := \gamma^k_{\ell; \vec b}\rangle \right)_{1\leq j \leq p_i}; \left (e^i_j \langle f^k_{\ell} (\vec b) := \gamma^k_{\ell; \vec b}\rangle \right) _{1 \leq j \leq q_i}\right )_{1 \leq i \leq n} $ est encore une famille convenable.

Preuve: regarder quel est le terme le plus à gauche de la liste qui peut être modifié de façon non triviale par la substitution de terme $\langle f^k_{\ell} (\vec b) := \gamma^k_{\ell; \vec b}\rangle$ et distinguer les cas où c'est un

$t^i_j$ et celui où c'est un $e^i_j$ (dans cette deuxième circonstance on sera nécessairement dans la situation (ii) de 6° ci-dessus).

8°) Etant donnée une liste de formules $F_1,...,F_m$, s'il y a au moins une occurrence d'un des symboles de fonctions $f^i_j$, il y a également au moins une occurrence dans $F_1,....,F_m$ d'un terme de la forme $f^k_{\ell} (\vec b)$, où $\vec b$ est un uplet de termes purs. En effet il suffit de prendre pour cela une occurrence de terme commançant par l'un des $f^i_j$ dans $F_1,...,F_m$ et qui a le nombre de caractères le plus petit possible.

9°) On dit désormais qu'une formule $F$ (et non une suite de termes) est convenable s'il existe une famille convenable $\left ( \left (t^i_j \right)_{1\leq j \leq p_i}; \left (e^i_j \right) _{1 \leq j \leq q_i}\right )_{1 \leq i \leq n}$(cf 6°) telle que $F = H\left [x_h^i:= t_h^i; y_j^i := e^i_j; 1 \leq i \leq n; 1\leq h \leq p_i; 1 \leq j \leq q_i \right ]$.
Compte tenu de la remarque 0°) plus haut, toutes les formules $C_1,...,C_r$ du préambule (issues de l'application du théorème de Herbrand) sont convenables.

10°) Etant donnés une formule convenable $F$, $k\leq n$, et $\ell \leq q_k$, $\vec b:=\left ( b^1_1, ..., b^1_{p_k}, ... b^k_1, ... b^k_{p_k}\right)$ un uplet de termes tous purs, $F \langle f^k_{\ell} (\vec b) := \gamma^k_{\ell; \vec b}\rangle $. C'est une conséquence immédiate de 7°) et de 4°) (appliqué à $\mathcal L'':= \mathcal L_{\infty}$) puisque $F$ est obtenue en substituant des termes à $H$ qui est une formule de $\mathcal L$ d'après 9°).

11°) En utilisant 10°) plusieurs fois sur $C_1,...,C_r$ on produit une suite de suite de formules convenables dont le nombre d'occurrences de symboles $f_j^i$ diminue strictement. Tant qu'il y en a encore au moins un on applique 8°) pour trouver un uplet de termes purs convenables. Chaque nouvelle suite de formules convenables constitue un séquent prouvable propositionnellement (cf 3°). Ainsi:

12°) Il existe un séquent $\vdash D_1,... , D_r$ ayant une preuve propositionnelle, et tel que pour tout $i$, $D_i$ est une formule convenable sans aucune occurrence d'un des symboles de fonctions $(f^i_j)_{1 \leq i \leq n; 1 \leq j \leq q_i}$
C'est à partir de ce séquent qu'on construit une preuve de $A$ du préambule, en alternant règles à droite de contraction, introduction de $\forall$, e intriduction de $\exists$. Pour cela il suffit de constater que:

13°) Soient $\left ( \left (t^i_j \right)_{1\leq j \leq p_i}; \left (e^i_j \right) _{1 \leq j \leq q_i}\right )_{1 \leq i \leq n}$ et $\left ( \left (t'^i_j \right)_{1\leq j \leq p_i}; \left (e'^i_j \right) _{1 \leq j \leq q_i}\right )_{1 \leq i \leq n}$ deux suites convenables dans lesquelles il n'y a aucun nouveau symbole de fonction $(f^i_j)_{1 \leq i \leq n; 1 \leq j \leq q_i}$ (autrement dit chaque $e^i_j$ est de la forme $\gamma^i_{j; \vec b}$ avec $b = (t^1_1,...,t^i_{p_i})$). Soit $k\leq n$; on suppose qu'il existe $\ell \in \{1,...,q_k\}$ tel que $e^k_{\ell} = e'^k_{\ell}$ (*).
Alors pour tous $i\leq k$, $j \leq p_k$ et $h \leq q_k$ on a $t^i_j = t'^i_j$ et $e^i_h = e'^i_h$ (regarder ce qu'implique (*) au vu de la définition de famille convenable, sachant qu'on est toujours dans le cas (ii) de 6°).

14°) On conclut avec 13°) et 12°).

samok · 23 Apr

Tu as employé le signe $=$ entre deux termes, j'arrête de lire ces inepties

Foys · 23 Apr

Lol @samok par "sans égalité" il faut bien comprendre que cela fait référence aux règles du système de preuves étudié et ne concerne pas le méta-discours.

On va maintenant régler le cas de $F:= (\forall \vec x (R(\vec x,f(\vec x))) \Rightarrow S$ prouvable qui entraîne $G:= (\forall \vec x \exists y(R(\vec x,y )) \Rightarrow S$ prouvable ($f$ n'apparaissant ni dans $R$, ni dans $S$). $\vec x$ est un uplet de la forme $x_1,...,x_d$ et "$\forall \vec x$" abrège évidemment $\forall x_1 \forall x_2 ... \forall x_d$.

Dans ce qui suit on pose $\tilde {\exists}:= \forall$ et $\tilde{\forall}:= \exists$.

On suppose sans perte de généralité $R$ et $S$ prénexes, autrement dit respectivement de la forme $Q^1 z_1 Q^2 z_2 ... Q^m z_m R'$ et $Q^{m+1} z_{m+1} Q^{m+2} z_{m+2} ... Q^n z_n S'$ avec $Q^1, Q^2, ... Q^n \in \{\forall, \exists\}$, les lettres $z_1,z_2, ..., z_n$ toutes distinctes (quitte à alpha-renommer les formules) et différentes de $x_1,...,x_d,y$ et enfin $R'$ et $S'$ sans quantificateurs.

On pose $\begin{align} F':= & \exists x_1 \exists x_2 ... \exists x_d \tilde {Q^1} z_1 \tilde {Q^1} z_2 ... \tilde {Q^m} z_m Q^{m+1} z_{m+1} Q^{m+2} z_{m+2} ... Q^n z_n \left (R'[y:= f(x_1,...,x_n)] \Rightarrow S' \right )\\ G := & \exists x_1 \exists x_2 ... \exists x_d \forall y \tilde {Q^1} z_1 \tilde {Q^1} z_2 ... \tilde {Q^m} z_m Q^{m+1} z_{m+1} Q^{m+2} z_{m+2} ... Q^n z_n \left (R'\Rightarrow S' \right )\end{align}$

Il est clair que $F$ équivaut à $F$, $G$ équivaut à $G'$ et enfin, que $F'$ et $G'$ sont prénexes.

Le résultat visé découle immédiatement de mon long message précédent et du fait que les transformées de Herbrand de $F'$ et de $G'$ sont identiques, au renommage près des nouveaux symboles de fonctions introduits (pour $G'$ il suffit de prendre $f$ pour le premier d'entre eux).

La "transformée de Herbrand" d'une formule prénexe $\exists x^1_1 ... \exists x^1_{p_1} \forall y_1^1...\forall y_{q_1}^1 ... \exists x^n_1 ... \exists x^n_{p_n} \forall y_n^1...\forall y_{q_n}^n H $ n'est rien d'autre que la formule sans quantificateurs universels mais avec nouveaux symboles de fonctions à la place introduite dans mon message précédent, c'est-à-dire $\exists x^1_1 ... \exists x^1_{p_1} ... \exists x^n_1 ... \exists x^n_{p_n} H[y^i_j:= f^i_j (x_1^1 ... x^i_{p_i}); 1 \leq i \leq n, 1 \leq j \leq q_i] $.

Preuves syntaxiques du théorème de Herbrand et de la déskolémisation (sans égalité).

Réponses

Bonjour!

Catégories

In this Discussion