2 La preuve réparée
Nous devons donc être plus fins, et remplacer la construction du
lemme 1 par une construction plus précise, qui
assure en plus que B¥ vérifie la propriété 4.
Lemme 7
Pour toute branche cohérente finie B, il existe une branche
cohérente maximale B¥ contenant B, et qui soit de plus
saturée.
Preuve : La construction du lemme 1 consiste grosso modo
à ajouter des formules signées à B de sorte à préserver
la cohérence, et ce jusqu'à ce que pour toute formule F, soit
+F soit -F ait été rajoutée. L'idée ici va être que,
dès que l'on souhaite ajouter une formule d à B, on va
aussi lui ajouter d1 (y), où y est une variable
fraîche.
Notons que : (a) pour toute branche finie cohérente B' contenant
d, alors B' È {d1 (y)} est encore une branche
finie cohérente, pour toute variable y non libre dans B'.
Considérons le cas où B' contient d de la forme
+" x · F1, et montrons que B' È {+F1 [y/x]} est
encore cohérente. En effet, supposons le contraire, écrivons
B' sous la forme B'' È {+" x · F1}, et B''
sous forme de séquent comme G ¾® D. Si B' È
{+F1 [y/x]} n'était pas cohérente, nous aurions par
définition une preuve de G ¾® D, " x·
F1, F1 [y/x]. Comme y n'est pas libre dans B', nous pouvons
donc appliquer la règle (" R) et en déduire G
¾® D, " x· F1, " x· F1,
c'est-à-dire B'; mais ceci contredit la cohérence de B'.
(Le cas ou d est de la forme -$ x · F1 est
symétrique, et utilise la règle $L.)
Nous construisons maintenant une suite croissante de branches finies
cohérentes Bn contenant B comme suit. Fixons une
énumération ± F1, ± F2, ..., ± Fn, ..., de
toutes les formules signées. Nous construisons Bn par
récurrence sur n comme suit. Pour n=0, posons Bn = B. Si
n³ 1, et si Bn-1 È {± Fn} est incohérente, alors
soit Bn = Bn-1. Si n³ 1, et si Bn-1 È {±
Fn} est cohérente, alors de deux choses l'une : ou bien ±
Fn est une formule de la forme d, et l'on pose alors Bn =
Bn-1 È {d, d1 (y)}, où y est une variable
quelconque non libre dans Bn-1 È {d} (Bn est alors
bien finie et cohérente, par (a)); ou bien ± Fn n'est pas une
formule de la forme d, et l'on pose alors Bn = Bn-1 È
{± Fn}.
Posons B¥= Èn³ 0 Bn. B¥ contient
B0, donc B. De plus, B¥ est cohérente : sinon,
B¥ contiendrait une sous-branche finie prouvable, et cette
branche serait incluse dans un Bn pour n assez grand, ce qui
contredirait la cohérence de Bn. B¥ est maximale :
supposons que non, alors il existerait une formule signée ±
Fn (n³ 1) en-dehors de B¥ telle que B¥È
{± Fn} soit cohérente; mais comme ± Fn n'est pas dans
B¥, en particulier ± Fn n'est pas dans Bn, donc par
construction de Bn, Bn-1 È {± Fn} doit être
incohérente, donc prouvable (en tant que séquent); mais ceci
contredit la cohérence de B¥È {± Fn}.
Finalement, B¥ est saturée. En effet, il suffit de
vérifier 4., puisque 1.--3. sont des conséquences du fait que
B¥ est cohérente maximale, par le
lemme 2. Or, pour toute formule d
dans B¥, d s'écrit ± Fn pour un (unique)
n³ 1. Comme d est dans B¥, B¥È {±
Fn} est cohérente, donc Bn-1 È {± Fn} (qui est un
sous-ensemble fini du précédent) est cohérent. Mais par
construction, on a alors Bn = Bn-1 È {± Fn, d1
(y)} pour une certaine variable y, et donc d1 (y) Î
Bn, d'où d1 (y) Î B¥ : B¥ est bien
saturée.
¤
La preuve est maintenant réparée :
Théorème 8
LK est complet : tout séquent valide est prouvable.
Preuve : Par le théorème 6 et le
lemme 7.
¤