DÉMONSTRATION THÉORIE DE LA

Système LK

Dans ce qui suit, L est un langage du premier ordre arbitraire. Un séquent est une expression formelle Γ ⊢Δ, où Γ et Δ sont des suites finies d'énoncés de L. L'interprétation intuitive de A₁, ..., A_n⊢ B₁, ..., B_m, c'est que la conjonction des A_i implique la disjonction des B_j. En particulier, ⊢ A veut dire A, et A ⊢ veut dire ¬ A ; quant au séquent vide ⊢, il signifie l'absurdité. Dans les systèmes séquentiels, la cohérence sera toujours interprétée par la non-prouvabilité de ⊢. Dans la formulation qui suit du calcul des séquents LK, on utilise la virgule pour dénoter la mise bout à bout (concaténation) de suites, par exemple Γ, Λ ; on utilise Γ, A au lieu de Γ, {A}.

Les règles représentées dans le tableau ci-après sont divisées en quatre groupes ; mais elles sont d'importance inégale. En particulier, les règles structurelles sont de peu d'intérêt ; il convient cependant de ne pas mépriser l'importance des règles de contraction. Dans les groupes II et III, les règles sont divisées en droites et gauches : pour toutes ces règles (sauf l'échange), on a une « formule principale » : il s'agit de la formule écrite explicitement en conclusion ; sa localisation par rapport à ⊢ détermine le caractère gauche ou droit de la règle ; dans la règle de coupure, A est la formule de coupure.

Théorème de complétude. Le séquent Γ ⊢ Δ est vrai dans tout modèle de L si et seulement s'il est démontrable dans LK. En particulier, si on se restreint aux séquents de la forme ⊢ A, LK est équivalent au calcul des prédicats.

Théorème d'élimination des coupures ( Hauptsatz de Gentzen). Dans LK, la règle de coupure (C) est inutile, autrement dit tout théorème de LK est démontrable sans coupures.La démonstration de ce résultat, assez longue et délicate, consiste à remplacer toute coupure de formule principale A par de nombreuses coupures dont les formules de coupure sont des sous-formules (voir leur définition plus bas) strictes de A.

Donnons quelques exemples :

est remplacée par :(la double barre indique que, en plus de la coupure, on a utilisé un certain nombre de règles structurelles). De la même manière,devient :et on remplace enfin :par :La démonstration de Γ ⊢ A[t], Δ est obtenue en remplaçant a par t dans la démonstration de Γ ⊢ A[a], Δ. Dans la pratique, tout est rendu beaucoup plus compliqué par la règle de contraction, mais l'idée essentielle est exprimée dans les exemples donnés ci-dessus.

Le Hauptsatz a pour corollaire la propriété de la sous-formule. Par définition, une sous-formule de A est soit A elle-même, soit :

– dans le cas où A est ¬B, toute sous-formule de B,

– dans le cas où A est B ∨ C, B & C, B → C, toute sous-formule de B et/ou de C,

– dans le cas où A est ∀x B[x], ∃x B[x], toute sous-formule des formules B[t], t étant un terme quelconque.

Théorème. La « propriété de la sous-formule » s'exprime[...]