Previous Next Contents

5  Propriétés méta-mathématiques

La logique du premier a de nombreuses propriétés logiques intéressantes, et la plupart peuvent être approchées soit du point de vue sémantique, au moyen d'interprétations (la théorie des modèles), soit du point de vue syntaxique, au moyen d'arguments portant sur les preuves, disons en LK (la théorie de la preuve).



5.1  Formes prénexes et de Skolem

Notre but en démonstration automatique est de découvrir si des formules sont valides (resp. prouvables). Cependant, avant de chercher des preuves, il est commode de simplifier les formules à prouver. Étant donnée une formule du premier ordre F, nous voulons calculer une formule F' plus simple (en un sens à préciser) dont la validité (resp. la prouvabilité) soit équivalente à celle de F.


Définition 7  [Prénexe]  Une formule est dite prénexe si et seulement si elle est de la forme Q1 x1·... Qn xn·F, où Q1, ..., Qn sont des quantificateurs et F est sans quantificateur.


Que F soit sans quantificateur signifie qu'elle a été construite sans utiliser de quantifications. Autrement dit, F est en fait une formule propositionnelle où les atomes jouent le rôle de variables propositionnelles.


Théorème 8   Pour toute formule du premier ordre F, il existe une formule prénexe F', calculable à partir de F, telle que F et F' sont (sémantiquement, resp. prouvablement) équivalentes.
Preuve : Exercice : l'idée est de pousser les quantificateurs vers l'extérieur par des règles comme ¬" x·Y¾® $ x·¬Y ou YÙ(" x·Y')¾® " x'· YÙY'[x'/x], où x'Ïfv(Y). La terminaison du processus est obtenu par exemple par l'utilisation d'un ordre récursif sur les chemins (rpo). Si vous avez bien conçu vos règles de transformation, alors l'équivalence sémantique devrait être évidente, alors que l'équivalence pour la prouvabilité devrait être aussi simple, quoique pénible à démontrer formellement. ¤

Le théorème 8 montre qu'au lieu de travailler avec une formule arbitraire, nous pouvons nous restreindre aux formules prénexes, qui ont une structure plus précise. Nous pouvons encore simplifier, grâce à l'idée suivante.

Soit une formule de la forme, par exemple, " x·F : elle est valide si et seulement si pour tout x, F est vraie. Remplaçons x par une nouvelle constante c dans F. Alors " x· F est valide si et seulement si, pour toute interprétation de c, F[c/x] est vraie, autrement dit, si et seulement si F[c/x] est valide. En somme, nous pouvons coder la quantification universelle sur x par l'utilisation d'une constante c et la quantification universelle implicite sur toutes les interprétations dans la définition de la validité.

Maintenant considérons une formule de la forme $ x·" y·F : elle est valide si et seulement s'il existe une valeur pour x telle que pour tout y, F soit vraie. Un contre-exemple de la validité serait, pour chaque valeur donnée de x, une valeur de y telle que F ne serait pas vraie; en d'autres termes, un contre-exemple pour y est une application f(x), où f est un nouveau symbole de fonction, et pas seulement une constante c. Sans avoir à recourir à la notion de contre-exemple, nous pouvons dire que $ x·" y·F est valide si et seulement si $ x·F[f(x)/y] est valide, où la quantification universelle sur y est implicite, cachée dans la définition de la validité.

Formellement, ceci nous mène à :


Définition 9  Une formule existentielle est une formule de la forme $ x1·...$ xn·F, où F est sans quantificateur.

Une formule universelle est une formule de la forme " x1·..." xn·F, où F est sans quantificateur.


Ce qui suit est dû pour l'essentiel à Thoralf Skolem pour les formules universelles, mais Jacques Herbrand l'utilisait abondamment pour les formules existentielles :


Théorème 10  [Herbrand-Skolem]   Soit F une formule du premier ordre.

Il existe une formule existentielle F', calculable à partir de F, telle que F' est valide si et seulement si F est valide. Nous disons que F' est obtenue en herbrandisant F, et que F' est une forme de Herbrand de F.

De façon duale, il existe une formule universelle F'', calculable à partir de F, telle que F'' est insatisfiable si et seulement si F est insatisfiable. Nous disons que F'' est obtenue en skolémisant F, et que F'' est une forme de Skolem de F.
Preuve : Nous pouvons supposer que F est en forme prénexe, par le théorème 8. Nous traitons de la skolémisation, l'herbrandisation s'en déduisant en niant la forme de Skolem de la négation. (Et réciproquement.)

Soit donc F de la forme Q1 x1·... Qn xn·Y, où Y est sans quantificateur. Pour chaque 1£ i£ n tel que Qi est le quantificateur existentiel $, soit xi1, ..., ximi la liste des variables universellement quantifiées d'indices inférieurs à i, soit fi un nouveau symbole de fonction d'arité mi et ti le terme fi(xi1, ..., ximi). Alors, soit Y' la formule Y où toute variable existentiellement quantifiée xi est remplacée par ti, et F' la formule " xi1·..." xim·Y', où xi1, ..., xim sont les variables universellement quantifiées. (Autrement dit, nous remplaçons les variables existentielles par des fonctions nouvelles de toutes les variables universelles qui les précèdent. Dans le cas de l'herbrandisation, nous remplaçons les variables universelles par des fonctions nouvelles de toutes les variables existentielles les précédant.)

Nous affirmons que F est satisfiable si et seulement si F' l'est. Pour le prouver, nous montrons que tout énoncé " y1· ... " yk· $ z· F1 est satisfiable si et seulement si " y1· ... " yk· F1[f(y1, ..., yk)/z] est satisfiable, où f est un symbole de fonction qui n'apparaît pas dans F1. L'affirmation s'en déduit par récurrence sur le nombre de quantificateurs existentiels dans le préfixe de F.

Si " y1· ... " yk· F1[f(y1, ..., yk)/z] est satisfiable, alors il y a un modèle I, et une interprétation de f dans I, tels que F1[f(y1, ..., yk)/z] est vraie pout toutes les affectations de valeurs v1, ..., vk aux variables y1, ..., yk respectivement. Alors I(f)(v1, ..., vk) est une valeur pour z qui rend F1 vraie dans I, pour toute affectation des yi, 1£ i £ k. Donc I satisfait " y1· ... " yk· $ z·F1.

Réciproquement, supposons qu'il existe une interprétation I satisfaisant " y1· ... " yk· $ z· F1. Pour toute affectation de valeurs v1 à y1, ..., vk à yk, soit G(v1, ..., vk) l'ensemble des valeurs de z qui rendent F1 vraie. Par hypothèse, G(v1, ..., vk) est non vide pour tout k-uplet de valeurs (v1, ..., vk). Nous utilisons maintenant l'axiome du choix pour en déduire qu'il existe une fonction g envoyant chaque (v1, ..., vk) vers un élément de G(v1, ..., vk). Étendons l'interprétation I en une nouvelle interprétation I' telle que I'(s)=I(s) pour tous les symboles dans F1, et telle que I'(f)=g, nous voyons alors que I' satisfait " y1· ... " yk· F1[f(y1, ..., yk)/z]. ¤

Note :Alors que la conversion en forme prénexe produit une formule logiquement équivalente, l'herbrandisation et la skolémisation ne le garantit pas. L'herbrandisation ne préserve que le statut de validité, et la skolémisation ne préserve que le statut de satisfiabilité.

En fait, l'herbrandisation préserve aussi le statut de prouvabilité, et la skolémisation le statut de cohérence de la formule, ce qui signifie que ce processus est justifié non seulement sémantiquement, mais aussi en ce qui concerne les preuves. Nous le montrerons en section 5.3.

On peut mieux herbrandiser/skolémiser si on évite de mettre la formule en forme prénexe. Définissons deux fonctions, une d'herbrandisation h et une de skolémisation s par [And86] : (Exercice : montrer que toute formule F, h (F) est valide si et seulement si F est valide, et que s (F) est satisfiable si et seulement si F est satisfiable. On peut même choisir le même symbole de Skolem f pour deux occurrences de formules quantifiées logiquement équivalentes.)



5.2  Théorie sémantique de Herbrand

Maintenant que nous avons restreint la classe des formules à considérer (pour la validité) aux formules existentielles, nous présentons quelques notions fondamentales, découvertes par Jacques Herbrand dans les années 30 :


Définition 11  [Univers de Herbrand]   Soit B un ensemble dit de constantes de base, tel que B¹Ø s'il n'y a pas de symbole de fonction 0-aire. Soit B0 le plus petit de ces B, autrement dit Ø s'il y a des symboles de fonction 0-aires, sinon {a} où a est une nouvelle constante.

L'ensemble des termes clos formés dans le langage étendu par l'ensemble B de constantes est appelé l'univers de Herbrand sur B. L'univers de Herbrand est H(B0).

Une interprétation de Herbrand I est un ensemble d'atomes clos dans le langage étendu par l'ensemble de constantes B. Elle définit une interprétation sur H par :


Les univers de Herbrand sont les interprétations les plus simples que nous puissions imaginer, étant donnée la syntaxe de la logique du premier ordre. En effet, ils consistent à interpréter les termes comme des termes clos, comme le lemme suivant le montre. La condition étrange sur la vacuité de B ou de B0 assure que H(B) est bien le domaine d'une interprétation, autrement dit, que H(B) est non vide.


Lemme 12   Soit r une affectation sur H(B). Alors r est une substitution close, et pour toute interprétation de Herbrand I, pour tout terme t, [t]Ir=tr.
Preuve : Remarquer que tr sur le côté droit signifie t auquel la substitution r a été appliquée. La preuve est par une récurrence structurelle immédiate sur t. ¤

En somme, sur les univers de Herbrand, les substitutions closes sont les affectations.

L'intérêt principal des univers et des interprétations de Herbrand tient aux théorèmes suivants. Le lemme suivant dit que les interprétations de Herbrand ne sont pas moins générales que les interprétations générales. C'est-à-dire que si la définition 11 montre que les interprétations de Herbrand définissent des interprétations sur H(B), le lemme suivant montre la réciproque :


Lemme 13   Soit I une interprétation sur un univers de Herbrand H(B). Alors il existe une interprétation de Herbrand I' sur H(B) telle que pour toute formule F et pour toute affectation r, [F]Ir=[F]I'r.
Preuve : Soit I' l'ensemble des atomes clos A tels que [A]Ir=T. Par définition, pour tout atome A --- pas nécessairement clos --- [A]I'r=[Ar]I'[] par le lemme 12, autrement dit [A]I'r=[Ar]I[] (par définition de I') =[A]Ir (par une récurrence facile sur les sous-termes de A). On en déduit le lemme par récurrence structurelle sur F. Nous venons d'en prouver le cas de base; les autres cas sont immédiats. ¤

À partir de maintenant, nous confondrons donc les deux notions d'interprétation sur H(B) et d'interprétation de Herbrand.

Ce qui suit montre que rien de plus que la syntaxe (les univers et interprétations de Herbrand) n'est nécessaire pour décider de la validité :


Théorème 14   Soit F une formule existentielle (une forme de Herbrand).

Les assertions suivantes sont équivalentes :
Preuve : (i) implique (ii), qui implique (iii). Il ne reste qu'à montrer que (iii) implique (i). Comme F est existentielle, elle a la forme $ x1· ...$ xn·Y, où Y est sans quantificateur. Par (iii), quelle que soit l'interprétation de Herbrand I, il existe des termes clos t1, ..., tn tels que Y[t1/x1, ..., tn/xn] soit vraie dans I, autrement dit il existe une instance close Ys de Y qui soit vraie dans I.

Maintenant, soit I' une interprétation arbitraire (pas nécessairement sur H(B0)) sur un domaine non vide arbitraire D. Cette interprétation induit une interprétation de Herbrand I sous forme de l'ensemble des atomes clos A tels que A soit vrai dans I'. Alors par (iii), il existe une instance close Ys de Y qui soit vraie dans I, donc dans I'. (L'argument est similaire à celui du lemme 13.) Ainsi l'affectation qui envoie chaque xi vers l'interprétation du terme clos xis dans D satisfait Y. Donc I' satisfait $ x1· ...$ xn·Y, c'est-à-dire F. Comme I' est arbitraire, (i) est prouvée. ¤

Ce théorème a comme conséquence le résultat important qui suit :


Théorème 15  [Herbrand, version sémantique]   Soit F une formule existentielle $ x1· ...$ xn·Y, où Y est sans quantificateur. Supposons de plus qu'il y a au moins une constante dans le langage.

Alors F est valide si et seulement s'il existe un entier k, et k instances closes Ys1, ..., Ysk de Y telles que Ys1Ú...ÚYsk soit propositionnellement valide.
Preuve : Si Ys1Ú...ÚYsk est propositionnellement valide, alors F est clairement valide, puisque dans toute interprétation, une des formules Ysi, 1£ i£ k doit être valide.

Réciproquement, si F est valide, par le théorème 14, pour toute interprétation de Herbrand I sur H(B0), il y a une instance close YsI satisfaite par I. (Remarquer que puisqu'il y a au moins une constante dans le langage, B0 est vide, et H(B0) est exactement l'ensemble des termes clos.) En particulier, l'ensemble de tous les ¬YsI est propositionnellement insatisfiable, et nous affirmons qu'il existe alors un sous-ensemble fini insatisfiable ¬Ys1, ..., ¬Ysk de l'ensemble des ¬YsI : on en conclut que Ys1Ú...ÚYsk est propositionnellement valide.

Nous prouvons l'affirmation en montrant que, de tout ensemble G (propositionnellement) insatisfiable d'atomes clos, on peut extraire un sous-ensemble fini D qui est aussi insatisfiable. Construisons un arbre de décision binaire comme dans le cas propositionnel, à ceci près que ses noeuds sont étiquetés par les atomes clos, et comme il peut y en avoir un nombre infini, ses branches peuvent être infinies. Les branches d'un tel arbre de Herbrand sont juste les interprétations de Herbrand. Maintenant, sur chaque branche I, il existe un atome clos AI dans G (autrement dit, un noeud sur I) qui est rendu faux par I, et nous pouvons définir AI comme le plus haut de ces noeuds sur la branche. Élaguons chaque branche I juste en-dessous de AI. Nous obtenons un arbre, appelé l'arbre clos T, dont les branches sont toutes finies. Par le lemme de König (une conséquence de l'axiome du choix, qui énonce que tout arbre dont tout noeud n'a qu'un nombre fini de fils, et dont toutes les branches sont finies, est fini), T est fini. Comme les AI sont des noeuds dans T, l'ensemble D de tous les AI est fini. De plus, il est insatisfiable par construction. (Le résultat est en fait juste même quand G est n'importe quel ensemble de formules propositionnelles, et pas seulement des atomes : c'est le théorème de compacité de la logique propositionnelle classique. Exercice : prouvez-le, en remarquant que toute formule propositionnelle ne contient qu'un nombre fini d'atomes.) ¤

Le thèorème de Herbrand est important parce qu'il fournit une procédure pour tester si une formule donnée est valide : herbrandiser la formule en une formule existentielle F, puis énumérer toutes les suites d'instances closes Ys1, ..., Ysk et tester si leur disjonction est propositionnellement valide. Ceci peut ne pas terminer, car nous ne connaissons pas de borne a priori sur k, mais au moins si la formule est valide, nous finirons par le découvrir par ce moyen. (Nous disons que ce processus est complet. Il est clairement correct, autrement dit il ne peut déclarer valide aucune formule invalide.) Cette méthode a été explorée jusqu'au début des années 1960, où des façons plus efficaces d'utiliser le théorème de Herbrand ont été conçues. Ces méthodes formeront le sujet des chapitres à venir.

Le théorème de Herbrand est en général présenté sous sa forme duale :


Théorème 16  [Herbrand, dual]   Soit F une formule universelle " x1· ..." xn·Y, où Y est sans quantificateur. Supposons de plus qu'il y ait au moins une constante dans le langage.

Alors F est insatisfiable si et seulement s'il existe un entier k, et k instances closes Ys1, ..., Ysk de Y telles que Ys1 Ù ... Ù Ysk soit propositionnellement insatisfiable.


Une composante mystérieuse de ce théorème est qu'il a besoin d'un entier k, alors qu'on imaginerait volontiers k=1. En d'autres termes, nous pourrions nous attendre à ce que $ x·Y soit valide si et seulement s'il existait un terme t tel que Y[t/x] soit valide. Un tel terme t s'il existe est appelé un témoin de la formule existentielle $ x·Y, et est une représentation sous forme de terme d'une valeur v telle que Y[v/x] est vraie. Ceci est le cas en logique intuitionniste, mais en logique classique toutes les valeurs ne sont pas représentables par des termes. Par exemple, $ x· P(a)Ù P(b)Þ P(x) est valide en classique, et une valeur v pour x serait a si P(a) est vraie, et b sinon, autrement dit nous pourrions choisir ``si P(a) alors a sinon b'' comme témoin ... mais ce n'est pas un terme du premier ordre ! Nous venons de comprendre un peu mieux ce que dit le théorème de Herbrand : $ x·Y est valide si et seulement si nous pouvons trouver des témoins pour x sous la forme de programmes si-alors-sinon finis qui retournent des termes.

Le théorème de Herbrand entraîne immédiatement :


Théorème 17  [Énumérabilité récursive]   L'ensemble des énoncés du premier ordre valides est récursivement énumérable. Autrement dit, il existe une procédure qui énumère tous les énoncés valides du premier ordre, et eux seulement.


Toutes les propriétés récursives P de formules (autrement dit, les propriétés décidables, celles qui peuvent être vérifiées par un algorithme qui termine) sont récursivement énumérables : énumérer toutes les formules, et vérifier si P est vraie pour chaque. Cependant, il existe des propriétés récursivement énumérables qui ne sont pas récursives, et malheureusement la validité au premier ordre n'est pas décidable :


Théorème 18  [Indécidabilité]   Il n'existe pas d'algorithme terminant qui, étant donnée une formule du premier ordre F en entrée, retourne vrai si et seulement si F est classiquement valide.
Preuve : Comme nous n'avons pas donné de définition précise de calculable ou récursif (cf. [Joh92, DW85]), et comme ce n'est pas notre propos, nous montrons ce théorème par réduction à partir d'un problème indécidable plus commode, le problème de correspondance de Post (du nom du logicien Emil Post).

Soit A un alphabet fini, contenant au moins deux lettres distinctes. A* est l'ensemble de tous les mots (y compris le mot vide) sur A, c'est-à-dire de toutes les suites finies de lettres. Soit E une collection finie de couples (ui, vi), 1£ i£ n, que nous noterons ui = vi. Étant donnée une suite finie i1, i2, ..., ik d'indices entre 1 et n, nous pouvons former la concaténation ui1 ui2 ... uik, et aussi vi1 vi2 ... vik. Le problème de correspondance de Post est : étant donné E, y a-t-il une suite non vide comme ci-dessus telle que ui1 ui2 ... uik = vi1 vi2 ... vik ?

Se reporter à la figure 3 pour un exemple : nous nous y donnons quatre équations (à gauche de la figure), et avons indiqué une solution au problème de Post sur la droite.


Figure 3: Un exemple du problème de correspondance de Post
Le problème de Post est indécidable; voir [DW85]. Nous pouvons de plus supposer que E ne contient pas l'équation (e, e), où e est le mot vide, et que l'alphabet ne contient que deux lettres distinctes a et b.

Pour coder le problème de Post en logique du premier ordre, nous créons deux symboles de fonction unaires pour représenter les lettres, et les nommons encore a et b; nous créons aussi une constante e représentant le mot vide, et un symbole de prédicat binaire P représentant la convertibilité par les règles de Post. Nous codons les mots w, disons aj1 aj2 ... ajm, comme des termes de la forme ajm (... aj2 (aj1 (x)) ...), où aj1, ..., ajm sont des lettres et x est une variable; soit w(x) ce dernier terme. Nous écrivons aussi w au lieu de w(e). Nous pouvons alors axiomatiser le problème de Post comme suit : Soit maintenant C la conjonction de ces formules, et soit F la formule CÞ $ x · P(a(x), a(x)) Ú P(b(x), b(x)). Intuitivement, C dit que P(w,w') est vraie soit quand w = w' = e soit quand w = w1 ui et w' = w'1 vi pour un certain i et des termes w1, w'1 tels que P(w1, w'1). La formule F dit que l'on peut fabriquer un mot non vide (autrement dit un mot de la forme wa ou wb pour un certain mot w éventuellement vide) à partir de ces règles. Comme E ne contient pas (e, e), ceci est équivalent au problème de Post.

Par exemple (cf. figure 3), nous avons P(aababbaa, aababbaa) parce que P(e, e), donc P(aab, a) par l'équation (4), donc P(aaba, aabab) par l'équation (1), donc P(aabab, aababba) par l'équation (2), donc P(aababbaa, aababbaa) par l'équation (3).

Nous montrons maintenant que F est valide si et seulement si le problème de Post a une solution. D'abord, si l'on met F en forme prénexe, on obtient une formule existentielle. Donc si F est valide, le théorème de Herbrand s'applique, et donc nous pouvons prouver F en démontrant que la disjonction de ¬ P(e, e), d'un nombre fini d'instances closes d'axiomes niés :
P(wj, w'j) Ù ¬ P(u
 
ij
(wj), v
 
ij
(w'j))
avec 1£ j £ m et pour tout j, 1£ ij £ n; et d'un nombre fini d'instances de la conclusion :
P(a(vk), a(vk))
P(b(vk), b(vk))
où 1£ k£ p, est propositionnellement valide. De façon équivalent, l'ensemble de clauses :
P(e, e)
¬ P(wj, w'j) Ú P(u
 
ij
(wj), v
 
ij
(w'j))
¬ P(a(vk), a(vk))
¬ P(b(vk), b(vk))
où 1£ j £ m et 1£ k£ p, est propositionnellement insatisfiable. Par la complétude de la résolution propositionnelle, il existe une dérivation de la clause vide à partir des clauses ci-dessus. Nous disons que (w,w') est une paire de Post si et seulement si w = uj0 uj1 ... ujl et w' = vj0 vj1 ... vjl pour un certain l³ 0 et des indices j0, ..., jl entre 1 et n. Une récurrence aisée sur la longueur de la dérivation par résolution montre que les seules clauses non vides que nous pouvons dériver sont : On ne peut alors dériver la clause vide qu'en résolvant sur des clauses de l'une des deux dernières formes : ceci implique qu'il y a deux paires de Post (w1, w'1) et (w2, w'2) telles que w2 (w1 (e)) = w'2 (w'1 (e)), autrement dit telles que w1 w2 = w'1 w'2, et que ce dernier mot n'est pas vide. Donc si F est valide, le problème de Post a une solution.

Réciproquement, il est clair que si le problème de Post a une solution, la formule F est valide.

Nous en concluons que l'espèce de problèmes du premier ordre qui code les problèmes de Post est indécidable, donc la validité en logique du premier ordre en général est indécidable. (Bien sûr, ceci est vrai de la satisfiabilité également.) ¤

Ceci n'a pas découragé les chercheurs d'essayer de trouver des procédures efficaces de recherche de preuve. Le théorème 18 dit que tout procédure de recherche de preuve correcte et complète doit ne pas terminer sur au moins une formule en entrée; nous pouvons quand même utiliser une telle procédure, et l'interrompre quand elle prend trop de temps, auquel cas nous ne savons pas si la formule d'entrée était valide ou non. (Plus finement, cet échec est une indication que la formule d'entrée, si elle est valide, est d'autant plus difficile à prouver qu'elle résiste plus longtemps.) Un autre point de vue est de dire que toute procédure correcte et qui termine doit être incapable de trouver des preuves de certaines propositions valides. Tous ces compromis sont acceptables, aussi longtemps que nous nous efforçons de décider la classe la plus grande de propositions en temps raisonnable. Il est clair que la procédure d'énumération décrite dans la preuve du théorème 17 est l'une des plus inefficaces que l'on puisse concevoir, et nous en examinerons d'autres dans les chapitres suivants.

D'un point de vue logique, ou méta-mathématique, les constructions de Herbrand fournissent aussi les résultats suivants :


Théorème 19  [Compacité]   Si G|= F, alors il existe un sous-ensemble fini D de G tel que D|= F.
Preuve : Il suffit de montrer que si G n'a pas de modèle, alors il existe un sous-ensemble fini D de G qui n'en a pas non plus. Supposons que toutes les formules de G ont été skolémisées, sans perte de généralité. Si G n'a pas de modèle, il n'a pas de modèle de Herbrand sur B0, ce qui signifie que l'ensemble des instances closes des formules sans quantificateur Y, où " x1·..." xn·Y Î G, n'a pas de modèle, par le théorème 14, point (iii). Ce dernier ensemble est un ensemble propositionnellement insatisfiable de formules propositionnelles : par le théorème de compacité propositionnelle (voir la preuve du théorème 15), il existe un sous-ensemble fini insatisfiable E de ces formules. Nous pouvons alors choisir un sous-ensemble fini D de G tel que pour tout Y' dans E, Y' est une instance d'une formule Y telle que " x1·..." xn·Y Î D. ¤

Ce qui a pour conséquence :


Théorème 20  [Löwenheim-Skolem, faible]   Si F a un modèle, alors il a des modèles de n'importe quel cardinal infini.
Preuve : Si F a un modèle, alors elle a un modèle de Herbrand sur H(B) pour tout B, par le théorème 14. Si tous les symboles de fonction dans F sont d'arité 0, et si nous choisissons B de cardinal a³À0, le cardinal de H(B) est celui de F plus a, autrement dit a puisque le cardinal de F est inférieur ou égal à À0. Sinon, s'il existe un symbole de fonction non nullaire dans F, le cardinal de H(B) est a.À0, c'est-à-dire a puisque a est supérieur ou égal à À0. Comme a est un cardinal infini arbitraire, le théorème est prouvé. ¤

Mais nous avons triché : dans le modèle ci-dessus, nous avons introduit de nombreuses valeurs qui peuvent être en fait prouvablement égales (si nous avons un prédicat d'égalité). En fait, nous pouvons prouver le résultat surprenant suivant :


Théorème 21  [Löwenheim-Skolem]  Soit = un symbol de prédicat binaire. Nous disons d'un modèle qu'il est équationnel si et seulement si = est interprété comme la relation d'égalité dans ce modèle.

Alors, si F a un modèle équationnel infini, il a des modèles équationnels de n'importe quel cardinal infini.
Preuve : Supposons que F a un modèle équationnel infini. Autrement dit, il existe une interprétation I sur un domaine D qui satisfait F et tous les axiomes de l'égalité =, telle que le quotient de D par la relation d'équivalence I(=) est infini.

Soit b le cardinal de ce quotient, et soit a n'importe quel cardinal infini tel que a£ b. Créons a nouveaux symboles de contante ci, 0£ i<a et étendons l'interprétation I de sorte que chaque I(ci) soit dans une classe d'équivalence distincte pour I(=). Nous pouvons le faire, parce qu'il y a b³ a classes d'équivalence. Soit S l'ensemble des formules contenant F et toutes les inéquations ¬ ci= cj, i¹ j (vu comme une conjonction); S admet clairement I comme modèle équationnel. Mais alors I induit une interprétation de Herbrand I' sur H(B), où B=B0È{ci| 0£ i<a}, telle que I' satisfait S. En particulier, I' satisfait F, et comme I' satisfait toutes les ¬ ci= cj, i¹ j, son quotient par I'(=) a un cardinal d'au moins a. Ensuite, B est de cardinal a, donc H(B) est de cardinal au plus a.À0, c'est-à-dire exactement a. En particulier, H(B)/I'(=) est un modèle équationnel de F de cardinal a. Ceci démontre ce que nous appelons la version descendante du théorème, à savoir que si F a un modèle équationnel infini, alors il a des modèles équationnels infinis de tout cardinal plus petit.

Pour montrer la version ascendante, nous construisons un modèle équationnel de cardinal a>b en en construisant d'abord un de cardinal ba, puis en utilisant la version descendante pour redescendre à a. En effet, comme b³ 2, nous avons a£ ba. Définissons Da comme le produit de a copies distinctes de D (son cardinal est ba), et définissons une interprétation Ia sur Da par Ia(f)(v1,...,vn)= (I(f)(v1i,...,vni))0£ i<a (application point à point) et en posant Ia(P)(v1,...,vn) égal à la conjonction de tous les booléens I(P)(v1i,...,vni), 0£ i<a. Remarquons que Ia(=) est l'égalité sur Da.

Pour toute affectation r de variables vers Da, et pour tout 0£ i<a, soit ri l'affectation envoyant x vers la iième composante de r(x). Par une récurrence facile sur les formules, pour toute formule Y, nous avons Ù0£ i<a[Y]Iri £ [Y]Iar £Ú0£ i<a[Y]Iri, où Ù est la conjonction distribuée, Ú est la disjonction distribuée et £ est l'ordre défini sur les booléens par F£ T, F¹T. Mais lorsque Y=F, la conjonction et la disjonction valent toutes les deux T, donc [F]Iar = T, autrement dit Ia est bien un modèle (équationnel) de F.

(Une preuve plus simple mais moins constructive de la version ascendante est : étant donné un cardinal a, ajoutons a nouvelles constantes ci, 0£ i<a, et considérons l'ensemble des formules S={F}È{¬ ci= cj| i¹ j}. Si S n'avait pas de modèle équationnel, par compacité il y aurait un sous-ensemble incohérent fini de S; mais tout sous-ensemble fini de S peut être interprété en envoyant chaque ci du sous-ensemble fini vers des éléments distincts du modèle infini I. Donc S a un modèle équationnel, qui est de cardinal au moins a, et nous utilisons la version descendante pour en obtenir un de cardinal exactement a.) ¤

En particulier, nous ne pouvons pas espérer caractériser les entiers ou les réels en logique du premier ordre, même avec une infinité d'axiomes (par compacité, ceci ce ramène au cas d'un nombre fini d'axiomes, donc au cas d'une formule). Ceci est dû au fait que, quelle que soit l'axiomatisation au premier ordre que nous choisissions, il existera des modèles non dénombrables de l'arithmétique. Le problème est analogue avec les réels : toute axiomatisation au premier ordre des réels doit avoir des modèles dénombrables, bien que les réels ne soient pas dénombrables. (La théorie des corps réels clos, aussi appelée théorie du premier ordre des réels, a en particulier comme plus petit modèle l'ensemble des nombres algébriques.)



5.3  Élimination des coupures et théorie de Herbrand syntaxique

Tout ce que nous avons effectué dans les dernières sections peut aussi être fait dans un cadre purement syntaxique, en remplaçant les notions de validité et de satisfiabilité par les notions leur correspondant en théorie de la preuve, à savoir la prouvabilité et la cohérence. C'est plus dur à faire que dans l'approche sémantique, mais nous gagnerons des intuitions supplémentaires sur ce qui se passe réellement.

L'outil de base est le théorème d'élimination des coupures (théorème 24), c'est-à-dire le fait que nous puissions transformer toute preuve de LK en une preuve sans coupure (Cut). Pour le démontrer, nous avons d'abord besoin de quelques définitions et quelques lemmes. Nous considérons que les séquents sont des ensembles de formules, de sorte que les contractions, les affaiblissements et les échanges seront traités implicitement; le lecteur est prié de vérifier que ceci n'invalide pas nos arguments.


Définition 22  Dans une règle de LK : les séquents Gi¾®Di sont appelés les prémisses, et G¾®D est la conclusion de la règle.

Dans une coupure (règle Cut) : F est appelée la formule de coupure.

Dans toutes les règles, les formules actives (cf. figure 2) dans les prémisses sont F, F' dans les cas ÙL, ÙR, ÚL, ÚR, ÞL, ÞR; F dans les cas ¬L et ¬R; F[t/x] dans les cas "L et $R; F[y/x] dans les cas "R et $L; et F (la formule de coupure) dans le cas de Cut.

Dans toutes les règles, la formule principale dans la conclusion est F dans le cas de Ax, FÙF' dans les cas ÙL et ÙR; FÚF' dans les cas ÚL et ÚR; FÞF' dans les cas ÞL et ÞR; ¬F dans les cas ¬L et ¬R; " x·F dans les cas "L et "R; $ x·F dans les cas $L et $R.

Soit F une formule. La profondeur d(F) de F est définie par : d(A) = 0 si A est un atome, d(F Ú F') = 1 + max(d(F), d(F')) (et de même pour Ù, ¬, Þ), d(" x·F') = 1 + d(F') (et de même pour $).

Soit p une preuve dans LK, que nous voyons comme un arbre inversé de séquents.

La profondeur d(p) de p est la profondeur de l'arbre qui le représente, autrement dit la profondeur d'un axiome Ax est 0, et la profondeur d'une preuve se terminant sur une règle de prémisses les conclusions de preuves pi, 1£ i£ n, est 1+max(d(p1), ...,d(pn)).

Une coupure est dite maximale s'il s'agit d'une coupure entre deux preuves sans coupure. Le rang de coupure r(p) de p est défini comme étant 0 si p est sans coupure, sinon comme le maximum de d(p')+d(F), où p' parcourt toutes les sous-preuves de p se terminant sur une coupure maximale, de formule de coupure F.


Le rang de coupure est une mesure de la complexité de la preuve p. Le lemme qui suit montre que nous pouvons toujours faire décroître cette complexité, le prix en étant une éventuelle augmentation de la taille de la preuve :


Lemme 23  [Élimination des coupures, une étape]   Soit p une preuve dans LK de rang de coupure r non nul. Alors il existe une preuve dans LK de rang de coupure au plus r-1 du même séquent.
Preuve : Soit n le nombre de sous-preuves sans coupure p' de p qui se terminent sur une coupure (maximale), de formule de coupure F, telles que d(p')+d(F)=r, autrement dit de rang maximal. Par hypothèse, n¹ 0. p' est de la forme :



où p1 et p2 sont sans coupure. L'idée est de pousser les coupures vers le haut le long de p1 et p2, jusqu'à ce que la coupure ci-dessus de rang maximal soit éliminée, ne laissant ainsi que des coupures de rang inférieur. Plus formellement, nous montrons que nous pouvons transformer la preuve p en une preuve du même séquent, avec au plus n-1 sous-preuves de rang r et aucune de rang supérieur.

Pour ce faire, nous montrons que nous pouvons transformer p' en une preuve de rang au plus r-1. L'argument est par récurrence sur d(p1)+d(p2). Il y a deux cas : Nous en concluons que le lemme est valide, par récurrence sur le nombre n de coupures maximales de rang maximal. ¤


Théorème 24  [Élimination des coupures]   Un séquent G¾®D est prouvable dans LK si et seulement s'il est prouvable dans LK sans la règle de coupure Cut.
Preuve : Par récurrence sur le rang de coupure d'une preuve de G¾®D, en utilisant le lemme 23. ¤

La preuve dit même plus : de toute preuve de G ¾® D, nous pouvons extraire par calcul une preuve sans coupure du même séquent.

Les propriétés suivantes sont des conséquences immédiates :


Définition 25  [Sous-formules]  Soit F une formule de la logique du premier ordre. L'ensemble des sous-formules de F est le plus petit ensemble de formules tel que :


L'ensemble des sous-formules est en général infini, et beaucoup plus gros que l'ensemble des noeuds dans le graphe qui représente F : c'est parce que toute instance de F' est considérée comme une sous-formule de " x·F' ou de $ x·F'. L'idée est que nous pouvons reconnaître les sous-formules d'une formule donnée, par filtrage (``pattern-matching'' en anglais).


Corollaire 26  [Propriété de la sous-formule]   Dans une preuve sans coupure du séquent G¾®D, tous les séquents consistent uniquement en des sous-formules de G ou de D.
Preuve : Récurrence structurelle immédiate sur la preuve. ¤


Corollaire 27   ¾®$ x·F est prouvable en LK si et seulement s'il existe un nombre fini k de termes t1, ..., tk tels que ¾®F[t1/x], ..., F[tk/x] soit prouvable en LK.
Preuve : Soit p une preuve sans coupure de ¾® $ x·F. Soient t1, ..., tk les termes tels que F[ti/x] apparaît dans p. Il ne peut y avoir qu'un nombre fini de telles formules, car la preuve est finie.

Nous transformons la preuve p en une preuve de ¾®F[t1/x], ..., F[tk/x] comme suit : pour chaque séquent dans la preuve, effacer toute occurrence de $ x·F du côté droit des séquents, et ajouter toutes les formules F[t1/x], ..., F[tk/x] à droite. Remarquer que $ x·F ne peut apparaître qu'à droite des séquents. En particulier, cette transformation préserve les axiomes Ax. Elle laisse aussi invariante toutes les autres règles, autres que Cut et les règles sur les quantificateurs. Mais la seule règle sur les quantificateurs qui pourrait poser un problème est $R, que nous remplaçons simplement par un affaiblissement, puisque la traduction de la prémisse est incluse dans celle de la conclusion. Nous obtenons finalement une preuve de ¾®F[t1/x], ..., F[tk/x]. ¤


Corollaire 28  [Herbrand, version syntaxique]   Soit F une formule existentielle $ x1·...$ xn·Y, où Y est sans quantificateur.

Si ¾®F est prouvable dans LK, alors il existe un nombre fini k, et k instances Ys1, ..., Ysk de Y telles que ¾®Ys1, ..., Ysk soit prouvable dans LK.
Preuve : Récurrence immédiate sur n, en utilisant le corollaire 27. ¤

Une autre application directe de l'élimination des coupures est :


Corollaire 29  [Cohérence]  Le système LK est cohérent, autrement dit il n'y a pas de preuve du séquent ¾® dans LK.
Preuve : S'il y en avait une, il y en aurait une sans coupure. Mais l'ensemble des sous-formules de ¾® est vide, donc il n'en existe aucune preuve sans coupure. ¤

Notre prochain but est de montrer que LK est correct est complet par rapport à la sémantique de la logique classique du premier ordre. La version sémantique du théorème de Herbrand entraîne que ceci est vrai pour les formules existentielles, et nous savons aussi comment traduire des formules générales en formules existentielles qui aient le même statut de validité, par herbrandisation; il reste à montrer que nous pouvons faire la même chose mais dans le but de conserver le statut de prouvabilité.

Nous le faisons en remarquant que les règles de LK permutent dans les preuves sans coupure, comme Stephen C. Kleene [Kle67] l'a montré. Par exemple, nous pouvons prouver AÙ B¾® BÙ A soit comme ceci :



soit comme cela :



où les règles ÙR et ÙL ont été permutées. En général, nous avons :


Théorème 30  [Permutabilité]   Pour toutes règles R1 et R2 autres que Cut, nous disons que R1 permute sous R2, ou que la paire R1/R2 permute, si et seulement si pour toute preuve de la forme :



où les formules principales des conclusions des règles R1 n'est pas active dans la prémisse de la règle R2, nous avons aussi une preuve avec les règles R1 et R2 permutées, autrement dit de la forme :



Alors, les seules paires de règles qui ne permutent pas en LK sont "L/"R, "L/$L, $R/"R.
Preuve : Par inspection de toutes les paires de règles possibles. Nous ne le faisons pas explicitement, car c'est fastidieux tout en n'étant pas particulièrement instructif. L'idée, comme l'exemple ÙR/ÙL le montre, est que comme R1 et R2 agissent sur des parties différentes des séquents (dans l'exemple, ÙR était utilisée pour construire BÙ A à droite, alors que ÙL était utilisée pour construire AÙ B à gauche), nous pouvons les appliquer dans l'ordre que nous voulons.

Ceci ne fonctionne pas sur "L/"R, parce que pour prouver " x·F¾® " x· FÚF', nous devons utiliser "R en dernier, sinon nous écririons :



où il faut que yÏfv(t) pour appliquer "R, mais en général nous ne pouvons pas montrer F[t/x]¾® F[y/x]ÚF'[y/x] à moins que t=y. (Prendre F atomique, et F' telle que xÏfv(F'), alors cela ne peut être dérivé que par Ax suivi de ÚR.) Les autres impermutabilités sont d'une nature similaire. ¤

Donc, pour trouver une preuve d'un séquent donné G¾®D, nous pouvons choisir d'expanser n'importe quelle formule de G ou de D, à moins que les dépendances entre quantifications ne l'interdise. Ceci nous laisse une liberté considérable dans le choix d'une stratégie d'expansion lors de la recherche d'une preuve d'un séquent donné.


Théorème 31  [Herbrand-Skolem, syntaxique]   Une formule F est prouvable dans LK si et seulement si son herbrandisation est prouvable en LK.

De façon duale, F est cohérente en LK si et seulement si sa skolémisation est cohérente en LK.
Preuve : Nous laissons en exercice au lecteur de vérifier que F est prouvable (resp. cohérente) si et seulement si n'importe laquelle de ses formes prénexes est prouvable (resp. cohérente).

Supposons donc que F est en forme prénexe. Si F n'a pas de quantificateur universel, le résultat est évident. Sinon, écrivons F sous la forme Q1 x1 · ... · Qn xn · " y · Y, où Y = $ z1 · ... ··· $ zm · Y', et Y' est sans quantificateur. Nous pouvons toujours permuter toutes les règles de quantificateurs (ici, "R et $R) sous toutes les règles propositionnelles, et permuter les règles "R sous $R. Alors F est prouvable si et seulement si elle a une preuve p0 où les permutations ci-dessus ont été effectuées. En remontant p0 (le long de n'importe quelle branche) jusqu'à rencontrer une application de "R qui introduit la quantification " y, nous arrivons nécessairement à une sous-preuve p1 de la forme :



où y1, ..., yk sont de nouvelles variables distinctes deux à deux. Nous supposerons aussi sans perte de généralité que les formules (" y·Y)si, 1£ i£ n sont distinctes deux à deux.

D'une part, si F est prouvable, alors nous pouvons remplacer yi dans la preuve ci-dessus par n'importe quel terme ti, du moment que les variables libres dans ti ne détruisent pas les conditions de bord sur les instances de "R ou $L qui sont sous p1 dans p0 (rappelons que ces conditions de bord disent que nous ne pouvons introduire " x à droite ou $ x à gauche que si x n'est pas libre dans le reste du séquent). Dans ce but, il suffit de vérifier qu'aucune variable universellement quantifiée (ou aucune variable nouvelle comme les yi) ne sont libres dans ti. Nous pouvons choisir ti de la forme f(xi1, ..., xip)si sans danger, où xi1, ..., xip sont les variables existentielles parmi x1, ..., xn, pour chaque 1£ i£ k; si l'on remplace ti par yi ci-dessus, on remplace toute sous-preuve de la même forme que p1 par une autre preuve p'1 à l'intérieur de p0 : ceci transforme p en une preuve de F' défini par Q1 x1 · ... · Qn xn · Y'', où Y'' = ( $ z1 · ... ··· $ zm · Y') [f (xi1, ..., xip) / y] est une formule existentielle, autrement dit F' est une formule avec un quantificateur universel de moins que F.

D'autre part, si F' est prouvable, alors il existe une sous-preuve de ¾® Y[f (xi1, ..., xip)/y]s1, ..., Y[f (xi1, ..., xip)/y]sk, où de plus les domaines de s1, ..., sk sont inclus dans l'ensemble des variables existentielles xi1, ..., xip. Nous pouvons aussi supposer sans perte de généralité que toutes les formules Y[f (xi1, ..., xip)/y]si, 1£ i£ k, sont distinctes deux à deux. Comme f est un symbole de fonction nouveau, les seuls sous-termes dans ces formules construits avec f sont f (xi1, ..., xip)si, 1£ i£ n. Comme la preuve peut être supposée sans coupure, elle a la propriété de la sous-formule. Ainsi, comme les formules ci-dessus sont sans quantificateur, les seuls sous-termes construits avec f dans toute la preuve sont ceux mentionnés ci-dessus. Nous remplaçons maintenant f (xi1, ..., xip)si par autant de variables nouvelles yi, 1£ i£ n dans toute la preuve : remarquons que nous ne pouvons le faire que si, chaque fois que i¹ j, f (xi1, ..., xip)si et f (xi1, ..., xip)sj sont des termes distincts. Mais nous avons supposé que Y[f (xi1, ..., xip)/y]si et Y[f (xi1, ..., xip)/y]sj étaient distinctes, donc qu'il y avait une variable libre dans Y[f (xi1, ..., xip)/y] qui était remplacée par des termes différents par si et par sj. Et toutes ces variables libres font partie de xi1, ..., xip; donc f (xi1, ..., xip)si et f (xi1, ..., xip)sj sont distincts.

Maintenant que nous avons remplacé f (xi1, ..., xip)si par yi pour tout i dans la preuve, nous avons obtenu une preuve de ¾® Y[y1/y]s1,Y[y2/y]s2, ..., Y[yk/y]sk. Nous utilisons maintenant "R sur ces k formules tour à tour (nous le pouvons, parce que les yi sont distinctes deux à deux), et obtenons une preuve de ¾® (" y·Y)s1, ..., (" y·Y)sk, ce qui redonne la sous-preuve p1 de départ.

Cette construction montre comment éliminer un quantificateur universel par un symbole de Herbrand. Que l'herbrandisation préserve la prouvabilité résulte d'une récurrence sur le nombre de quantifications universelles (ou de symboles de Herbrand). Que la skolémisation préserve la cohérence s'ensuit par dualité par négation. ¤

Nous concluons par le théorème de complétude pour la logique classique du premier ordre, qui a été prouvé pour la première fois par Kurt Gödel en 1930, quoique sous une forme différente :


Théorème 32  [Correction, complétude]  LK est correct et complet pour la sémantique de la logique classique du premier ordre, autrement dit |=F si et seulement si |-LKF.
Preuve : La correction est claire. Pour montrer la complétude, supposons que |=F. Soit F'= $ x1·...$ xn·Y une forme de Herbrand de F. Alors |=F'. Par la version sémantique du théorème de Herbrand, il existe k instances closes Ys1, ..., Ysk de Y telles que |= Ys1Ú...ÚYsk. Par le théorème de complétude pour LK0, |-LK0Ys1, ..., Ysk, donc |-LKYs1, ..., Ysk car LK0 est un sous-ensemble de LK. En utilisant $R k fois, nous en déduisons |-LKF', et par le théorème 31, |-LKF. ¤

Une preuve plus directe de la complétude d'un système de preuve pour la logique classique du premier ordre, qui n'utilise pas de forme prénexe, de Herbrand ou de Skolem, utilise ce qu'on appelle les constantes de Henkin, introduites par Leon Henkin en 1949. À notre avis, la preuve est au moins aussi compliquée et présente moins d'intuitions en rapport avec les façons de rechercher des preuves automatiquement. (Cf. [Man77].)



Previous Next Contents