Previous Next Contents

3  Complétude de la méthode des tableaux

Nous allons maintenant être beaucoup plus ambitieux, et montrer que la méthode des tableaux à variables libres avec règle d++ est complète. Le résultat sera beaucoup plus fort que la complétude de LK, et montrera non seulement la complétude, mais encore qu'on n'a jamais besoin de coupure, ni de contraction (sauf sur les règles g), et que n'importe quelle stratégie d'expansion de tableaux est complète du moment qu'elle est équitable. Mais beaucoup de techniques de preuve ressembleront à ceux développés pour la complétude de LK.

Comme nous voulons contrôler l'usage de la contraction, nous allons considérer dorénavant les branches comme des multi-ensembles de formules signées. Les règles d'expansion de tableaux sont : Ensuite, nous voulons pouvoir repérer des occurrences de formules dans les branches. Pour ceci, nous étiquetons les formules signées (certaines, au moins) par des entiers (ou n'importe quel autre moyen d'étiquetage) : notons ± Fi la formule signée ± F étiquetée par i. Une stratégie consistera à choisir une formule étiquetée dans la branche. Les règles d'expansion deviennent : si B1 ne contient que des formules non étiquetées, alors B1 ne s'expanse pas; sinon, la stratégie choisit une des formules étiquetées ± Fi de B1 : soit B = B1 \ {± Fi}. Si F est atomique, alors enlever l'étiquette, autrement dit B1 s'expanse en B È {± F}. Sinon, B È {ai} s'expanse en B È {a1j} et en B È {a2k}, où j et k sont deux nouvelles étiquettes; B È {bi} s'expanse en B È {b1j, b2k}, où j et k sont deux nouvelles étiquettes; B È {gi} s'expanse en B È {gj, g1 (y)k}, où y est une variable fraîche, et j et k sont deux nouvelles étiquettes (noter qu'on remplace l'occurrence i de g pour une nouvelle occurrence j); B È {di} s'expanse en une branche B È {d1 (f (x1, ..., xn))j} comme plus haut, avec j une nouvelle étiquette.

Nous supposerons qu'il n'y a jamais deux formules avec la même étiquette sur la même branche. De plus, nous supposerons que la stratégie choisi la formule étiquetée sur la branche sans regarder le contenu des formules, par exemple, on choisissant toujours la formule de plus petite étiquette (en général, ce qu'on voudra, c'est que si la stratégie choisit ± Fi dans B, alors elle choisit aussi ± Fi s dans l'instance B s de B). Finalement, nous supposerons que la stratégie est équitable, ce qui signifie que, quelle que soit la suite de branches B0, B1, ..., Bn, ..., telle que tout Bn+1 est obtenu par expansion à partir de Bn, pour toute formule étiquetée ± Fi dans Bn, il existe p³ n telle que la stratégie sélectionne ± Fi dans Bp.

Supposons maintenant que B est une branche close improuvable par la méthode des tableaux utilisant une stratégie équitable donnée. Nous pouvons alors construire une suite de branches closes improuvables B0, B1, ..., Bn, ..., comme suit. L'idée est que nous allons suivre la procédure des tableaux, en choisissant toujours une expansion de la branche courante qui n'a aucun tableau clos. Ceci va nous donner une suite de branches B'0, B'1, ..., B'n, ..., et nous allons construire chaque Bn comme une instance close B'n sn de B'n. Avant de commencer, soit t1, t2, ..., tp, ..., une énumération de tous les termes clos.

D'abord, B'0 = B0 = B, s0 est la substitution vide. Ensuite, si B'n, Bn, sn ont été construits, soit Bn ne contient que des formules non étiquetées, et la suite s'arrête ici, soit la stratégie choisit une des formules étiquetées ± Fi de B'n : soit B = B'n \ {± Fi}. Alors, en reprenant les notations déjà utilisées plus haut :
Lemme 9   Supposons que toutes les formules de B0 sont étiquetées. Alors l'ensemble B¥ des formules signées apparaissant étiquetées ou non dans Èn³ 0 Bn est saturé. On dira qu'un ensemble de formules signées est saturé si et seulement si les conditions 1.--4. sont vérifiées, en remplaçant ``terme'' par ``terme clos'' et ``formule'' par ``formule close''.
Preuve : Par récurrence, on montre aisément que toute formule non atomique de tout Bn est étiquetée. Si on a une formule a dans B¥, alors elle est dans un Bn. Mais comme la stratégie est équitable, cette formule finit par être choisie, disons au rang m³ n, et donc a1 ou a2 est dans Bm+1, donc dans B¥ : ceci prouve la condition 1. De même, si b Î B¥, alors b1 et b2 sont dans B¥, ce qui montre la condition 2. La condition 4 est maintenant facile, parce que si d est dans B¥, alors d1 (f (x1 sm+1, ..., xn sm+1)) est dans Bm+1, donc dans B¥, pour m assez grand. Il ne reste qu'à montrer la condition 3. Pour ceci, soit g Î B¥, nous montrons par récurrence sur p qu'il existe une branche étiquetée Bmp contenant g ainsi que g1 (t1), ..., g1 (tp) (chacune étant étiquetée de façon appropriée) pour tout p. Pour p=0, c'est évident. Sinon, supposons Bmp construite. Comme la stratégie est équitable, elle finit par expanser l'instance étiquetée de g, disons au rang mp+1-1. Bmp+1 contient alors une nouvelle version étiquetée de g, ainsi que g1 (t1), ..., g1 (tp), plus g1 (tp+1), puisque tp+1 est en effet le premier terme clos de l'énumération tel que g (tp+1) n'apparaissait pas sur la branche. On en conclut que B¥ contient tous les g1 (tp), donc tous les g1 (t) pour tout terme clos t : la condition 4. est donc vérifiée. ¤


Lemme 10   Un ensemble de formules signées est dit de Hintikka si et seulement s'il est saturé, et pour aucune formule atomique A, il ne contient à la fois +A et -A. Sous les hypothèses du lemme 9, B¥ est de Hintikka.
Preuve : Si on avait à la fois +A et -A dans B¥, alors +A serait dans un Bm et -A dans un Bn (à étiquetage près). Ceci implique que Bm contiendrait un +A' avec A' sm = A et que Bn contiendrait un -A'' avec A'' sn = A. Supposons que n³ m, le cas m³ n étant symétrique. Alors sn est de la forme sm È s, où s est une substitution de domaine disjoint d'avec celui de sm, comme on peut le vérifier dans la construction. Comme A est clos, aucune variable libre de A' n'est dans le domaine de s, donc A = A' sn. Il s'ensuit que, dans la branche Bn, A' et A'' sont unifiables, car sn est un unificateur. Mais c'est impossible, parce que Bn est improuvable. ¤

On peut maintenant montrer la complétude des tableaux en ajoutant à B¥ toutes les formules atomiques qui n'y apparaissaient pas (ajouter par exemple +A, pour tout A tel que ni +A ni -A n'est dans B¥), et en ajoutant suffisamment de formules pour que les conditions 1.--4. deviennent des équivalences. On obtient encore un ensemble de Hintikka, et la preuve du lemme 5 permet alors d'obtenir un contre-modèle de cette branche complétée, donc de B¥, donc de B.

Une façon plus directe de faire est la suivante :
Lemme 11  [Hintikka]   Tout ensemble de Hintikka B¥ a un contre-modèle.
Preuve : Soit D, le domaine, égal à l'ensemble des termes clos. L'interprétation est une interprétation de Herbrand, donc telle que pour chaque symbole de fonction f d'arité n, l'interprétation I (f) est la fonction qui aux termes clos t1, ..., tn associe le terme clos f (t1, ..., tn). Il ne reste donc qu'à spécifier quels atomes clos sont vrais dans I : ce seront les atomes A tels que -A Î B¥. (En particulier, les atomes tels que +A Î B¥ sont faux, mais aussi tous les atomes qui n'apparaissent pas dans B¥: mettre ces derniers à faux est un choix totalement arbitraire.) Nous allons montrer que : (*) pour toute formule close F, si -F Î B¥, alors I |= F, et si I |= F, alors +F ÏB¥. Ceci se fait par récurrence sur la taille de F. Si F, est une formule atomique A, alors -A Î B¥ implique I |= A par définition. Et si I |= A, alors -A Î B¥ par définition, donc +A ÏB¥ parce que B¥ est de Hintikka. Si F est une formule de la forme F1 Ù F2, alors -F est de type b. Donc si -FÎ B¥, alors -F1 et -F2 sont aussi dans B¥, donc par hypothèse de récurrence I |= F1 et I |= F2, donc I |= F. Et si I |= F, alors I |= F1 et I |= F2, donc ni +F1 ni +F2 ne sont dans B¥. Or si +F était dans B¥, comme +F est de type a, l'une des deux formules signées +F1 ou +F2 serait dans B¥. Donc +F Ï B¥. Si F est de la forme ¬ F1, et si -F Î B¥, alors +F1 Î B¥. Mais par récurrence, si I |= F1 alors +F1 ÏB¥. Donc il est faux que I |= F1, donc I |= F. Et si I |= F, alors il est faux que I |= F1, donc il est faux que -F1 Î B¥, par récurrence. Mais si +F était dans B¥, -F1 serait justement dans B¥. Donc +F n'est pas dans B¥.

Les cas des autres connecteurs propositionnels sont similaires. Examinons donc maintenant les quantificateurs. Si F est de la forme " x · F1, alors -F est de type g. Donc si -F Î B¥, pour tout terme clos t, -F1 [t/x] est dans B¥. Comme la taille de F1 [t/x] est égale à celle de F1, qui est strictement plus petite que celle de F, nous pouvons appliquer l'hypothèse de récurrence, et conclure que I |= F1 [t/x], et ce pour tout terme clos t, c'est-à-dire pour toute valeur tÎ D. Donc I |= F. Ensuite, si I |= F, alors I |= F1 [t/x] pour tout terme clos t, donc +F1 [t/x] n'est dans B¥ pour aucun terme clos t. Donc +F, qui est de type d, ne peut pas être dans B¥. Si F est de la forme $ x · F1, finalement, -F est de type d. Donc si -F Î B¥, alors -F1 [t/x] Î B¥ pour au moins un terme clos t, ce qui entraîne par l'hypothèse de récurrence que I |= F1 [t/x] pour au moins une valeur tÎ D, c'est-à-dire I |= F. Ensuite, si I |= F, alors il existe un terme clos t tel que I |= F1 [t/x], donc tel que +F1 [t/x] ne soit pas dans B¥, par récurrence. Mais alors F n'est pas non plus dans B¥, car sinon tous les +F1 [t/x] seraient dans B¥. (*) étant montrée, il s'ensuit que, pour tout -F Î B¥, I |= F, autrement dit I falsifie -F, et pour tout +F Î B¥, il est faux que I |= F, autrement dit I falsifie +F. Donc I falsifie B¥. ¤


Théorème 12   La méthode des tableaux à variables libres avec règle d++ est complète.
Preuve : Partons d'une branche B0 n'ayant pas de preuve par tableaux. Par le lemme 9, B¥ contient B0 et est saturé. Par le lemme 10, B¥ est un ensemble de Hintikka. Il s'ensuit que B¥ a un contre-modèle par le lemme 11, qui est donc un contre-modèle pour B0. ¤

Au risque de nous répéter, rappelons que ce résultat est beaucoup plus fort que la complétude de LK : observer que nous n'avons jamais utilisé la coupure, ni la contraction (sauf sur les règles g), que nous n'avons eu besoin de clore les branches que sur des formules atomiques, et que tout stratégie d'expansion de tableaux convient du moment qu'elle est équitable.

Previous Next Contents