3  Arithmétique de Peano-Heyting

Si l’on peut noter les preuves de la logique propositionnelle par des λ-termes typés, éventuellement légèrement étendus, on peut faire de même pour des logiques plus expressives, incluant notamment des quantifications (∀, ∃) et des principes de récurrence.

3.1  Logique du premier ordre

Nos formules, ou types, seront dans cette section non plus des formules propositionnelles mais des formules du premier ordre. Les types de base, ou formules atomiques, ne seront plus nécessairement de simples lettres b, mais de la forme P (t₁, …, t_n), où P est un symbole de prédicat, et où t₁, …, t_n sont n termes. Si n=0, on retrouve le cas de la logique propositionnelle, et nous noterons P au lieu de P (). Les termes servent à dénoter des valeurs sur lesquelles nous voulons raisonner. En arithmétique par exemple, les termes dénoteront des entiers naturels, et notre seul symbole de prédicat sera l’égalité ≈ (que nous notons ainsi pour ne pas confondre ce symbole avec la relation d’égalité =). Nous écrirons d’ailleurs par confort t₁ ≈ t₂ plutôt que ≈ (t₁, t₂). Si les formules atomiques sont décrites à l’aide de symboles de prédicats, les termes sont décrits à l’aide de variables i, j, k, …, sur lesquelles on pourra quantifier, et de symboles de fonctions f, g, h, … En arithmétique par exemple, + sera un symbole de fonction binaire, et on notera t₁ + t₂ au lieu de + (t₁, t₂); 0 sera un symbole de fonction nullaire (sans argument), c’est-à-dire une constante.

En général, un langage L du premier ordre est la donnée d’une famille d’ensembles F_n dits de symboles de fonctions d’arité n, et d’une famille d’ensembles P_n dits de symboles de prédicats d’arité n, tous ces ensembles étant disjoints deux à deux. Étant donné un ensemble X dit de variables, l’ensemble T ( L, X) des termes de L à variables dans X est le plus petit tel que:

• toute variable dans X est dans T ( L, X);
• pour tout n∈ N, tout f ∈ F_n, tous t₁, …, t_n ∈ T ( L, X), le terme f (t₁, …, t_n) est dans T ( L, X) (où f (t₁, …, t_n) est une notation pour le (n+1)-uplet (f, t₁, …, t_n)).

En d’autres termes, T ( L, X) est le langage T défini par la grammaire:

Les formules atomiques sont les P (t₁, …, t_n), où P ∈ P_n et t₁, …, t_n ∈ T ( L, X) (ceci représentant encore un (n+1)-uplet (P, t₁, …, t_n)).

Les formules F sont définies par la grammaire suivante, où A désigne n’importe quelle formule atomique:

Comme avant, on définit ¬ F par F ⇒ ⊥. La variable i dans ∀ i · F est liée par ∀, et nous supposons que ∀ i · F et ∀ j · (F [i:=j]) dénotent la même formule, lorsque j n’est pas libre dans F. On a ici exactement les mêmes difficultés pour définir les variables libres dans une formule ou un terme, l’α-renommage entre formules, et la notion de substitution de termes à des variables dans des termes ou formules, que dans le λ-calcul pur. Nous supposerons donc le problème réglé.

De même que nous avons étendu le langage des types, nous étendons le langage NJf des preuves par les règles suivantes, où t est un terme quelconque dans (∀ E):

On obtient ainsi le système NJf₁ de logique minimale du premier ordre.

La condition sur i dans la règle (∀ I) est indispensable. Si on ne l’imposait pas, on pourrait, à partir de P (i) ⊢ P (i), déduire P (i) ⊢ ∀ i · P (i) par (∀ I), c’est-à-dire pour plus de clarté P (i) ⊢ ∀ j · P (j), et à partir de là:

par exemple, ce qui est absurde: ceci signifie que si P est vraie de 0, alors P est vraie de toute valeur, et ceci pour n’importe quelle propriété P.

On veut trouver des constructions étendant le λ-calcul permettant de donner des termes de preuves pour les nouvelles règles. Une façon simple de faire est de considérer qu’une preuve de ∀ i · P (i) est une fonction qui à une valeur de i associe une preuve de P (i). Il n’y a donc quasiment pas à étendre le langage: si u est une preuve de P (i), nous prendrons λ i · u comme preuve de ∀ i · P (i): (∀ I) introduira donc un λ, comme (⇒ I), et de même (∀ E) appliquera un λ-terme à un terme du premier ordre.

Pour ceci, on enrichit le λ-calcul par des termes du premier ordre:

Pour qu’il n’y ait aucune ambiguïté, on supposera qu’aucun terme du premier ordre ne peut être confondu avec un λ-terme ordinaire, en particulier que X ne contient aucune des variables du λ-calcul ordinaire, dans V. Et les règles supplémentaires de NJf₁ par rapport à NJf sont les suivantes, où t est un terme et i ∈ X:

Les règles de calcul sont celles de NJf, soit celles du λ∇-calcul:

où dans (β₁) i ∈ X et t ∈ T ( L, X).

Preuve : Comme au lemme 1. Le cas suivant que nous devons traiter est celui d’un (β₁)-redex:

et nous devons montrer que l’on peut transformer la preuve π₁ en une dérivation de Γ ⊢ u [i:=t] : F [i:=t], sachant que i n’est libre dans aucune des formules de Γ. Pour ceci, il suffit de montrer le lemme auxiliaire suivant:

Preuve : On montre le résultat par récurrence sur la preuve donnée π de x₁ : F₁, …, x_n : F_n ⊢ u : F. Plus généralement, montrons que l’on peut produire une preuve de x₁ : F₁ [i:=t], …, x_n : F_n [i:=t] ⊢ u [i:=t] : F [i:=t] de même taille que π. Il n’y a aucune difficulté, sauf éventuellement lorsque la preuve se termine par une règle (∀ I). Alors u est de la forme λ j · v et F est de la forme ∀ j · G, et on a dérivé x₁ : F₁, …, x_n : F_n ⊢ u : F à partir d’une preuve π₁ de x₁ : F₁, …, x_n : F_n ⊢ v : G plus courte que π, où j n’est pas libre dans F₁, …, F_n. Notons que j peut être libre dans t. Soit k une variable qui n’est ni libre dans F₁, …, F_n, ni dans t, ni dans v. Par hypothèse de récurrence, on produit une preuve π′₁ de x₁ : F₁ [j:=k], …, x_n : F_n [j:=k] ⊢ v [j:=k] : G [j:=k], c’est-à-dire de x₁ : F₁, …, x_n : F_n ⊢ v [j:=k] : G [j:=k]. Comme π′₁ est de même taille que π₁, on peut encore appliquer l’hypothèse de récurrence et produire une preuve π″₁ de x₁ : F₁ [i:=t], …, x_n : F_n [i:=t] ⊢ v [j:=k] [i:=t] : G [j:=k] [i:=t]. Comme k n’est pas libre dans F₁ [i:=t], …, F_n [i:=t] par construction (au contraire de j qui pourrait être libre dans t), on en déduit une preuve π′ de x₁ : F₁ [i:=t], …, x_n : F_n [i:=t] ⊢ λ k · (v [j:=k] [i:=t]) : ∀ k · (G [j:=k] [i:=t]) par (∀ I), qui est de même taille que π. Il ne reste qu’à observer que, à α-renommage près, λ k · (v [j:=k] [i:=t]) est (λ j · v) [i:=t] et que ∀ k · (G [j:=k] [i:=t]) est (∀ j · G) [i:=t], c’est-à-dire F [i:=t].     ♦

    ♦

Preuve : C’est la même preuve qu’au théorème 2. Il suffit de modifier la définition des termes réductibles au type F du théorème 1. Pour ceci, on définit RED_ι comme étant l’ensemble des termes fortement normalisants du premier ordre—c’est-à-dire de tous les termes du premier ordre. D’autre part, RED_{∀ i · F} est défini comme l’ensemble des λ-termes u tels que pour tout t ∈ RED_ι, ut ∈ RED_{F [i:=t]}. Cette définition de RED_F est toujours une définition valide, cette fois-ci non pas sur la structure de F, mais sur la structure du squelette Sk (F) de F. On définit ce squelette par: Sk (A) =_def * pour toute formule atomique A, où * est un symbole fixé, Sk (F ⇒ G) =_def Sk (F) ⇒ Sk (G), Sk (∀ i · F) =_def ∀ i · Sk (F). Il est nécessaire de passer par le squelette: dans la définition de RED_{∀ i · F} en fonction de RED_{F [i:=t]}, F [i:=t] n’est pas en général une sous-expression de ∀ i· F; par contre, Sk (F [i:=t]) = Sk (F) est une sous-expression stricte de Sk (∀ i · F) = ∀ i · Sk (F), ce qui justifie la récurrence utilisée dans la définition.

La preuve du théorème se déroule ensuite comme au théorème 1, modifié comme au théorème 2, sans différence essentielle.

Mais il y a une façon plus simple d’établir le même résultat, qui consiste à effacer toute information du premier ordre dans les types et les λ-termes. Le slogan ici est que, du point de vue de la réduction des preuves, tout ce qui est terme et quantification du premier ordre ne sert à rien.

La fonction d’effacement sur les formules est définie par:

et fournit donc des types simples à partir de formules, où les types de base sont simplement les symboles de prédicats. Sur les termes, on définit:

où t est un terme du premier ordre. Il est facile de voir que si Γ ⊢ u : F est dérivable en NJf₁, alors E (Γ) ⊢ E (u) : E (F) est dérivable en NJf, où E (Γ) est défini par E (x₁:F₁, …, x_n:F_n) =_def x₁ : E (F₁), …, x_n : E (F_n). D’autre part, si u → v par (β) ou (∇), alors E (u) → E (v) par (β) ou (∇) respectivement; et si u → v par (β₁), alors E (u) = E (v). Donc s’il existe une réécriture infinie partant d’un terme u typé en NJf₁, alors comme toute réduction partant de E (u) est finie par le théorème 2, c’est qu’il existe un réduit v de u à partir duquel on peut mener une réduction infinie en n’utilisant que la règle (β₁). Mais cette règle fait diminuer de 1 le nombre d’applications de λ-termes à des termes du premier ordre, et ne peut donc être appliquée qu’un nombre fini de fois à la suite. (Les termes du premier ordre ne contiennent aucun rédex susceptible d’être dupliqué par β₁-réduction, contrairement à ce qui se passe avec la β-réduction.) D’où le théorème. Formellement, un argument rigoureux consiste à ordonner les termes u en comparant les couples (E (u), #1 (u)), où #₁ (u) est le nombre d’applications de λ-termes à des termes du premier ordre dans u, dans le produit lexicographique de →⁺ et >.     ♦

Preuve : Exactement comme au Corollaire 3.     ♦

Il n’y a donc pas de contradiction en logique intuitionniste du premier ordre.

Un point qui se dégage ici est que le quantificateur universel se comporte presque exactement comme l’implication. Ceci peut être formalisé en utilisant des types dépendants. Ceci a aussi le mérite de rendre plus esthétique le système de types de ND₁. On aboutit ainsi à une logique qui s’appelle LF, dans laquelle le constructeur fondamental de types n’est plus l’implication ⇒ mais le produit dépendant Π x : F₁ · F₂. Les termes du premier ordre sont codés comme des λ-termes d’un type spécial que l’on notera ι. Lorsque F₁ = ι, Π x : ι · F représente ∀ x· F, et lorsque F₁ est une formule et x n’est pas libre dans F₂, Π x : F₁ · F₂ représente F₁ ⇒ F₂. Consulter [HHP87] pour plus de renseignements sur LF.

3.2  Arithmétique de Heyting

L’arithmétique de Peano est la façon usuelle de formaliser l’ensemble des entiers naturels N et ses propriétés. Il s’agit d’une théorie du premier ordre, dont les symboles de fonction sont 0 (constante, représentant 0), S (fonction unaire, dénotant la fonction qui à n associe n+1), + et * (fonctions binaires dénotant l’addition et la multiplication respectivement), et dont le seul symbole de prédicat est ≈, qui est binaire. Le type ι dénote l’ensemble des entiers naturels, et les axiomes de Peano sont:

1. ∀ i · i ≈ i (réflexivité de l’égalité);
2. ∀ i · ∀ j · i ≈ j ⇒ F ⇒ F [i:=j] (remplacement des équivalents: on peut toujours remplacer i par un j égal à i dans toute formule F);
3. ∀ i · ¬ 0 ≈ S (i);
4. ∀ i · ∀ j · S (i) ≈ S (j) ⇒ i ≈ j;
5. ∀ i · i + 0 ≈ i (définition de l’addition, 1);
6. ∀ i · ∀ j · i + S (j) ≈ S (i + j) (définition de l’addition, 2);
7. ∀ i · i * 0 ≈ 0 (définition de la multiplication, 1);
8. ∀ i · i * S (j) ≈ i * j + i (définition de la multiplication, 2);

plus le schéma de récurrence:

qui exprime qu’une propriété F (i) est vraie pour tout i dès qu’elle est vraie en i=0 et que F (i) implique F (i+1).

La version intuitionniste de cette théorie s’appelle l’arithmétique de Heyting, et a les mêmes axiomes qui ci-dessus, mais est codée comme une extension de NJf₁ plutôt que ND₁. Nous étudions l’arithmétique de Heyting parce que les transformations de preuve seront un peu plus simples que dans l’arithmétique de Peano.

La principale difficulté ici est de trouver une nouvelle construction de λ-termes interprétant le schéma de récurrence. Intuitivement, il s’agit d’un terme R de type le schéma de récurrence lui-même. Si u est un terme de type F [i:=0], si v est un terme de type ∀ j · F [i:=j] ⇒ F [i:=S (j)], c’est-à-dire une fonction qui prend un entier j en argument, un autre argument de type F [i:=j] et retourne un terme de type F [i:=S (j)], alors les règles de réduction suivantes semblent raisonnables, parce qu’elles satisfont la propriété d’auto-réduction, autrement ce sont des transformations de preuves correctes. D’abord, R u v 0 → u; ensuite, R u v (S (j)) → v (S (j)) (R u v j).

Ce qui est intéressant, d’un point de vue calculatoire, c’est que R u v définit une fonction de type ∀ i · F, des entiers i vers des preuves de F, cette fonction g étant définie par les règles: g (0) → u, g (S (j)) → v (S (j)) (g (j)). La fonction g est définie par cas: son argument est soit 0 soit un successeur. De plus, la définition de g est récursive, mais il n’y a qu’un appel récursif à g, et g (j+1) est définie en fonction de g (j) uniquement. Une telle définition s’appelle une définition par récurrence primitive, et g est une fonction primitive récursive.

Nous allons aussi ajouter un terme r₀ de type 0 ≈ 0, pour modéliser en partie l’axiome 1, mais il est beaucoup plus naturel de ne pas ajouter de termes pour représenter les autres axiomes de Peano. À la place, on va définir une relation de simplification des formules de l’arithmétique par:

Ceci est l’approche naturelle en Coq [BBC⁺99], et est aussi une instance de déduction modulo [DHK98].

Notons ↔_N^* la plus petite relation réflexive symétrique et transitive contenant →_N: ceci va nous permettre de considérer deux formules en relation par la relation d’équivalence ↔_N^* comme interchangeables.

Les termes de preuves de l’arithmétique de Heyting du premier ordre sont les λ∇ R-termes, définis par la grammaire suivante, où T est T ( L, X) et L est le langage contenant les symboles ≈, 0, S, + et * comme décrit plus haut:

Les règles de HA₁, l’arithmétique de Heyting du premier ordre, sont alors les suivantes:

L’originalité de ce système est la règle (↔_N^*), qui permet de remplacer une formule par une formule équivalente; pas n’importe quelle formule équivalente, d’ailleurs, juste une qui est calculatoirement équivalente, où l’équivalence calculatoire est définie par les règles de calcul →_N. On a ici deux niveaux de calculs: un dans les formules, par →_N, et un dans les preuves, par les règles de réduction de notre λ∇ R-calcul. Ces règles sont les suivantes (noter que les quatre dernières sont aussi des règles de →_N):

L’axiome 1 se démontre à l’aide de la règle (0 ≈ 0) et du schéma de récurrence (Rec). Intuitivement, la preuve est la suivante. Montrons s ≈ s par récurrence sur s. Le cas de base est 0 ≈ 0, ce qui est démontré par la règle (Refl₀). Le cas récurrent demande à établir S (s) ≈ S (s) sous l’hypothèse s ≈ s. Mais la conclusion S (s) ≈ S (s) est équivalente à l’hypothèse, à cause de la règle de calcul (S ≈ S). Formellement:

Le schéma d’axiomes de remplacement des équivalents 2 peut lui aussi entièrement se démontrer dans HA₁, ou plutôt chacune de ses instances peut se démontrer en HA₁ (cf. exercice 27). On dit que ce schéma est admissible en HA₁.

Exercice 27 ()  

1. Montrer que le terme λ x · x est un terme de preuve de s ≈ t ⇒ S (s) ≈ S (t).
2. Montrer qu’on peut démontrer s₁ ≈ t₁ ⇒ s₂ ≈ t₂ ⇒ s₁ + s₂ ≈ t₁ + t₂, par récurrence sur l’entier s₂ puis sur l’entier t₂. (Les courageux montreront que R u (λ j · λ z · v) s₂ en est un terme de preuve, où u =_def R (λ x · λ y · x) (λ t₂ · λ z₁ · λ x · λ y · ∇ y) t₂ : s₁≈ t₁ ⇒ 0≈ t₂ ⇒ s₁≈ t₁ + t₂ et v =_def R (λ x · λ y · ∇ y) (λ t₂ · λ z₂ · z) t₂ : s₁≈ t₁ ⇒ S (j) ≈ t₂ ⇒ S (s₁ + j)≈ t₁ + t₂ dans le contexte z : s₁ ≈ t₁ ⇒ s₂ ≈ t₂ ⇒ s₁ + s₂ ≈ t₁ + t₂.)
3. Montrer qu’on peut démontrer s₁ ≈ t₁ ⇒ s₂ ≈ t₂ ⇒ s₁ * t₁ ≈ s₂ * t₂, par récurrence sur s₂ puis sur t₂, en utilisant le point précédent.
4. En déduire que pour tout terme t, on peut montrer s₁ ≈ s₂ ⇒ t [i:=s₁] ≈ t [i:=s₂]. (Appliquer une récurrence structurelle sur t — pas une récurrence (Rec) sur la valeur entière de t, notez bien.)
5. Montrer qu’on peut démontrer la symétrie de l’égalité en HA₁: ∀ i · ∀ j · i ≈ j ⇒ j ≈ i. (Appliquer une récurrence sur i, et dans chaque cas appliquer une récurrence sur j et simplifier par →_N. Bonus si vous arrivez à montrer qu’un terme de preuve possible est λ i · R (λ j · R  id₀ (λ i · λ x · id_⊥) j) (λ i · λ y · R  id_⊥(λ k · λ z · yk) j) i, où id₀ est le terme λ x₀ · x₀ de type 0 ≈ 0 ⇒ 0 ≈ 0 et id_⊥ est le terme λ x₁ · x₁ de type ⊥ ⇒ ⊥.)
6. Montrer qu’on peut démontrer la transitivité de l’égalité en HA₁: ∀ i · ∀ j · ∀ j · i≈ j ⇒ j ≈ k ⇒ i≈ k. (Indication: effectuer des récurrences sur i, j, k imbriquées dans cet ordre. Bonus si vous arrivez à fournir un terme de preuve explicite !)
7. Déduire des points 4, 5 et 6 que l’on peut montrer s₁ ≈ t₁ ⇒ F [i:=s₁] ⇒ F [i:=t₁] pour toute formule F qui est une égalité s≈ t.
8. En déduire que l’on peut montrer s₁ ≈ t₁ ⇒ F [i:=s₁] ⇒ F [i:=t₁] pour toute formule F, par récurrence structurelle sur F. En conséquence, toute instance du principe de remplacement des équivalents est démontrable en HA₁.

À cause de la règle (↔_N^*), la propriété d’auto-réduction est plus compliquée à démontrer qu’avant. Le lemme d’affaiblissement (cf. lemme 2) est toujours aussi facile. Par contre, le lemme suivant est plus difficile:

Preuve : Plus généralement, soit π₂ une preuve de Γ, x : F₁, Δ ⊢ u : F₂ et π₁ une de Γ ⊢ v : F₁. On construit une preuve π de Γ, Δ ⊢ u [x:=v] : F₂ par récurrence structurelle sur π₂.

Si π₂ se termine par la règle (Ax), alors soit u est x, donc F₁ = F₂, et on prend pour π un affaiblissement idoine de π₁, soit u est une autre variable y et π est la preuve qui produit Γ, Δ ⊢ y : F₂ par (Ax). Si π₂ se termine par (⇒ E) ou (⇒ I), c’est comme au lemme 1, cas (App) et (Abs). Les cas où π₂ se terminent par (⊥ E), (∀ E), (∀ I) sont faciles. Si π₂ se termine par (Refl₀), alors u = r₀ et u [x:=v] est encore r₀: on définit π comme la preuve qui déduit Γ, Δ ⊢ r₀ : 0 ≈ 0 par (Refl₀).

Si π₂ se termine par (↔_N^*), alors on a dérivé Γ, x : F₁, Δ ⊢ u : F₂ à partir d’une preuve plus courte de Γ, x : F₁, Δ ⊢ u : F′₂, avec F₂ ↔_N^*F′₂. Par hypothèse de récurrence, on a une preuve de Γ, Δ ⊢ u [x:=v] : F′₂, d’où l’on déduit une de Γ, Δ ⊢ u [x:=v] : F₂ par (↔_N^*).

Si π₂ se termine par (Rec), alors on a dérivé Γ, x : F₁, Δ ⊢ u : G [i:=t], avec F₂ = G [i:=t] et u = R u′ v′ t, à partir de preuves plus courtes de Γ, x : F₁, Δ ⊢ u′ : G [i:=0] et de Γ, x : F₁, Δ ⊢ v′ : ∀ j · G [i:=j] ⇒ G [i:=S (j)]. Par hypothèse de récurrence, on peut déduire Γ, Δ ⊢ u′ [x:=v] : G [i:=0] et Γ, Δ ⊢ v′ [x:=v] : ∀ j · G [i:=j] ⇒ G [i:=S (j)], donc Γ, Δ ⊢ u : G [i:=t].     ♦

L’auto-réduction exprime alors que les règles de réduction de HA₁ sont bien des règles de transformations de preuves de séquents en des preuves des mêmes séquents:

Preuve : Le cas de la règle (β) est par le lemme 12. Celui de la règle (β₁) est comme au lemme 11. Le cas de (∇) est évident. La règle (R0) correspond à réécrire la preuve:

en π, et (RS) correspond à réécrire la preuve:

en:

    ♦

Preuve : Montrons d’abord que tout terme t du premier ordre termine. Interprétons les termes t dans les entiers par: [0] =_def 1, [S (t)] =_def [t]+1, [s + t] =_def [s] + 2 [t], [s * t] =_def [s] (3[t]+1). Nous montrons que: (*) si t₁ → t₂, alors [t₁] > [t₂]; ceci impliquera qu’il ne peut exister aucun réduction infinie à partir de t₁. On montre (*) par récurrence sur la profondeur du rédex contracté dans t₁. Si t₁ est lui-même le rédex, remarquons que [s + 0] = [s] + 2 > [s], [s + S (t)] = [s] + 2[t] + 2 > [s] + 2[t] + 1 = [S (s + t)], [s * 0] = 4 [s] > 1 = [0] (car [s]≥ 1 pour tout s, comme une récurrence facile sur s le montre), et [s * S (t)] = [s] (3[t]+4) > [s] (3 [t] + 3) = [s] (3 [t] + 1) + 2 [s] = [s * t + s]. Si t₁ n’est pas lui-même le rédex, alors c’est par l’hypothèse de récurrence. Par exemple, si t₁ est de la forme S (t′₁), avec t′₁ → t′₂ et t₂ = S (t′₂), alors [t₁] = [t′₁]+1 > [t′₂]+1 = [t₂].

Un λ∇ R-terme est dit neutre s’il ne commence pas par λ ou ∇. Soit SN l’ensemble des λ∇ R-termes fortement normalisants, RED_⊥ et RED_{s≈ t} sont définis comme étant SN, RED_{F ⇒ G} est l’ensemble des λ∇ R-termes u tels que pour tout v ∈ RED_F, uv ∈ RED_G, et RED_{∀ i · F} est l’ensemble des λ∇ R-termes u tels que pour tous termes t du premier ordre (qui terminent), ut ∈ RED_{F [i:=t]}. Ceci est une définition de RED_F par récurrence structurelle sur le squelette Sk (F) de F. Comme d’habitude, montrons:

• (CR1) Si u ∈ RED_F, alors u ∈ SN.
• (CR2) Si u ∈ RED_F et u → u′, alors u′∈ RED_F.
• (CR3) Si u est neutre et pour tout u′ tel que u → u′, u′ ∈ RED_F, alors u ∈ RED_F.

Ceci est par récurrence structurelle sur Sk (F). Si F est de la forme ⊥ ou s≈ t, ces propriétés sont évidentes. Si F est de la forme G ⇒ H, alors si u ∈ RED_F, pour tout v ∈ RED_G, uv ∈ RED_H, donc par hypothèse de récurrence (CR1), uv ∈ SN; par hypothèse de récurrence (CR3), la variable x de type G est dans RED_G, donc ux ∈ SN; donc u ∈ SN: (CR1) est vraie. Si u ∈ RED_F et u → u′, par définition pour tout v∈ RED_G, uv ∈ RED_H et de plus uv → u′v, donc par hypothèse de récurrence (CR2) u′v ∈ RED_H; comme v est arbitraire, u′ ∈ RED_H, établissant (CR2). Si u est neutre et pour tout u′ tel que u → u′, u′ ∈ RED_F, montrons que pour tout v∈ RED_G, uv ne se réduit qu’à des termes de RED_H. C’est par récurrence sur ν (v). Comme u est neutre, uv ne se réduit qu’à des termes de la forme u′v avec u → u′ (donc u′v ∈ RED_H car par hypothèse u′ ∈ RED_F) ou de la forme uv′ avec v → v′ (donc uv′ ∈ RED_H par hypothèse de récurrence). Comme uv est lui-même neutre, par hypothèse de récurrence (CR3), u ∈ RED_F, ce qui établit (CR3).

On montre maintenant que:

par récurrence structurelle sur u. Ceci impliquera le théorème. Si u est une variable, une application ou une abstraction, c’est comme au théorème 1. Si u est de la forme ∇ v, alors c’est comme au théorème 2.

Le cas intéressant est celui où u est de la forme R v w t, et découle du résultat auxiliaire: (∘) si v ∈ RED_{F [i:=0]} et w ∈ RED_{∀ j · F[i:=j] ⇒ F[i:=S (j)]}, alors R v w t ∈ RED_{F [i:=t]}. Nous montrons (∘) par récurrence sur ν (v) + ν (w) + [t]. Notons que R v w t est neutre, donc par (CR3) il suffit de montrer que tous les réduits immédiats de R v w t sont dans RED_{F [i:=t]}. Mais R v w t ne peut se réduire qu’en R v′ w t avec v → v′ (qui est dans RED_{F [i:=t]} par hypothèse de récurrence), ou en R v w′ t avec w → w′ (idem), en R v w t′ avec t → t′ (donc t →_Nt′, en particulier [t] > [t′] et l’hypothèse de récurrence s’applique), ou en v si t = 0 (auquel cas v ∈ RED_{F [i:=0]} = RED_{F [i:=t]}), ou en w t′ (R v w t′) avec t = S (t′): dans ce dernier cas, [t] = [t′]+1, donc [t′] < [t], donc l’hypothèse de récurrence s’applique et R v w t′ ∈ RED_{F [i:=t′]}; par définition de la réductibilité, w t′ (R v w t′) est dans RED_{F [i:=S (t′)]} = RED_{F [i:=t]}.     ♦

Preuve : Supposons que u soit un terme normal tel que ⊢ u : ⊥ soit dérivable. On peut supposer sans perte de généralité que u ne contient aucune variable libre du premier ordre, car si i₁, …, i_k sont ces variables, alors ⊢ u [i₁:=0, …, i_k:=0] : ⊥ est dérivable, et on peut remplacer u par toute forme normale de u [i₁:=0, …, i_k:=0], qui n’a aucune variable variable libre du premier ordre.

Supposons donc que u est un terme normal sans variable libre du premier ordre tel que ⊢ u : ⊥ soit dérivable, de taille minimale. Alors u est nécessairement de la forme h u₁ … u_n, où h est une variable ou le symbole ∇ (auquel cas n=1), ou de la forme R u₁ u₂ t. Le premier cas est impossible car le côté gauche du jugement est vide. Le second cas implique que ⊢ u₁ : ⊥, ce qui contredit la minimalité de u. Dans le dernier cas, t étant normal et sans variable libre, t est de la forme S (… (S (0))); c’est par récurrence structurelle sur t: si t = 0, c’est clair; si t est de la forme S (t₁), c’est par hypothèse de récurrence; et t ne peut pas être ni de la forme t₁ + t₂ ni de la forme t₁ * t₂, car par hypothèse de récurrence t₂ commencerait par 0 ou par S, ce qui contredirait l’hypothèse de normalité de t. Mais comme t = S (… (S (0))), R u₁ u₂ t n’est pas normal, ce qui montre que le dernier cas est impossible lui aussi.     ♦

Ceci est le premier résultat de cohérence non complètement trivial que nous avons démontré. Il peut apparaître trivial, cependant, et en voici une démonstration élémentaire. Pour toute fonction ρ de X vers N (une valuation du premier ordre), pour tout terme t, définissons [t] ρ par: [0] ρ =_def 0, [S (t)] ρ =_def [t] ρ + 1, [s + t] ρ =_def [s] ρ + [t] ρ, [s * t] ρ =_def [s] ρ × [t] ρ. Définissons la relation ρ ⊨ F (“F est vraie dans la valuation ρ”) par: ρ ⊨ ⊥ est faux, ρ ⊨ s ≈ t si et seulement si [s] ρ = [t] ρ, ρ ⊨ F ⇒ G si et seulement si ρ ⊨ F implique ρ ⊨ G, et ρ ⊨ ∀ i · F si et seulement si ρ [i:=n] ⊨ F pour tout n∈ N, où ρ [i:=n] envoie i vers n et toute autre variable j vers ρ (j). Il est facile de voir que pour toute preuve de x₁:F₁, …, x_n:F_n ⊢ u:F, pour toute valuation ρ, ρ ⊨ F₁ et … et ρ ⊨ F_n impliquent ρ ⊨ F. HA₁ est alors cohérent parce que par exemple ⊢ u : ⊥ n’est prouvable pour aucun λ∇ R-terme u, sinon ρ ⊨ ⊥ serait vrai.

Cette démonstration sémantique est beaucoup plus simple que la démonstration syntaxique par normalisation des λ∇ R-termes typés, mais en fait elle ne dit pas grand-chose: pour démontrer que pour toute preuve de x₁:F₁, …, x_n:F_n ⊢ u:F, pour toute valuation ρ, ρ ⊨ F₁ et … et ρ ⊨ F_n impliquent ρ ⊨ F, nous utilisons les règles usuelles de l’arithmétique. Autrement dit, on utilise essentiellement les mêmes règles que celles de HA₁ pour montrer que les règles de HA₁ sont correctes: c’est un cercle vicieux.

En général, on peut démontrer la cohérence de n’importe quelle théorie par ce moyen, même de théories incohérentes. Par exemple, considérons un langage de termes dans lequel on peut écrire {x ∣ F(x)} pour toute formule F(x), dont la sémantique est l’ensemble de toutes les valeurs pour x qui rendent F(x) vraie. On adopte une règle de déduction qui exprime que t ∈ {x ∣ F(x)} si et seulement F (t) est vraie. Cette règle est valide, et par le même argument sémantique que ci-dessus, ce système est cohérent. Mais on verra au lemme 17 que cette théorie — la théorie naïve des ensembles — est en réalité incohérente. La raison pour laquelle la démonstration sémantique est incorrecte ici, c’est qu’elle suppose que l’on peut toujours définir l’ensemble de toutes les valeurs vérifiant une formule donnée (voir la définition de la sémantique de {x ∣ F (x)}). Le fait que la théorie naïve des ensembles soit incohérente montre que, justement, ceci n’a pas de sens.

C’est pour éviter ce cercle vicieux, dans lequel finalement on ramène la cohérence d’une théorie à elle-même, que David Hilbert a proposé au début du vingtième siècle d’établir la cohérence des systèmes logiques utilisés en mathématiques par des moyens finitistes, c’est-à-dire n’utilisant des moyens de raisonnement qui ne portent que sur des objets finis: entiers, arbres finis (donc aussi formules, preuves), mais pas les ensembles quelconques d’entiers ou les arbres infinis, par exemple; et des principes de récurrence structurelle ou sur les entiers, mais pas de quantification sur l’ensemble (infini) de tous les entiers ou de tous les arbres finis par exemple. (Le système logique correspondant s’appelle l’arithmétique primitive récursive PRA et est beaucoup moins expressif, donc aussi beaucoup moins suspect d’incohérence, que PA₁.)

La preuve de cohérence de HA₁ que nous avons donnée est alors presque finitiste: les notions de formules et de preuves sont finitistes, de même que les transformations de preuves définies par les règles de réduction du λ∇ R-calcul et que l’argument du corollaire 5 montrant qu’il n’y a pas de λ∇ R-calcul clos de type ⊥. Le seul argument non finitiste dans la preuve est l’argument de normalisation du théorème 6, où la définition par récurrence structurelle sur F du prédicat u ∈ RED_F repose sur des quantifications universelles sur des domaines infinis: u ∈ RED_{F ⇒ G} si et seulement si, pour tout v ∈ RED_F, uv ∈ RED_G. (Le fait que l’on raisonne sur des ensembles RED_F n’est pas non plus finitiste, mais comme la démonstration n’utilise RED_F que comme un prédicat u ∈ RED_F, ceci n’est pas une entorse grave au finitisme.)

En un sens, on ne peut pas faire mieux, et donc on ne peut pas échapper au cercle vicieux mentionné plus haut: le second théorème d’incomplétude de Gödel peut en effet être invoqué pour prouver qu’on ne peut montrer la cohérence de HA₁ que dans un système logique au moins aussi fort que HA₁ lui-même. (Nous ne décrirons pas formellement ce théorème; informellement, il énonce qu’on ne peut pas montrer la cohérence d’une théorie mathématique T dans T elle-même dès que T est cohérente, récursivement axiomatisable et contient l’arithmétique de Peano du premier ordre — ou de Heyting, ce qui ne change rien.)

Toutefois, la démonstration du corollaire 5 montre que que la seule partie non finitiste, et ce donc d’une façon essentielle, est l’argument de normalisation du λ∇ R-calcul typé. En résumé, on a réduit la question de la cohérence de HA₁ à la question de la seule terminaison d’une classe de programmes informatiques.

Exercice 28 ()   L’arithmétique de Heyting du premier ordre inclut en fait aussi le ∧, le ∨ et le quantificateur ∃. Considérons le système HA₁^∃, obtenu à partir de HA₁ en ajoutant les constructions de l’exercice 23. Montrer que le λ∇ R-calcul enrichi par les constructions ι t u et case u {ι i x ↦ v} avec les règles de typage correspondantes est fortement normalisant. (Adapter la technique de réductibilité. Pourquoi la technique d’effacement ne fonctionne-t-elle pas ? Montrer cependant que la technique d’effacement permet de montrer que HA₁^∃ normalise faiblement: toute stratégie qui normalise d’abord par (β), (β₁), (∇), (R0), (RS), (∃case), puis normalise le terme obtenu par →_N aboutit à une forme normale pour les règles de HA₁^∃. Voir aussi l’exercice 30 et l’exercice 37.) En conclure que HA₁^∃ est cohérent.