Théorème de Herbrand

Modèle:À sourcer Modèle:Confusion En logique, le théorème de Herbrand, publié en 1930 par Jacques Herbrand, établit un lien entre la logique du premier ordre et la logique propositionnelle (qui peut-être vu comme la logique d'ordre zéro). La validité (ou prouvabilité) d’une formule du premier ordre se ramène à la validité (ou prouvabilité) d'un ensemble fini de formules propositionnelles.

Alors qu'il est possible de déterminer algorithmiquement si une formule propositionnelle est démontrable ou pas, on sait — depuis les travaux de Gödel, Tarski, Church, Turing et autres — que la même question pour les formules du premier ordre est indécidable. Le théorème de Herbrand montre qu’elle est cependant semi-décidable : bien qu’il n’existe pas d’algorithme qui détermine si une formule donnée est prouvable ou pas, il existe une procédure qui résout partiellement la question en répondant « oui » si et seulement si la formule donnée est prouvable (pour certaines formules non prouvables, le calcul ne s'arrête pas).

Formules prénexes et formules universelles

Une formule du calcul des prédicats est prénexe si tous les quantificateurs qu'elle contient se trouvent au début de la formule. Toute formule admet une formule prénexe équivalente. Par exemple, la formule $(\mathrm{\exists }xP(x))\to (\mathrm{\exists }yQ(y))$ est équivalente successivement à $\mathrm{\neg }(\mathrm{\exists }xP(x))\vee (\mathrm{\exists }yQ(y))$, $(\mathrm{\forall }x\mathrm{\neg }P(x))\vee (\mathrm{\exists }yQ(y))$, et enfin $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\neg }P(x)\vee Q(y)$ (où $\to$, $\mathrm{\neg }$, $\vee$, $\mathrm{\exists }$, $\mathrm{\forall }$ désignent respectivement l'implication, la négation, la disjonction, le quantificateur existentiel et le quantificateur universel, et $P$ et $Q$ sont des prédicats unaires).

Une formule prénexe est universelle si elle ne possède que des quantificateurs universels (symbole $\mathrm{\forall }$). Il est possible d'associer à une formule quelconque une formule universelle en appliquant une transformation appelée skolémisation. Elle consiste à introduire de nouveaux symboles de fonction pour chaque quantificateur existentiel (symbole $\mathrm{\exists }$). Par exemple, la forme skolémisée de $\mathrm{\forall }x\mathrm{\exists }y(\mathrm{\neg }P(x)\vee Q(y))$ est $\mathrm{\forall }x\mathrm{\neg }P(x)\vee Q(f(x))$. Intuitivement, si pour chaque $x$, il existe $y$ tel qu'une propriété $R(x,y)$ soit vérifiée, alors on peut introduire une fonction $f(x)=y$ telle que, pour tout $x$, $R(x,f(x))$ est vérifiée. On montre que la formule initiale admet un modèle si et seulement si sa forme skolémisée en admet un. Autrement dit, la formule initiale est satisfiable si et seulement si sa forme skolémisée l'est. De même, la formule initiale est insatisfiable si et seulement si sa forme skolémisée l'est, et donc, par complétude, la négation de la formule initiale est prouvable si et seulement si la négation de sa forme skolémisée l'est.

Le théorème de Herbrand

Soit Modèle:Mvar une formule universelle (ou un ensemble de telles formules), par exemple $\mathrm{\forall }x,\mathrm{\forall }y,P(x,y)$ où Modèle:Math est un prédicat, et soit Modèle:Math une suite de termes. Considérons les trois propriétés suivantes.

1. Modèle:Mvar est cohérente, c’est‐à‐dire qu’on ne peut pas déduire une contradiction de l'hypothèse Modèle:Mvar ; autrement dit, Modèle:Math n'est pas prouvable dans un système de déduction du calcul des prédicats — telle la déduction naturelle par exemple —, ce qu'on note $⊬\mathrm{\neg }F$.
2. Modèle:Mvar est satisfiable, c’est‐à‐dire qu’il existe un modèle dans lequel Modèle:Mvar est vraie, ce qu'on note $\models ̸\mathrm{\neg }F$.
3. Pour tout entier Modèle:Mvar, la formule $\underset{1⩽i,j⩽n}{\bigwedge }P(a_i,a_j)$ est satisfiable, ce qu’on note $\models ̸\mathrm{\neg }Q(a_1,...,a_n)$ où Modèle:Math est cette proposition.

Le théorème de complétude de Gödel énonce l'équivalence entre 1) et 2). Par ailleurs, 2) entraîne 3) car tout modèle qui vérifie 2) permet de déduire des modèles qui vérifient 3). Le théorème de Herbrand énonce que, réciproquement, 3) entraîne 2) lorsque les Modèle:Math décrivent un domaine particulier, le domaine de Herbrand. On constate que, dans la formulation de 3), les quantificateurs ont disparu dans les formules à satisfaire, et que les formules à prouver sont alors de simples propositions du calcul propositionnel.

De manière duale, en posant Modèle:Math et Modèle:Math, on obtient l’équivalence des trois propriétés suivantes.

1. Modèle:Mvar est prouvable, c’est‐à‐dire qu’il existe une démonstration de Modèle:Mvar dans un système de déduction du calcul propositionnel, ce qu'on note $⊢G$.
2. Modèle:Mvar est valide, c’est‐à‐dire que Modèle:Mvar est vraie dans tout modèle, ce qu'on note $\models G$.
3. Il existe un entier Modèle:Mvar pour lequel Modèle:Math est valide, ce qu’on note $\models R(a_1,...,a_n)$.

Modèle:Mvar est alors un théorème.

Si la formule du calcul des prédicats Modèle:Mvar n'est pas satisfiable (c’est‐à‐dire si Modèle:Mvar est un théorème), alors en vérifiant Modèle:Math pour Modèle:Math, puis Modèle:Math, etc., on finira par trouver un entier Modèle:Mvar tel que la formule propositionnelle Modèle:Math ne soit pas satisfiable, et réciproquement.

Par contre, si Modèle:Mvar est satisfiable (si Modèle:Mvar n'est pas un théorème), alors pour tout Modèle:Mvar la proposition Modèle:Math sera satisfiable et le processus de calcul ne se terminera pas, sauf dans le cas particulier où les termes Modèle:Math sont en nombre fini.

Cela illustre le fait que l'ensemble des formules non satisfiables et l'ensemble des théorèmes sont récursivement énumérables, mais que le calcul des prédicats n'est pas décidable.

Exemples

Le domaine de Herbrand du modèle est défini au moins par un élément constant (afin d'être non vide) et est constitué de tous les termes que l'on peut former à partir des constantes et des fonctions utilisées dans les formules considérées. On définit un modèle de Herbrand en attribuant la valeur vraie à certains prédicats définis sur ces termes.

Exemple 1 : On considère la formule $F=\mathrm{\forall }x,P(x)\wedge \mathrm{\neg }P(a)$, où Modèle:Mvar est une constante. Le domaine de Herbrand est constitué du singleton $\{a\}$. On forme alors la formule $Q_1=P(a)\wedge \mathrm{\neg }P(a)$ qui est fausse, donc Modèle:Mvar est réfutable (sa négation est prouvable).

Exemple 2 : On considère la formule $F=\mathrm{\forall }x,(P(x)\vee Q(x))\wedge \mathrm{\neg }P(a)\wedge \mathrm{\neg }Q(b)$. Le domaine de Herbrand est $\{a,b\}$. On forme alors $Q_1=(P(a)\vee Q(a))\wedge \mathrm{\neg }P(a)\wedge \mathrm{\neg }Q(b)$ qui est vraie dans un modèle où l'on donne la valeur vraie à $Q(a)$, puis on forme $Q_2=Q_1\wedge (P(b)\vee Q(b))\wedge \mathrm{\neg }P(a)\wedge \mathrm{\neg }Q(b)$ qui est vraie dans un modèle où l'on donne la valeur vraie à $\{Q(a),P(b)\}$. Ayant épuisé le domaine de Herbrand, le calcul se termine et Modèle:Mvar est satisfiable dans le modèle précédemment défini.

Exemple 3 : On considère la formule $F=\mathrm{\forall }x,\mathrm{\forall }y,P(x)\wedge \mathrm{\neg }P(f(y))$. Le domaine de Herbrand est constitué de $\{a,f(a),f^2(a),...,f^n(a),...\}$. On forme alors $Q_1=P(a)\wedge \mathrm{\neg }P(f(a))$ qui possède un modèle en attribuant la valeur vraie à Modèle:Math mais fausse à Modèle:Math. Puis, en prenant les deux premiers éléments du domaine Modèle:Mvar et Modèle:Mvar(Modèle:Mvar), on forme $Q_2=P(a)\wedge \mathrm{\neg }P(f(a))\wedge P(a)\wedge \mathrm{\neg }P(f(f(a)))\wedge P(f(a))\wedge \mathrm{\neg }P(f(a))\wedge P(f(a))\wedge \mathrm{\neg }P(f(f(a)))$ qui ne peut posséder de modèle à cause de la conjonction fausse $P(f(a))\wedge \mathrm{\neg }P(f(a))$. Donc Modèle:Mvar ne possède pas de modèle. F est réfutable et sa négation est prouvable.

Exemple 4 : On considère la formule $G=(\mathrm{\exists }x,\mathrm{\forall }y,P(x,y))\to (\mathrm{\forall }y,\mathrm{\exists }x,P(x,y))$ dont on veut montrer qu'il s'agit d'un théorème. Après avoir renommé les variables Modèle:Mvar et Modèle:Mvar dans la deuxième partie de Modèle:Mvar afin d'éviter d'avoir des variables liées de même nom, on obtient une forme prénexe équivalente à Modèle:Mvar :

$(\mathrm{\exists }x,\mathrm{\forall }y,P(x,y))\to (\mathrm{\forall }z,\mathrm{\exists }t,P(t,z))$

$\mathrm{\neg }(\mathrm{\exists }x,\mathrm{\forall }y,P(x,y))\vee (\mathrm{\forall }z,\mathrm{\exists }t,P(t,z))$

$(\mathrm{\forall }x,\mathrm{\exists }y,\mathrm{\neg }P(x,y))\vee (\mathrm{\forall }z,\mathrm{\exists }t,P(t,z))$

$\mathrm{\forall }x,\mathrm{\exists }y,\mathrm{\forall }z,\mathrm{\exists }t,\mathrm{\neg }P(x,y)\vee P(t,z)$

La formule prénexe Modèle:Mvar équivalente à Modèle:Math est :

$\mathrm{\exists }x,\mathrm{\forall }y,\mathrm{\exists }z,\mathrm{\forall }t,P(x,y)\wedge \mathrm{\neg }P(t,z)$

dont la forme skolémisée est :

$\mathrm{\forall }y,\mathrm{\forall }t,P(a,y)\wedge \mathrm{\neg }P(t,f(y))$

La formation des formules Modèle:Math en prenant pour Modèle:Math le couple Modèle:Math puis de Modèle:Math en prenant Modèle:Math conduit à $P(a,a)\wedge \mathrm{\neg }P(a,f(a))\wedge P(a,f(a))\wedge \mathrm{\neg }P(a,f(f(a)))$ qui est fausse dans tout modèle. Modèle:Mvar est réfutable et Modèle:Mvar est un théorème.

Exemple 5 : On considère la formule $G=(\mathrm{\forall }x,\mathrm{\exists }y,P(x,y))\to (\mathrm{\exists }y,\mathrm{\forall }x,P(x,y))$. Par un procédé comparable à l'exemple précédent, on obtient pour forme prénexe équivalente à Modèle:Mvar : $\mathrm{\exists }x,\mathrm{\forall }y,\mathrm{\exists }z,\mathrm{\forall }t,\mathrm{\neg }P(x,y)\vee P(t,z)$. La formule prénexe Modèle:Mvar équivalente à $\mathrm{\neg }G$ est :

$\mathrm{\forall }x,\mathrm{\exists }y,\mathrm{\forall }z,\mathrm{\exists }t,P(x,y)\wedge \mathrm{\neg }P(t,z)$

dont la forme skolémisée est :

$\mathrm{\forall }x,\mathrm{\forall }z,P(x,f(x))\wedge \mathrm{\neg }P(g(x,z),z)$

Elle est satisfiable en donnant la valeur vraie à tout Modèle:Math et fausse à tout Modèle:Math, où Modèle:Mvar et Modèle:Mvar décrivent le domaine de Herbrand $\{a,f(a),g(a,a),f(f(a)),f(g(a,a)),g(a,f(a)),...\}$, et en donnant une valeur arbitraire aux autres prédicats. Cependant, le calcul successif des formules correspondantes Modèle:Math, Modèle:Math… ne se termine pas. Modèle:Mvar est satisfiable et donc Modèle:Mvar n'est pas un théorème, mais la démarche précédente ne permet pas de le montrer par un calcul en un nombre fini d'étapes.

Voir aussi

• Élimination des quantificateurs