6. Déduction naturelle au premier ordre : quantificateurs, copie et égalité

En plus des règles du chapitre 3, nous ajoutons les règles concernant les quantificateurs, la copie et l'égalité. Notre système comporte toujours une seule règle pour enlever les hypothèses (la règle d'introduction de l'implication). Les définitions de brouillon de preuve, environnement, contexte, formule utilisable restent inchangées. Nous montrons la cohérence des règles de notre système, mais nous admettons sans preuve, que ce système est complet : des preuves de complétude pour des systèmes de règles similaires peuvent être trouvées dans les livres [2,11]. Contrairement au cas propositionnel, il n'y a aucun algorithme pour décider si une formule est valide ou non valide (preuve donnée par Alonzo Church et Alan Türing en 1936 et 1937 [4,24]). Autrement dit, en admettant l'équivalence entre prouvable (sans environnement) et valide, il n'y a pas d'algorithme qui, étant donné une formule, puisse nous en construire la preuve, ou nous avertir que cette formule n'a pas de preuve.

Plan :

Nous étendons d'abord les règles de la déduction naturelle proposées pour la logique propositionnelle. Nous présentons ensuite deux nouvelles tactiques pour aider à la rédaction de preuves. Enfin, nous prouvons la cohérence de notre système.

6.1 Règles pour la logique du premier ordre

Notre système de règles se divise en plusieurs familles de règles :

• les règles «propositionnelles»,
• les règles d'introduction et d'élimination de quantificateur,
• les règles régissant l'égalité,
• et une règle de copie.

L'ensemble des règles définies dans la section 3 peuvent être utilisées dans notre système de déduction. Nous renvoyons le lecteur à la table 3.1, qui récapitule l'ensemble de ces règles. Dans la suite de cette section, nous présentons uniquement les règles de déduction naturelle dédiées à la logique du premier ordre.

6.1.1 Règles des quantificateurs

L'ensemble des règles d'introduction et d'élimination de quantificateur est présenté dans la table 6.1. Dans cette table, A et B sont des formules, x est une variable, t est un terme. Notez que contrairement aux règles « propositionnelles», l'usage de ces nouvelles règles est contraint par des conditions d'emploi, qui utilisent les notions de variable libre (Définition 4.2.3) et de terme libre pour une variable (Définition 4.3.34).

Dans la suite, nous détaillons ces règles et nous illustrons leur usage sur des exemples et des contre-exemples montrant les erreurs occasionnées par le non respect des conditions d'emploi.

Tableau 6.1: Règles d'introduction et d'élimination des quantificateurs.

Règles	Conditions d'emploi
$\infer[\forall I]{\forall x A}{A}$
$\infer[\forall E]{A\!\!<\!\!x:=t\!\!>}{\forall x A}$
$\infer[\exists I]{\exists x A}{A\!\!<\!\!x:=t\!\!>}$
$\infer[\exists E]{B}{\exists x A & (A \Rightarrow B)}$

6.1.1.1 Règles pour le quantificateur universel

La règle d'élimination du quantificateur universel, notée ∀E, signifie que si la formule A est vraie pour toute valeur de x alors toute instance de A où x est remplacé par un terme t libre pour x est vraie. Notez que cette règle est une simple application du corollaire 4.3.38, page .

$\infer[\forall E]{A\!\!<\!\!x:=t\!\!>}{\forall x A}$

Nous justifions ci-dessous les conditions d'emploi de cette règle par un exemple montrant qu'un usage incorrect de la règle peut conduire à prouver une formule non-valide.

Exemple 6.1.1   Nous montrons qu'un usage incorrect de la règle ∀E conduit à «prouver» une formule non valide.

contexte	numéro	ligne	règle
1	1	Supposons ∀x∃yP(x, y)
1	2	∃yP(y, y)	∀E 1, y ERREUR
	3	Donc ∀x∃yP(x, y)⇒∃yP(y, y)

À la ligne 2, nous n'avons pas respecté les conditions d'applications de la règle ∀E car le terme y n'est pas libre pour x dans la formule ∃yP(x, y). Nous donnons une interprétation qui est un contre-modèle de la «conclusion» : soit I l'interprétation de domaine {0, 1} avec P_I =

La règle d'introduction du quantificateur universel, notée ∀I, signifie que si nous avons pu déduire la formule A indépendemment de la valeur de x, nous pouvons généraliser en déduisant ∀xA. Ainsi, il est nécessaire que x ne soit libre ni dans l'environnement de la preuve, ni dans le contexte de la ligne où nous avons déduit A.

$\infer[\forall I]{\forall x A}{A}$

Nous illustrons maintenant l'emploi de la règle d'introduction du quantificateur universel avec un exemple d'usage correct (exemple 6.1.2) et un exemple d'usage incorrect (exemple 6.1.3) de la règle.

Exemple 6.1.2   Nous prouvons ∀yP(y)∧∀yQ(y)⇒∀x(P(x)∧Q(x)).

contexte	numéro	ligne	règle
1	1	Supposons ∀yP(y)∧∀yQ(y)
1	2
1	3
1	4
1	5
1	6
1	7
	8	Donc ∀xP(x)∧∀xQ(x)⇒∀x(P(x)∧Q(x))	⇒I 1,7

Exemple 6.1.3   Nous montrons qu'un usage incorrect de la règle ∀I conduit à «prouver» une formule non valide.

contexte	numéro	ligne	règle
1	1	Supposons P(x)
1	2	∀xP(x)	∀I 1 ERREUR
	3	Donc P(x)⇒∀xP(x)	⇒I 1,2

À la ligne 2, nous n'avons pas respecté les conditions d'applications de la règle ∀I car la prémisse P(x) est établie dans le contexte P(x), ce qui interdit de généraliser sur x. Nous donnons un contre-modèle de la «conclusion » :

6.1.1.2 Règles pour le quantificateur existentiel

La règle d'élimination du quantificateur existentiel, notée ∃E, signifie que si ∃xA est vraie et que nous pouvons déduire A⇒B indépendemment de la valeur de x, alors nous pouvons déduire B, si la formule B ne dépend, elle non plus, de la valeur de x. Ainsi, il est nécessaire que x ne soit libre ni dans l'environnement de la preuve, ni dans B, et ni dans le contexte de la ligne A⇒B.

$\infer[\exists E]{B}{\exists x A & (A \Rightarrow B)}$

La condition d'emploi de cette règle étant complexe, nous illustrons l'emploi de la règle avec deux exemples d'usage incorrect.

Exemple 6.1.4   Nous montrons qu'un usage incorrect de la règle ∃E conduit à «prouver» une formule non valide.

contexte	numéro	ligne	règle
1	1	Supposons ∃xP(x)∧(P(x)⇒∀yQ(y))
1	2	∃xP(x)	∧E1 1
1	3	P(x)⇒∀yQ(y)	∧E2 1
1	4	∀yQ(y)	∃E 2,3 ERREUR
	5	Donc ∃xP(x)∧(P(x)⇒∀yQ(y))⇒∀yQ(y)	⇒I 1,4

Nous n'avons pas respecté la condition que le contexte de la prémisse P(x)⇒∀yQ(y) ne doit pas dépendre de x. Il est clair que la conclusion obtenue n'est pas valide. Nous donnons une assignation (I, e) qui est un contre-modèle de cette « conclusion» :

Exemple 6.1.5   Nous montrons qu'un usage incorrect de la règle ∃E conduit à «prouver» une formule non valide.

contexte	numéro	ligne	règle
1	1	Supposons ∃xP(x)
1,2	2	Supposons P(x)
1	3	Donc P(x)⇒P(x)	⇒I 2,2
1	4	P(x)	∃E 1,3 ERREUR
1	5	∀xP(x)	∀I 4
	6	Donc ∃xP(x)⇒∀x P(x)

La conclusion de la règle ∃E est P(x), contrairement à la condition d'application de cette règle qui impose que la conclusion ne doit pas dépendre de x. Nous donnons une interprétation qui est un contre-modèle de la cette «conclusion» :

La règle d'introduction du quantificateur existentiel, notée ∃I, signifie que si une instance de la formule A où x est remplacé par un terme t libre pour x est vraie, alors la formule ∃xA est vraie. Notez que cette règle est une simple application du corollaire 4.3.38, page . Ce qui justifie la condition d'emploi. Pour s'en convaincre, il suffit d'étudier l'exemple 4.3.37, qui précède le corollaire 4.3.38.

Ci-dessous, nous donnons un exemple d'usage correct de la règle d'introduction du quantificateur existentiel en démontrant l'une des lois de De Morgan.

Exemple 6.1.6 (Lois de De Morgan)   Nous montrons que pour toute formule A, ¬∀xA⇒∃x¬A.

contexte	numéro	ligne	règle
1	1	Supposons ¬∀xA
1,	2
1,	3
1,	4
1,	5
1,	6
1,	7
1,	8
1,	9
1	10
1	11
	12	Donc ¬∀xA⇒∃x¬A	⇒I 1,11

6.1.2 Copie

La règle de copie consiste à déduire d'une formule A, une autre formule A' égale au changement près des variables liées, au sens de la définition 4.4.5, page . Par exemple, ∀x∃yP(x, y) est une copie de ∀y∃xP(y, x).

${\frac{{A'}}{{A}}}$ Copie

Notez qu'il n'y pas de condition d'emploi pour cette règle.

6.1.3 Les règles de l'égalité

Deux règles caractérisent l'égalité : un terme est égal à lui-même (règle de la réflexivité) et si deux termes sont égaux, nous pouvons les remplacer l'un par l'autre (règle de la congruence).

$\infer[R\acute{e}flexivit\acute{e}]{t = t}{}$
$\infer[Congruence]{A\!\!<\!\!x:=t\!\!>}{s = t & A\!\!<\!\!x:=s\!\!>}$

Nous remarquons que la première règle n'a pas de prémisse. C'est ce que nous appelons aussi un axiome. Nous remarquons aussi que les conditions d'emploi de la deuxième règle sont similaires à celles des règles ∀E et ∃I. Ces conditions d'emploi se justifient de la même manière que précédemment.

Nous donnons maintenant deux exemples d'application des règles d'égalités.

Exemple 6.1.7   Prouvons que s = t⇒t = s, autrement dit prouvons que l'égalité est symétrique.

contexte	numéro	ligne	règle
1	1	Supposons s = t
1	2
1	3
	4	Donc s = t⇒t = s

Exemple 6.1.8   Prouvons que s = t∧t = u⇒s = u, autrement dit prouvons que l'égalité est transitive.

1	1	Supposons s = t∧t = u
1	2
1	3
1	4
	5	Donc s = t∧t = u⇒s = u

6.2 Tactiques de preuves

Nous instroduisons deux nouvelles tactiques pour l'application des règles ∀I et ∃E et nous illustrons ces tactiques avec un exemple.

6.2.1 Raisonner en avant avec une hypothèse d'existence

Soient Γ un ensemble de formules, x une variable, A et C des formules. Supposons que nous cherchons une preuve de C dans l'environnement Γ,∃xA.

1. Supposons que x n'est libre ni dans Γ, ni dans C. Dans ce cas, la preuve peut toujours s'écrire :

   Supposons A
   preuve de C dans l'environnement Γ, A
   Donc A⇒C	⇒I 1,_
   C	∃E

2. Supposons que x soit libre dans Γ ou C. Nous choisissons une variable y «nouvelle», c'est-à-dire non libre dans Γ, C et absente de A, puis nous nous ramenons au cas précédent, via la règle de copie. La preuve s'écrit alors :

   ∃yA < x : = y >	Copie de ∃xA
   Supposons A < x : = y >
   preuve de C dans l'environnement Γ, A < x : = y >
   Donc A < x : = y > ⇒C	⇒I 1,_
   C	∃E

La recherche de la preuve initiale a été réduite à la recherche d'une preuve dans un environnement plus simple. C'est exactement le mode de raisonnement appliqué dans les cours de mathématiques quand nous cherchons une preuve d'une formule C avec l'hypothèse ∃xP(x). Nous introduisons une constante «nouvelle» a vérifiant P(a) et nous prouvons C sous l'hypothèse P(a).

6.2.2 Raisonner en arrière pour généraliser

Nous reprenons les notations du paragraphe précédent. Supposons que nous cherchons une preuve de ∀xA dans l'environnement Γ.

1. Supposons que x n'est pas libre dans Γ. Dans ce cas, la preuve peut toujours s'écrire :

   preuve de A dans l'environnement Γ
   ∀xA	∀I

2. Supposons que x est libre dans Γ. Nous choisissons une variable y «nouvelle», c'est-à-dire non libre dans Γ, puis nous nous ramenons au cas précédent, via la règle de copie. La preuve s'écrit alors :

   preuve de A < x : = y > dans l'environnement Γ
   ∀yA < x : = y >	∀I
   ∀xA	Copie de la formule précédente

La recherche de la preuve initiale a été réduite à la recherche d'une preuve dans un environnement plus simple. C'est exactement le mode de raisonnement appliqué dans les cours de mathématiques quand nous cherchons une preuve de ∀xP(x). Nous introduisons une constante «nouvelle» a et nous prouvons P(a). Puis nous ajoutons : puisque le choix de a est arbitraire, nous avons ∀xP(x).

6.2.3 Un exemple d'application des tactiques

Nous notons «il existe un et un seul x » par ∃!x. Formellement, ∃!xP(x) signifie ∃x(P(x)∧∀y(P(y)⇒x = y)). En séparant l'existence de x et son unicité, nous pouvons aussi définir ∃!xP(x) par ∃xP(x)∧∀x∀y(P(x)∧P(y)⇒x = y). Ces deux définitions sont bien sûr équivalentes et nous montrons formellement que la première implique la deuxième. Comme la preuve est longue, il faut apprendre à décomposer les preuves.

Plan de la preuve

Nous appliquons les deux tactiques suivantes :

• Pour prouver A⇒B, supposer A et déduire B
• Pour prouver A∧B, prouver A et prouver B.

1	Supposons ∃x(P(x)∧∀y(P(y)⇒x = y))
	preuve de ∃xP(x) dans l'environnement de (1)
	preuve de ∀x∀y(P(x)∧P(y)⇒x = y) dans l'environnement de (1)
	∃xP(x)∧∀x∀y(P(x)∧P(y)⇒x = y)	∧I
	Donc ∃x(P(x)∧∀y(P(y)⇒x = y))⇒∃xP(x)∧∀x∀y(P(x)∧P(y)⇒x = y)	⇒I

Application de la tactique utilisant une hypothèse d'existence

Nous cherchons une preuve de ∃xP(x) dans l'environnement de ∃x(P(x)∧∀y(P(y)⇒x = y)). Nous appliquons la tactique «raisonner en avant en présence d'une hypothèse existentielle».

référence	formule
i	∃x(P(x)∧∀y(P(y)⇒x = y))
1	Supposons P(x)∧∀y(P(y)⇒x = y)
2	P(x)	∧E1 1
3	∃xP(x)	∃I 2, x
4	Donc P(x)∧∀y(P(y)⇒x = y)⇒∃xP(x)	⇒I 1,2
5	∃xP(x)	∃E i, 3

Application de la tactique pour obtenir une conclusion générale

Nous cherchons une preuve de ∀x∀y(P(x)∧P(y)⇒x = y) dans l'environnement de ∃x(P(x)∧∀y(P(y)⇒x = y)). Nous appliquons, dans l'ordre ci-dessous, les tactiques suivantes :

• «raisonner en avant en utilisant d'une hypothèse existentielle».
• Pour prouver A⇒B, supposer A et déduire B
• «raisonner en arrière pour obtenir une conclusion générale».

environnement
référence		formule
i		∃x(P(x)∧∀y(P(y)⇒x = y))
contexte	numéro	preuve	règle
1	1	Supposons P(x)∧∀y(P(y)⇒x = y)
1	2
1	3
1	4
1	5
1	6
1	7
1	8
1	9
1	10
1	11
1	12
1	13
1	14
1	15
	16	∀x∀y(P(x)∧P(y)⇒x = y)

La tactique «utiliser une hypothèse d'existence» sert à produire la ligne 16. La tactique «introduire une implication» sert à produire la ligne 15 : elle introduit l'hypothèse (1) dans laquelle x est une variable libre. Donc, pour appliquer la tactique « obtenir une conclusion générale», il faut changer de variable dès la ligne 2. Observer aussi que la formule, ligne 3, est instanciée aux lignes 5 et 8.

Comme sur cet exemple, toute la difficulté des preuves est concentrée autour des règles ∀E et ∃I :

• dans le raisonnement en avant, il faut trouver les bonnes instanciations des formules commençant par un quantificateur existentiel.
• dans le raisonnement en arrière, il faut trouver la bonne instance permettant de déduire une formule commençant par un quantificateur universel.

6.3 Cohérence du système

Nous commençons par montrer deux propriétés à propos des quantificateurs existensiel et universel. Enfin nous montrons la cohérence de notre système de déduction.

Propriété 6.3.1   Soient Γ un ensemble de formules, x une variable et A une formule. Supposons que x ne soit pas libre dans Γ, alors nous avons : Γ $\models$ A si et seulement si Γ $\models$ ∀xA.

Preuve :



$\Box$

Si nous observons d'un œil critique cette preuve, nous observons que c'est une paraphrase, dans un autre formalisme, de la loi ∀I. C'est l'équivalence ci-dessus, qui explique que la tactique «raisonner en arrière pour généraliser», est une tactique utilisable sans risque. En effet, en admettant la complétude du système, lorsque x n'est pas libre dans Γ, il y a une preuve de A dans l'environnement Γ si et seulement s'il a une preuve de ∀xA dans ce même environnement.

Propriété 6.3.2   Soient Γ un ensemble de formules, x une variable, A et B deux formules. Supposons que x ne soit libre ni dans Γ, ni dans B, alors nous avons : Γ $\models$ A⇒B si et seulement si Γ $\models$ (∃xA)⇒B

Preuve :

⇒

Supposons que Γ $\models$ A⇒B. Soit (I, e) une assignation modèle de Γ. Puisque x n'est pas libre dans Γ, pour tout état f identique à e sauf pour la valeur de x, (I, f ) et (I, e) donnent la même valeur aux formules de Γ, donc (I, f ) est modèle de Γ. Puisque Γ $\models$ A⇒B, pour tout état f identique à e sauf pour la valeur de x, (I, f ) est modèle de A⇒B. Supposons que (I, e) est modèle de ∃xA, il existe g identique à e sauf pour la valeur de x tel que (I, g) est modèle de A. Puisque pour tout état f identique à e sauf pour la valeur de x, (I, f ) est modèle de A⇒B, alors (I, g) est modèle de B. Puisque x n'est pas libre dans B, (I, e) est modèle de B.

⇐

Supposons que Γ $\models$ (∃xA)⇒B. Puisque la formule A⇒(∃xA) est valide (d'après le corollaire 4.3.38), nous avons Γ $\models$ A⇒B.

$\Box$

Si nous observons d'un œil critique cette preuve, nous voyons que c'est une paraphrase, dans un autre formalisme, de la loi ∃E. C'est l'équivalence ci-dessus, qui explique que la tactique «raisonner en avant avec une hypothèse d'existence», est une tactique utilisable sans risque. En effet, en admettant la complétude du système, lorsque x n'est libre ni dans Γ, ni dans B, il y a une preuve de B dans l'environnement Γ, A si et seulement s'il a une preuve de B dans l'environnement Γ,∃xA.

Théorème 6.3.3 (Cohérence de la déduction)   Si une formule est déduite d'un environnement de formules alors elle en est une conséquence.

Preuve : La preuve obéit au même plan que celle du même théorème dans le cas propositionnel (voir théorème 3.3.1) et nous en reprenons les notations en traitant uniquement le cas des nouvelles règles.

Soit Γ un ensemble de formules. Soit P une preuve de A dans cet environnement. Soient C_i la conclusion et H_i le contexte de la i-ème ligne de la preuve P. Rappelons que les lignes d'une preuve sont numérotées à partir de 1 et que H₀ est la liste vide.

Notons par Γ, H_i l'ensemble des formules de l'ensemble Γ et de la liste H_i. Supposons que pour tout i où 0 < i < k, Γ, H_i $\models$ C_i. Montrons que, pour 0 < k, Γ, H_k $\models$ C_k.

Nous examinons uniquement le cas des nouvelles règles et pour simplifier nous ne faisons pas de distinctions entre deux formules égales aux abréviations près de la négation et de l'équivalence.

• Supposons que C_k = ∀xA et que cette ligne ait été déduite, par la règle ∀I, de la formule A avec A = C_i et 0≤i < k ou A∈Γ. Si A = C_i et 0 < i < k, par hypothèse de récurrence nous avons, Γ, H_i $\models$ A. Si A∈Γ alors Γ $\models$ A. Puisque H₀ est la liste vide, il existe i où 0≤i < k tel que Γ, H_i $\models$ A. Vu les conditions d'application de la règle, x n'est pas libre dans Γ, H_i. Donc, d'après la propriété 6.3.1, nous avons aussi Γ, H_i $\models$ ∀xA. Puisque la ligne i est utilisable sur la ligne k - 1 et que H₀ est la liste vide, H_i est préfixe de H_k-1. Puisque le contexte n'est pas modifié par la ligne k, nous avons H_k-1 = H_k, donc Γ, H_k $\models$ C_k.

• Supposons que C_k = A < x : = t > et que cette ligne ait été déduite, par la règle ∀E, de la formule ∀xA avec ∀xA = C_i et 0 < i < k ou ∀xA∈Γ. Par hypothèse de récurrence ou parce que H₀ est la liste vide, il existe i où 0≤i < k tel que Γ, H_i $\models$ ∀xA. D'après les conditions d'application de la règle, le terme t est libre pour la variable x dans la formule A. Donc, d'après le corollaire 4.3.38, la formule ∀xA⇒A < x : = t > est valide et par suite Γ, H_i $\models$ A < x : = t >. Puisque la ligne i est utilisable sur la ligne k - 1, et que H₀ est la liste vide, H_i est préfixe de H_k-1. Puisque le contexte n'est pas modifié par la ligne k, nous avons H_k-1 = H_k, donc Γ, H_k $\models$ C_k.

• Supposons que C_k = ∃xA et que cette ligne ait été déduite, par la règle ∃I, de la formule A < x : = t > avec A < x : = t > = C_i et 0 < i < k ou A < x : = t > ∈Γ. Par hypothèse de récurrence ou parce H₀ est la liste vide, il existe i où 0≤i < k tel que Γ, H_i $\models$ A < x : = t >. D'après les conditions d'applications de la règle, le terme t est libre pour la variable x dans la formule A. Donc, d'après le corollaire 4.3.38, la formule A < x : = t > ⇒∃xA est valide et par suite Γ, H_i $\models$ ∃xA. Puisque la ligne i est utilisable sur la ligne k - 1, et que H₀ est la liste vide, H_i est préfixe de H_k-1. Puisque le contexte n'est pas modifié par la ligne k, nous avons H_k-1 = H_k, donc Γ, H_k $\models$ C_k.

• Supposons que C_k = B et que cette formule ait été déduite, par la règle ∃E, de la formule ∃xA avec ∃xA = C_i et 0 < i < k ou ∃xA∈Γ et de la formule A⇒B avec A⇒B = C_j et 0 < j < k ou A⇒B∈Γ. Par hypothèse de récurrence ou parce H₀ est la liste vide, il existe i et j tels que 0≤i < k, 0≤j < k, Γ, H_i $\models$ ∃xA et Γ, H_j $\models$ A⇒B. Vu les conditions d'application de la règle, x n'est libre ni dans Γ, H_j, ni dans B. Donc, d'après la propriété 6.3.2, nous avons aussi Γ, H_j $\models$ (∃xA)⇒B. Puisque les lignes i et j sont utilisables sur la ligne k - 1, et que H₀ est la liste vide, H_i et H_j sont préfixes de H_k-1. Puisque le contexte n'est pas modifié par la ligne k, nous avons H_k-1 = H_k, donc Γ, H_k $\models$ ∃xA et Γ, H_k $\models$ (∃xA)⇒B. Par suite Γ, H_k $\models$ C_k.
• Supposons que C_k = A' et que cette formule ait été déduite, par la règle de copie de la formule A avec A = C_i et 0 < i < k ou A∈Γ. Par hypothèse de récurrence ou parce H₀ est la liste vide, il existe i tel que 0≤i < k, Γ, H_i $\models$ A. Puisque, d'après le théorème 4.4.6, les formules A et A' sont équivalentes, nous avons Γ, H_i $\models$ A'. Puisque la ligne i est utilisable sur la ligne k - 1, et que H₀ est la liste vide, H_i est préfixe de H_k-1. Puisque le contexte n'est pas modifié par la ligne k, nous avons H_k-1 = H_k, donc Γ, H_k $\models$ C_k.

• Supposons que C_k = (t = t). Puisque cette formule est valide (dans le sens attribué à l'égalité), Γ, H_k $\models$ C_k.

• Supposons que C_k = A < x : = t > et que cette ligne ait été déduite, par la règle de congruence, de la formule s = t avec (s = t) = C_i et 0 < i < k ou (s = t)∈Γ et de la formule A < x : = s > avec A < x : = s > = C_j et 0 < j < k ou A < x : = s > ∈Γ. Par hypothèse de récurrence ou parce H₀ est la liste vide, il existe i et j tels que 0≤i < k, 0≤j < k, Γ, H_i $\models$ (s = t) et Γ, H_j $\models$ A < x : = s >. Puisque les lignes i et j sont utilisables sur la ligne k - 1, et que H₀ est la liste vide, H_i et H_j sont préfixes de H_k-1. Puisque le contexte n'est pas modifié par la ligne k, nous avons H_k-1 = H_k, donc Γ, H_k $\models$ (s = t) et Γ, H_k $\models$ A < x : = s >. D'après le théorème 4.3.36 et les conditions d'application de la règle, nous avons : s = t, A < x : = s > $\models$ A < x : = t >. Par suite Γ, H_k $\models$ C_k.

$\Box$