Théorème de Herbrand

Soit F une formule universelle (ou un ensemble de telles formules), par exemple ${\displaystyle \forall x,\forall y,P(x,y)}$ où P est un prédicat, et soit a₁, …, a_n, … une suite de termes. Considérons les trois propriétés suivantes :

1. F est cohérente, c’est‐à‐dire qu’on ne peut pas déduire une contradiction de l'hypothèse F ; autrement dit, ¬F 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 ${\displaystyle \not \vdash \lnot F}$ ;
2. F est satisfiable, c’est‐à‐dire qu’il existe un modèle dans lequel F est vraie, ce qu'on note ${\displaystyle \not \vDash \lnot F}$ ;
3. Pour tout entier n, la formule ${\displaystyle \bigwedge _{1\leqslant i,j\leqslant n}P(a_{i},a_{j})}$ est satisfiable, ce qu’on note ${\displaystyle \not \vDash \lnot Q(a_{1},...,a_{n})}$ où Q(a₁, …, a_n) 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 a_i 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 G = ¬F et R = ¬Q, on obtient l’équivalence des trois propriétés suivantes :

1. G est prouvable, c’est‐à‐dire qu’il existe une démonstration de G dans un système de déduction du calcul propositionnel, ce qu'on note ${\displaystyle \vdash G}$ ;
2. G est valide, c’est‐à‐dire que G est vraie dans tout modèle, ce qu'on note ${\displaystyle \vDash G}$ ;
3. Il existe un entier n pour lequel R(a₁, …, a_n) est valide, ce qu’on note ${\displaystyle \vDash R(a_{1},...,a_{n})}$.

G est alors un théorème.

Si la formule du calcul des prédicats F n'est pas satisfiable (c’est‐à‐dire si G est un théorème), alors en vérifiant Q(a₁, …, a_n) pour n=1, puis n=2, etc., on finira par trouver un entier n tel que la formule propositionnelle Q(a₁, …, a_n) ne soit pas satisfiable, et réciproquement.

Par contre, si F est satisfiable (si G n'est pas un théorème), alors pour tout n la proposition Q(a₁, …, a_n) sera satisfiable et le processus de calcul ne se terminera pas, sauf dans le cas particulier où les termes a_i 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.

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 ${\displaystyle F=\forall x,P(x)\land \lnot P(a)}$, où a est une constante. Le domaine de Herbrand est constitué du singleton ${\displaystyle \{a\}}$. On forme alors la formule ${\displaystyle Q_{1}=P(a)\land \lnot P(a)}$ qui est fausse, donc F est réfutable (sa négation est prouvable).

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

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

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

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

${\displaystyle \lnot (\exists x,\forall y,P(x,y))\lor (\forall z,\exists t,P(t,z))}$

${\displaystyle (\forall x,\exists y,\lnot P(x,y))\lor (\forall z,\exists t,P(t,z))}$

${\displaystyle \forall x,\exists y,\forall z,\exists t,\lnot P(x,y)\lor P(t,z)}$

La formule prénexe F équivalente à ¬G est :

${\displaystyle \exists x,\forall y,\exists z,\forall t,P(x,y)\land \lnot P(t,z)}$

dont la forme skolémisée est :

${\displaystyle \forall y,\forall t,P(a,y)\land \lnot P(t,f(y))}$

La formation des formules Q₁ en prenant pour (y, t) le couple (a, a) puis de Q₂ en prenant (y, t) = (f(a), a) conduit à ${\displaystyle P(a,a)\land \lnot P(a,f(a))\land P(a,f(a))\land \lnot P(a,f(f(a)))}$ qui est fausse dans tout modèle. F est réfutable et G est un théorème.

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

${\displaystyle \forall x,\exists y,\forall z,\exists t,P(x,y)\land \lnot P(t,z)}$

dont la forme skolémisée est :

${\displaystyle \forall x,\forall z,P(x,f(x))\land \lnot P(g(x,z),z)}$

Elle est satisfiable en donnant la valeur vraie à tout P(u, f(u)) et fausse à tout P(g(u, v), v), où u et v décrivent le domaine de Herbrand ${\displaystyle \{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 Q₁, Q₂… ne se termine pas. F est satisfiable et donc G 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.

• Élimination des quantificateurs

• Portail de la logique
• Portail des mathématiques