MAGISTERE MATH.-INFO.

(2003-2004) Logique
E. Bouscaren

Théorème de complétude du calcul

propositionnel
Notes complémentaires (0)

1 Quelques rappels de sémantique

Définition: Un ensemble de formules Σ est satisfaisable si il existe une distribution de
valeurs de vérité, δ, qui satisfait toutes les formules de Σ, c’est-à-dire telle que, pour toute
formule B ∈ Σ, δ(B) = 1. Un ensemble qui n’est pas satisfaisable est dit inconsistant .

On a démontré en cours:
Proposition 1.1 (Theorème de compacité du calcul propositionnel) Soit Σ un ensem-
ble de formules, Σ est satisfaisable si et seulement si tout sous-ensemble fini de Σ est
satisfaisable.
Définition : Soient Σ un ensemble de formules et A une formule. On dit que A est
conséquence sémantique de Σ, noté Σ ` A, si toute distribution de valeurs de vérité δ
qui satisfait Σ satisfait également A.
Si A est une tautologie on a ∅ ` A, noté ` A.

Les premières propriétés:

Lemme 1.2 Soit Σ un ensemble de formules et B une formule.
(i) Σ est inconsistant ssi il existe une formule A telle que Σ ` A et Σ ` ¬A.
(ii) Σ est inconsistant ssi, pour toute formule A, Σ ` A et Σ ` ¬A.
(iii) Σ ` B ssi Σ ∪ {¬B} est inconsistant.
La proposition suivante est équivalente au théorème de compacite (1.1):
Proposition 1.3 Soit Σ un ensemble de formules et B une formule. Alors Σ ` B si et
seulement si il existe un sous-ensemble fini F de Σ tel que F ` B.
Démonstration de l’équivalence : Supposons d’abord 1.1: Si Σ ` B, par le lemme 1.2,
Σ∪{¬B} est inconsistant. Par 1.1, il existe un sous-ensemble fini F de Σ tel que F ∪{¬B}
est inconsistant. Par 1.2 à nouveau, F ` B.
Réciproquement, supposons 1.3, et soit Σ un ensemble de formules inconsistant. Alors
par 1.2 , il existe une formule A telle que Σ ` A et Σ ` ¬A. Par 1.3, il existe F1 et F2 ,
sous-ensembles finis de Σ tels que F1 ` A et F2 ` ¬A. Donc F1 ∪ F2 ` A et F1 ∪ F2 ` ¬A,
et donc F1 ∪ F2 est un sous-ensemble fini de Σ qui est inconsistant. 2

1
2 Complétude pour le calcul propositionnel
On reprend ici brièvement la démonstration du théorème de complétude donné en cours
(et qui est celle du livre “Introduction to Mathematical Logic” de E. Mendelson.)

On considère le calcul propositionnel avec les connecteurs {¬, → }

2.1 Preuves formelles, premières propriétés

LES AXIOMES
On prend trois schémas d’axiomes:
(A1) : Pour toutes formules propositionnelles A, B
– (A → (B → A))

(A2) : pour toutes formules propositionnelles A, B, C

– ((A → (B → C)) → ((A → B) → (A → C)))

(A3) : pour toutes formules propositionnelles A, B

– ((¬B → ¬A) → ((¬B → A) → B))

Une RÈGLE de déduction:

- le Modus Ponens: pour toutes formules propositionnelles A, B, de {A, (A → B)} on
déduit B.

Définition: Soit Σ un ensemble de formules propositionnelles et A une formule proposi-

tionnelle. On dit que A est conséquence syntaxique, ou conséquence formelle de Σ,
noté Σ |∼ A, s’il existe une démonstration formelle (ou preuve formelle) de A à partir
de Σ, c’est-à-dire, s’il existe une suite finie {A1 , . . . , Ak } de formules propositionnelles,
telles que
- Ak = A,
- pour chaque i ≤ k, l’une des trois conditions suivantes est remplie
– soit Ai est une formule de Σ,
– soit Ai est un axiome
– soit Ai a été déduit par Modus Ponens de deux formules Al et Am = (Al → Ai )
avec m, l < i.

Remarques évidentes:
– {A} |∼ A
– Si A est un axiome, |∼ A
– Si Σ1 ⊂ Σ2 et Σ1 |∼ A, alors Σ2 |∼ A.

Un exemple de démonstration formelle

Lemme 2.1 Pour toute formule A, |∼ (A → A).

2
Démonstration :
(1) A1 = ((A → ((A → A) → A)) → ((A → (A → A)) → (A → A))) , (Axiome
2 avec B = (A → A) et C = A )
(2) A2 = (A → ((A → A) → A)), (Axiome 1 avec B = (A → A))
(3) A3 = ((A → (A → A)) → (A → A)), ( Modus Ponens appliqué à A1 et A2 )
(4) A4 = (A → (A → A)), (Axiome 1 avec B = A)
(5) A5 = (A → A) ( Modus Ponens appliqué à A3 et A4 ). 2

Les lemmes suivant sont immédiats mais importants. Σ est un ensemble de formules, A
et B sont des formules:

Lemme 2.2 Si Σ |∼ A et Σ |∼ (A → B), alors Σ |∼ B.

Lemme 2.3 Si A1 , . . . , Ak est une démonstration formelle de Σ |∼ A, de longueur k,

alors pour chaque i < k, A1 , . . . , Ai est une démonstration formelle de Σ |∼ Ai qui est de
longueur i, donc de longueur strictement inférieure à k.

Lemme 2.4 (Finitude) Si Σ |∼ A, alors il existe un sous-ensemble fini Σ0 de Σ tel que

Σ0 |∼ A.

Lemme 2.5 Si Σ |∼ (A → B), alors Σ ∪ {A} |∼ B.

Démonstration : Σ ∪ {A} ⊃ Σ, donc puisque Σ |∼ (A → B), a fortiori Σ ∪ {A} |∼ (A →

B). Par la remarque plus haut: Σ ∪ {A} |∼ A, donc (2.2) Σ ∪ {A} |∼ B. 2

Un peu plus difficile, la réciproque:

Lemme 2.6 (Lemme de déduction)

Si Σ ∪ {A} |∼ B , alors Σ |∼ (A → B).

Démonstration : On raisonne par récurrence sur la longueur d’une démonstration formelle,

B1 , . . . , Bk+1 = B, de Σ ∪ {A} |∼ B.
On suppose que k ≥ 0.
Premier cas: Bk+1 est un axiome ou un élément de Σ. Alors on a la suite suivante:
(1) C1 = B (axiome ou élément de Σ )
(2) C2 = (B → (A → B)) (axiome A1)
(3) C3 = (A → B) (par Modus Ponens appliqué à C1 et C2 )
qui est une démonstration formelle de (A → B) à partir de Σ.
Deuxième cas: B = A. Alors on a vu plus haut (Lemme 2.1) que |∼ (A → A).
Troisième cas (possible uniquement si k ≥ 2): Bk+1 = B est obtenu par application de la
règle de Modus ponens à Bi et Bj = (Bi → B), avec i, j < k + 1.
Par le lemme 2.3, il y a des preuves de Σ ∪ {A} |∼ Bi et de Σ ∪ {A} |∼ Bj de longueurs
inférieures ou égales à k. Donc par hypothèse de récurrence, on a
(1) Σ |∼ (A → Bi )
(2) Σ |∼ (A → (Bi → B)).
Par l’axiome (A2), on a aussi

3
 (3) Σ |∼ ((A → (Bi → B)) → ((A → Bi ) → (A → B))).
Par Modus Ponens appliqué à (2) et (3),
(4) Σ |∼ ((A → Bi ) → (A → B)).
et par Modus Ponens appliqué à (1) et (4),
(5) Σ |∼ (A → B). 2

Avec l’aide du Lemme de déduction (2.6) et un peu de travail, on peut montrer:

Lemme 2.7 Pour toutes formules A, B et C,

(i) |∼ (¬¬A → A)
(ii) |∼ (A → ¬¬A)
(iii) |∼ (¬A → (A → B))
(iv) |∼ (A → (¬B → (¬(A → B))))
(v) |∼ ((A → B) → ((¬A → B) → B))

Les “théorèmes” donnés dans le lemme précédent sont exactement ceux dont on va avoir
besoin pour démontrer le théorème de complétude (on aurait bien sûr pu les prendre au
départ comme axiomes supplémentaires, mais cela n’aurait pas été très économique).

Enfin un dernier résultat fondamental:

Lemme 2.8 Pour tout ensemble de formules Σ, pour toutes formules A et B, si

Σ ∪ {A} |∼ B et Σ ∪ {¬A} |∼ B, alors Σ |∼ B.

Démonstration : Par le lemme de déduction (2.6), on a

(1) Σ |∼ (A → B)
et
(2) Σ |∼ (¬A → B).
Par 2.7 (v):
(3) |∼ ((A → B) → ((¬A → B) → B))
par Modus Ponens appliqué à (1) et (3),
(4) Σ |∼ ((¬A → B) → B)
par Modus Ponens appliqué à (2) et (4),
(5) Σ |∼ B. 2

Définition : On dit que Σ est contradictoire si il existe une formule A telle que Σ |∼ A
et Σ |∼ ¬A.

Lemme 2.9 Σ est contradictoire si et seulement si, pour toute formule B, Σ |∼ B.

Démonstration : Supposons Σ contradictoire, donc il existe une formule A telle que Σ |∼ A

et Σ |∼ ¬A. Par le lemme 2.7 (iii), |∼ (¬A → (A → B)). En appliquant le Modus Po-
nens deux fois, on obtient bien Σ |∼ B. 2

4
2.2 Rapports avec la sémantique
2.2.1 Le théorème de complétude finitaire
Proposition 2.10 (Validité) Soient Σ un ensemble de formules et A une formule. Si
Σ |∼ A , alors Σ ` A. En particulier, si |∼ A, alors A est une tautologie.

Démonstration : On commence par vérifier facilement que si A est l’un des axiomes (A1),
(A2) ou (A3), alors A est une tautologie.
Ensuite, on raisonne par récurrence sur la longueur d’une preuve formelle de Σ |∼ A,
A1 , . . . , An+1 = A, avec n ≥ 0.
Premier cas: An+1 = A est un axiome, alors on a vérifié que A est une tautologie donc
certainement Σ ` A.
Deuxième cas: A ∈ Σ et le résultat est évident.
Troisième cas (si n ≥ 2): A est obtenu par application de la règle de Modus Ponens à Ai
et Aj = (Ai → A), avec i, j ≤ n. Par le le lemme 2.3, on a donc des preuves de longueur
inférieure ou égale à n de Σ |∼ Ai et de Σ |∼ Aj . Par hypothèse de récurrence, on a donc

Σ ` Ai et Σ ` (Ai → A).

Soit δ une distribution qui satisfait Σ, alors par ce qui précéde, δ(Ai ) = 1 et δ(Ai →
A) = 1. Par définition (sémantique) du connecteur → , on doit avoir δ(A) = 1. 2

Proposition 2.11 (Théorème de complétude finitaire)

Soit A une formule, si ` A alors |∼ A.

Il s’agit donc d’exhiber une preuve formelle de la tautologie A. Pour cela on commence
par le lemme suivant qui est très astucieux.

Lemme 2.12 Soit A une formule à variables parmi {P1 , . . . , Pn }. Soit δ une distribution
de valeurs de vérité, δ : {P1 , . . . , Pn } 7→ {0, 1}. On pose, pour 1 ≤ i ≤ n ,
Pi δ = Pi si δ(Pi ) = 1, Pi δ = ¬Pi si δ(Pi ) = 0.
Et on pose
Aδ = A si δ(A) = 1, Aδ = ¬A si δ(A) = 0.
Alors {P1 δ , . . . , Pn δ } |∼ Aδ .

Démonstration : Par induction sur la complexité de la formule A.

– Si A est une variable propositionnelle, A = Pi , alors Pi δ = Aδ et certainement
{P1 δ , . . . , Pn δ } |∼ Pi δ .
– Si A = ¬B. Si δ(B) = 0, alors B δ = ¬B = A = Aδ et donc, par hypothèse
d’induction, {P1 δ , . . . , Pn δ } |∼ Aδ .
Si δ(B) = 1, B δ = B et Aδ = ¬¬B. Par hypothèse d’induction on a {P1 δ , . . . , Pn δ } |∼ B,
par le lemme 2.7(ii), |∼ (B → ¬¬B) et donc par Modus Ponens, {P1 δ , . . . , Pn δ } |∼ ¬¬B.
– Si A = (B → C), avec par hypothèse d’induction, pour toute δ, {P1 δ , . . . , Pn δ } |∼ B δ
et {P1 δ , . . . , Pn δ } |∼ C δ . Il y a trois cas. Tout d’abord, si δ(B) = 0, alors B δ = ¬B, et
δ(B → C) = 1, donc Aδ = A. On a {P1 δ , . . . , Pn δ } |∼ ¬B, par le lemme 2.7 (iii),

5
 |∼ (¬B → (B → C)), et par Modus Ponens, {P1 δ , . . . , Pn δ } |∼ (B → C).
Deuxième cas, si δ(B) = 1 et δ(C) = 1, donc C δ = C et Aδ = A = (B → C). On a
par hypothèse {P1 δ , . . . , Pn δ } |∼ C , par l’axiome (A1), |∼ (C → (B → C)), donc par
Modus Ponens, {P1 δ , . . . , Pn δ } |∼ (B → C).
Dernier cas, si δ(B) = 1 et δ(C) = 0, donc δ(A) = 0. Par induction, {P1 δ , . . . , Pn δ } |∼ B
et {P1 δ , . . . , Pn δ } |∼ ¬C. Par le lemme 2.7 (iv), |∼ (B → (¬C → ¬(B → C))). En
appliquant le Modus Ponens deux fois de suite, on obtient bien {P1 δ , . . . , Pn δ } |∼ ¬(B →
C) (= Aδ ). 2

On peut maintenant démontrer la proposition 2.11 :

Soit A une tautologie. Alors pour toute application δ de {P1 , . . . , Pn } dans {0, 1},
Aδ = A et donc, par le lemme précédent, {P1 δ , . . . , Pn δ } |∼ A.
En particulier, pour toute δ0 application de {P1 , . . . , Pn−1 } dans {0, 1}, on a
{P1 δ0 , . . . , Pn−1 δ0 , Pn } |∼ A
et
{P1 δ0 , . . . , Pn−1 δ0 , ¬Pn } |∼ A.
Par le lemme 2.8, on déduit que :
{P1 δ0 , . . . , Pn−1 δ0 } |∼ A,
et ceci à nouveau pour toute δ0 .
En appliquant ce raisonnement plusieurs fois on arrive à
{P1 } |∼ A et {¬P1 } |∼ A
et en appliquant une dernière fois le lemme 2.8, à
|∼ A. 2

Corollaire 2.13 Soient Σ un ensemble fini de formules et A une formule. Si Σ ` A,

alors Σ |∼ A.

Démonstration : Par hypothèse, Σ est fini, on raisonne par récurrence sur sa cardinalité.
Si Σ est vide (de cardinalité nulle) , alors c’est exactement la proposition 2.11.
Si Σ = {D0 , . . . , Dn } (n ≤ 0), alors soit Σ0 = {D0 , . . . , Dn−1 }. On a Σ0 ∪ {Dn } ` A.
Il suit facilement que Σ0 ` (Dn → A). En effet, soit δ qui satisfait Σ, alors si δ(Dn ) = 0,
on a toujours δ((Dn → A)) = 1; si δ(Dn ) = 1, δ satisfait Σ0 ∪ {Dn }, donc δ(A) = 1 et
δ((Dn → A)) = 1 aussi.
Par hypothèse de récurrence, Σ0 |∼ (Dn → A). Par le lemme 2.5, Σ0 ∪ {Dn } |∼ A. 2

2.2.2 Les théorèmes de complétude et de compacité

On peut déduire le théorème de complétude général du corollaire précédent et du théorème
de compacité:

Proposition 2.14 (Théorème de complétude)

Soient Σ un ensemble de formules et A une formule. Si Σ ` A, alors Σ |∼ A.

6
Démonstration : Si Σ ` A, par compacité, il existe Σ0 sous-ensemble fini de Σ tel que
Σ0 ` A (voir section 1). Par le corollaire 2.13, Σ0 |∼ A, et donc Σ |∼ A. 2

Mais on trouve souvent des preuves directes du théorème de complétude général, avec
un ensemble de formules Σ infini. On peut alors en déduire le théorème de compacité:
Soit Σ un ensemble de formules non satisfaisable. On a vu (1.2) que alors il existe une
formule A telle que Σ ` A et Σ ` ¬A. Par le théorème de complétude, Σ |∼ A et Σ |∼ ¬A.
Par le lemme de finitude ( 2.4), il y a Σ1 et Σ2 , sous-ensembles finis de Σ, tels que Σ1 |∼ A
et Σ2 |∼ ¬A, Par le lemme de validité (2.10), Σ1 ` A et Σ2 ` ¬A. Le sous-ensemble fini
Σ1 ∪ Σ2 est donc non satisfaisable.
En fait on démontre souvent le théorème de complétude sous la forme équivalente
suivante:

Proposition 2.15 Soit Σ un ensemble de formules non contradictoire, alors Σ est satis-
faisable.

Démonstration de l’équivalence des propositions 2.14 et 2.15:

Supposons 2.14, et soit Σ un ensemble de formules qui n’est pas satisfaisable. Alors
par (1.2), il existe une formule A telle que Σ ` A et Σ ` ¬A. Par 2.14, Σ |∼ A et Σ |∼ ¬A,
donc Σ est contradictoire.
Maintenant supposons 2.15. Si Σ ` A, alors (1.2) Σ ∪ {¬A} est non satisfaisable. Par
2.15, donc Σ ∪ {¬A} est contradictoire, et donc par 2.9, Σ ∪ {¬A} |∼ A , et bien sûr on a
aussi Σ ∪ {A} |∼ A. Par 2.8, Σ |∼ A. 2