Theoreme de Herbrand

Théorème de Herbrand

En logique, le théorème de Herbrand établit un lien entre calcul des prédicats et calcul des propositions. Alors qu'il est possible de déterminer de manière certaine si une proposition du calcul des propositions est démontrable ou pas, la question équivalente pour une formule du calcul des prédicats est plus délicate. Le théorème de Herbrand répond partiellement à cette question, bien qu'on sache depuis les travaux de Gödel, Tarski, Church, Turing et autres, qu'il n'existe pas d'algorithme permettant de décider si une formule générale du calcul des prédicats est prouvable ou non.

Formules prénexes

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 est équivalente à une formule prénexe. Par exemple, la formule $(\exists x \;P(x)) \to (\exists y \;Q(y))$ est équivalente successivement à $\lnot(\exists x \;P(x)) \lor (\exists y \;Q(y))$, $\forall x \;\lnot P(x) \lor \exists y \;Q(y)$, et enfin $\forall x \;\exists y\; \lnot P(x) \lor Q(y)$ (où $\to, \lnot, \lor, \land$ désignent respectivement l'implication, la négation, la disjonction, la conjonction. P et Q sont des prédicats unaires).

Une formule prénexe est universelle si elle ne possède que des quantificateurs universels $\forall$. Il est possible d'associer à une formule quelconque une formule universelle en lui appliquant une transformation de Skolem, consistant à introduire de nouveaux symboles de fonctions pour chaque quantificateur existentiel $\exists$. Par exemple, la forme skolémisée de $\forall x \;\exists y\; (\lnot P(x) \lor Q(y))$ est $\forall x \;\lnot P(x) \lor 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 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

Considérons alors une formule F universelle (ou un ensemble de formules), par exemple du type $\forall x, \forall y, P(x,y)$, où P est un prédicat, et soit un ensemble de variables a₁,a₂,...,a_n,.... Considérons les trois propriétés :

1. F est consistante, i.e on ne peut déduire une contradiction de l'hypothèse F. Ou encore $\lnot 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 : $\not\vdash \lnot F$.
2. F est satisfiable, i.e. il existe un modèle dans lequel F est vraie, ce qu'on note : $\not\vDash \lnot F$.
3. Pour tout entier n, il existe un modèle dans lequel la proposition suivante que nous noterons Q(a₁,...,a_n) est vraie :

$P(a_1,a_1) \land P(a_1,a_2) \land P(a_2,a_1) \land P(a_2,a_2) \land \cdots P(a_1,a_n) \land \cdots P(a_{n-1},a_n) \land P(a_n,a_1) \land \cdots P(a_n,a_n)$ ce qu'on note : pour tout n, $\not\vDash \lnot Q(a_1, ..., a_n)$

Le théorème de complétude de Gödel énonce l'équivalence entre 1) et 2). Par ailleurs, 2) entraîne 3), le modèle dans lequel 2) est vérifié permettant d'en déduire des modèles vérifiant 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 universels ont disparu et que les formules à prouver deviennent alors de simples propositions du calcul propositionnel.

De manière duale, en posant $G = \lnot F$ et $R = \lnot Q$, on obtient les équivalences entre les trois propriétés :

1. G est prouvable, i.e il existe une démonstration de G dans un système de déduction du calcul propositionnel. ce qu'on note : $\vdash G$.
2. G est valide, i.e. G est vraie dans tout modèle, ce qu'on note : $\vDash G$.
3. Il existe un entier n pour lequel R(a₁,...,a_n) est valide : $\vDash R(a_1, ..., a_n)$

G est alors un théorème.

Si F n'est pas satisfiable (ce qui se produit si et seulement si $G = \lnot F$ est un théorème), alors en vérifiant Q(a₁,...,a_n) pour n = 1, puis n = 2, etc., on finira par tomber sur un entier n tel que Q(a₁,...,a_n) est fausse, et réciproquement.

Par contre, si F est satisfiable (et donc si G n'est pas un théorème), alors pour tout n, Q(a₁,...,a_n) sera vraie, et le processus de calcul ne se terminera pas, sauf dans le cas particulier où les variables a_i sont en nombre fini.

Cela illustre le fait que l'ensemble des formules non satisfiables ou l'ensemble des théorèmes sont des ensembles 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 : considérons la formule $F = \forall x, P(x) \land \lnot P(a)$, où a est une constante. Le domaine de Herbrand est constitué du singleton {a}. On forme alors la formule $Q_1 = P(a) \land \lnot P(a)$ qui est fausse, donc F n'est pas satisfiable.

Exemple 2 : On considère la formule $F = \forall x,(P(x) \lor Q(x)) \land \lnot P(a) \land \lnot Q(b)$. Le domaine de Herbrand est {a,b}. On forme alors $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 à Q(a), puis on forme $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 à {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 $F = \forall x, \forall y, P(x) \land \lnot P(f(y))$. Le domaine de Herbrand est constitué de {a,f(a),f²(a),...,fⁿ(a),...}. On forme alors $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 $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 $P(f(a)) \land \lnot P(f(a))$. Donc F ne possède pas de modèle.

Exemple 4 : On considère la formule $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 :

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

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

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

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

La formule prénexe F équivalente à $\lnot G$ est :

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

dont la forme skolémisée est :

$\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 Q₂ en prenant (y,t) = (f(a),a) conduit à $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 n'est donc pas satisfiable et G est un théorème.

Exemple 5 : On considère la formule $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 : $\exists x, \forall y, \exists z, \forall t, \lnot P(x,y) \lor P(t,z)$. La formule prénexe F équivalente à $\lnot G$ est :

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

dont la forme skolémisée est :

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

Elle est satisfiable en donnant la valeur vrai à tout P(u,f(u)) et faux à tout P(g(u,v),v), où u et v 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 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.

Ce document provient de « Th%C3%A9or%C3%A8me de Herbrand ».