4  Logique intuitionniste d’ordre deux et système F

L’arithmétique de Peano du premier ordre PA₁, ou bien celle de Heyting HA₁, est en fait un système logique relativement faible. Il se trouve que, même si de nombreuses vérités arithmétiques sont démontrables en PA₁ ou en HA₁, il en existe de relativement simples qui ne sont pas démontrables en PA₁ [PH78].

4.1  Logique et arithmétique d’ordre deux

Un système beaucoup plus complet est l’arithmétique de Peano du second ordre PA₂, et sa contrepartie intuitionniste HA₂. Nous allons nous intéresser à HA₂, qui est défini comme HA₁ à partir de la logique du premier ordre, mais à partir de la logique du second ordre. La nouveauté apportée par la logique du second ordre est que nous disposons maintenant de variables de prédicats X, Y, …, que l’on peut appliquer à des termes du premier ordre, et sur lesquelles on peut quantifier.

Formellement, étant donné un langage du premier ordre L donné par des familles de symboles de fonctions F_n, n≥ 0, et des familles de symboles ou variables de prédicats P_n, n≥ 0, on définit les formules du second ordre par la grammaire:

où A parcourt l’ensemble des formules atomiques, et les formules sont vues à α-conversion près. La différence avec les formules du premier ordre est l’ajout de la quantification ∀ P · F d’ordre deux. Par commodité, nous supposerons que chaque ensemble P_n est infini.

L’autre différence avec la logique d’ordre un est la notion de substitution. Pour toute variable du premier ordre i et pour tout terme t du premier ordre, F [i:=t] est défini comme d’habitude. Fixons une fois pour toutes une suite de variables k₁, k₂, …, alors F [P (k₁, …, k_n) := G], où P est une variable de prédicat n-aire et G est une formule est défini par récurrence structurelle sur F par:

où dans la première ligne, côté droit, la substitution est une substitution du premier ordre. Intuitivement, la substitution [P (k₁, …, k_n) := G] consiste à remplacer P (k₁, …, k_n) par G, et donc aussi P (t₁, …, t_n) = P (k₁, …, k_n) [k₁:=t₁, …, k_n:=t_n] par G [k₁:=t₁, …, k_n:=t_n].

Les règles de déduction de la logique d’ordre deux sont celles de la logique d’ordre un plus:

où P ∈ P_n. De même, HA₂ est HA₁ plus ces deux règles, et PA₂ est PA₁ plus ces deux règles.

Notre λ-calcul est le même que le λ∇ R-calcul, plus les constructions u G (application d’un terme à un type) et Λ P · u (abstraction sur une variable de prédicat), et est défini par la grammaire:

où T est le langage des termes du premier ordre de l’arithmétique, et F est celui des formules du second ordre.

Les règles de réduction sont celles de HA₁, plus:

où P est n-aire, et la substitution est étendue aux termes de preuve de façon immédiate.

4.2  Système F₂

Les termes et les réductions de HA₂ sont complexes, et nous allons commencer par étudier une restriction drastique, un système de typage du λ-calcul appelé le système F₂ et dû à Jean-Yves Girard. Nous verrons plus tard que le système F₂ contient l’essentiel des caractéristiques logiques de HA₂.

On obtient le système F₂ d’une part en supprimant dans les formules tous les termes et toutes les quantifications du premier ordre, en ne gardant que des variables de prédicats 0-aires, et en ne gardant dans le λ∇ R-calcul que le λ-calcul plus les applications et abstractions du second ordre sur les variables de prédicats 0-aires — on supprime récurseur, application et abstraction du premier et du second ordre non 0-aire.

Ce qui reste est un langage de types de la forme:

La substitution sur les types est la substitution usuelle (regarder la définition de la substitution d’ordre deux lorsque la variable de prédicat est 0-aire).

Le λ-calcul du système F₂ est défini par:

où F₂ parcourt l’ensemble des formules ci-dessus; et les règles de typage sont:

Comme dans le système des types simples, nous utilisons la convention que les règles sont données pour des termes à α-renommage près. Ceci nous permet d’écrire les règles (Abs) et (TAbs) comme ci-dessus, plutôt que sous la forme plus complexe (mais rigoureuse) ci-dessous:

D’un point de vue logique, ce système de typage est un système de déduction naturelle pour la logique intuitionniste minimale propositionnelle quantifiée.

Les règles de réduction définissant →_βη sont:

Preuve : Bien que la preuve ne soit pas très longue, elle est beaucoup plus subtile que dans les cas précédents. Essayons d’adapter la méthode de réductibilité. Le problème est de définir RED_{∀ P · F}: on est tenté de le définir comme étant l’ensemble des λ-termes u tels que, pour toute formule G, uG soit dans RED_{F [P:=G]}. Mais la formule F [P:=G] n’est non seulement pas en général une sous-expression de ∀ P · F, mais elle peut en fait être beaucoup plus grosse. Le passage par le squelette comme aux théorèmes 4 et 6 ne fonctionne plus. Prenons en effet par exemple RED_{∀ P · P}: si on le définit comme ci-dessus, ce sera l’ensemble des λ-termes u tels que, pour toute formule G, uG est dans RED_G. Autrement dit, pour définir RED_{∀ P · P}, on a besoin de disposer déjà par hypothèse de récurrence des définitions des RED_G pour toutes les formules G — y compris ∀ P · P, au passage. La subtilité fondamentale du système F₂, comme on le voit, est que lorsque l’on quantifie sur P pour définir ∀ P · F, P varie sur toutes les formules, y compris la formule à définir ∀ P · F elle-même. Un système logique qui a cette propriété est dit imprédicatif.

On contourne le problème comme suit. Considérons des contextes C servant à interpréter les variables de types: C est une fonction qui à chaque variable de type P associe un ensemble de λ-termes. Pour toute variable de type P et pour tout ensemble S de λ-termes, notons C [P:=S] le contexte qui à P associe S et à tout Q ≠ P associe C (Q). On définit alors l’ensemble RED_F^C des termes réductibles au type F dans le contexte C. Ceci permettra de contourner le problème en définissant (en gros) RED_{∀ P · F}^C comme l’ensemble des termes u tels que pour tout ensemble S de termes, pour toute formule G, u G est dans REC_F^{C [P:=S]}. L’ensemble RED_F^C sera tel, notamment, que pour toute variable de type P, RED_P^C sera simplement l’ensemble C (P). (Dans les preuves précédentes, c’était SN: on peut rejouer ces preuves en utilisant le contexte qui à tout P associe SN.) Mais pour que la preuve de normalisation forte fonctionne, il faudra que nous vérifions les propriétés (CR1), (CR2) et (CR3). Ces propriétés ne sont pas valides sur RED_P^C si C (P) est un ensemble arbitraire de termes. On restreint donc les C (P) a être des ensembles de λ-termes particuliers appelés candidats de réductibilité. Définissons donc les candidats de réductibilité en paraphrasant les conditions (CR1), (CR2) et (CR3). Un candidat de réductibilité est un ensemble S de λ-termes tels que:

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

Dans cette définition, un terme neutre est un terme ne commençant pas par λ, et SN est l’ensemble des termes fortement normalisants pour →_βη.

Reprenons maintenant la définition de RED_F^C. Pour toute variable de prédicat P, on pose donc RED_P^C =_def C (P); RED_{F1 ⇒ F2}^C est l’ensemble des termes u tels que pour tout v∈ RED_F1^C, uv ∈ RED_F2^C; et RED_{∀ P · F}^C est l’ensemble des termes u tels que, pour tout candidat de réductibilité S, pour toute formule G, uG ∈ RED_F^{C [P:=S]}. Cette définition de RED_F^C est valide, et procède par récurrence structurelle sur F.

Un contexte C est appelé un contexte de candidats si C (P) est un candidat de réductilibité pour tout P. Montrons que RED_F^C vérifie les conditions (CR1) à (CR3), autrement dit que RED_F^C est un candidat de réductibilité pour tout contexte de candidats C et pour toute formule F. Ceci ne présente pas plus de difficulté qu’au théorème 1, et s’effectue par récurrence structurelle sur F. Si F est une variable de type P, RED_P^C = C (P) est un candidat de réductibilité par hypothèse. Si F est de la forme F₁ ⇒ F₂, c’est comme au théorème 1. Le cas intéressant est celui où F est de la forme ∀ P · F₁. Remarquons d’abord que SN est lui-même un candidat de réductibilité; en particulier, il existe des candidats de réductibilité.

• (CR1) Si u ∈ RED_F^C, alors pour tout candidat S, pour toute formule G, u G ∈ RED_F1^{C [P:=S]} par définition. En particulier pour S =_def SN, G =_def ∀ X · X (par exemple). Par hypothèse de récurrence, partie (CR1), u G est dans SN, donc u aussi.
• (CR2) Si u ∈ RED_F^C et u →_βη u′, alors pour tout candidat S, pour toute formule G, u G ∈ RED_F1^{C [P:=S]} par définition. Par hypothèse de récurrence (CR2), comme u G → u′ G, u′ G ∈ RED_F1^{C [P:=S]}. Comme S et G sont arbitraires, u′ ∈ RED_F^C.
• (CR3) Si u est neutre et pour tout u′ tel que u →_βη u′, u′ ∈ RED_F^C, montrons que u ∈ RED_F^C. Pour cela, il suffit, par définition, de montrer que u G ∈ RED_F1^{C [P:=S]} pour tout candidat S et toute formule G. Soit donc S un candidat arbitraire, G une formule arbitraire. Comme u G est neutre, pour montrer que u G ∈ RED_F1^{C [P:=S]}, il suffit de montrer que tous ses réduits en une étape sont dans RED_F1^{C [P:=S]}, par hypothèse de récurrence (CR3). Mais u G ne peut se réduire qu’en u′ G avec u →_βη u′ (auquel cas u′ ∈ RED_F^C par hypothèse, donc u′ G ∈ RED_F1^{C [P:=S]}) ou en u₁ [P:=G], à condition que u soit de la forme λ P · u₁; mais ce dernier cas est impossible, puisqu’alors u ne serait pas neutre.

Observons que: (*) si Q n’est pas libre dans G, alors RED_G^C = RED_G^{C [Q:=S]} pour tout candidat S. Autrement dit, RED_G^C ne dépend que de la restriction de C aux variables de prédicats libres dans G. On montre (*) par récurrence structurelle sur G. Si G est une variable de prédicat P, alors RED_G^C = C (P), alors que RED_G^{C [Q:=S]} = (C [Q:=S]) (P) = C (P) aussi, car par hypothèse Q n’est pas libre dans G, donc Q ≠ P. Si G est de la forme G₁ ⇒ G₂, alors RED_G^C = {u ∣ ∀ v ∈ RED_G1^C · uv ∈ RED_G2^C} = {u ∣ ∀ v ∈ RED_G1^{C [Q:=S]} · uv ∈ RED_G2^{C [Q:=S]}} (par hypothèse de récurrence) = RED_G^{C [Q:=S]}. Si G est de la forme ∀ P · G₁ (où par α-renommage on peut supposer P≠ Q), alors RED_G^C = {u ∣ ∀ S′ candidat · ∀ G′ · u G′ ∈ RED_G1^{C [P:=S′]}} = {u ∣ ∀ S′ candidat · ∀ G′ · u G′ ∈ RED_G1^{C [P:=S′] [Q:=S]}} (par hypothèse de récurrence) = {u ∣ ∀ S′ candidat · ∀ G′ · u G′ ∈ RED_G1^{C [Q:=S] [P:=S′]}} = RED_G^{C [Q:=S]} (car P ≠ Q).

Montrons maintenant que: (**) RED_F^{C [P := RED_GC]} = RED_{F [P:=G]}^C. Ceci est par récurrence structurelle sur F. Si F=P, alors RED_F^{C [P := RED_GC]} = (C [P:= RED_G^C]) (P) = RED_G^C = RED_{F [P:=G]}^C. Si F est une autre variable de prédicat Q, RED_F^{C [P := RED_GC]} = C (Q) = RED_Q^C = RED_{F [P:=G]}^C. Si F est de la forme F₁ ⇒ F₂, alors RED_F^{C [P := RED_GC]} = {u ∣ ∀ v ∈ RED_F1^{C [P := RED_GC]} · uv ∈ RED_F2^{C [P := RED_GC]}} = {u ∣ ∀ v ∈ RED_{F1 [P:=G]}^C · uv ∈ RED_{F2 [P:=G]}^C} (par hypothèse de récurrence) = RED_{F1 [P:=G] ⇒ F2 [P:=G]}^C = RED_{F [P:=G]}^C. Si F est de la forme ∀ Q · F₁, alors RED_F^{C [P := RED_GC]} = {u ∣ ∀ S candidat · ∀ H · u H ∈ RED_F1^{C [P:=RED_GC] [Q:=S]}} = {u ∣ ∀ S candidat · ∀ H · u H ∈ RED_F1^{C [Q:=S] [P:=RED_GC]}} = {u ∣ ∀ S candidat · ∀ H · u H ∈ RED_F1^{C [Q:=S] [P:=RED_GC [Q:=S]]}} (par (*), car par α-renommage on peut supposer Q non libre dans G) = {u ∣ ∀ S candidat · ∀ H · u H ∈ RED_{F1 [P:=G]}^{C [Q:=S]}} (par hypothèse de récurrence) = RED_{F [P:=G]}^C.

On a alors: (+) pour tout terme u₁ tel que u₁ [x:=v] ∈ RED_F2^C pour tout v∈ RED_F1^C, alors λ x· u₁ ∈ RED_{F1 ⇒ F2}^C. C’est comme au lemme 6, voir la preuve du théorème 1.

Aussi: (++) pour tout terme u₁ tel que u₁ [P:=G] ∈ RED_F1^{C [P:=S]} pour toute formule G et tout candidat S, alors λ P · u₁ ∈ RED_{∀ P · F1}^C. Par hypothèse, en prenant G=_def P et S =_def C (P), u₁ lui-même est dans RED_F1^C, donc dans SN par (CR1). Nous démontrons (++) en montrant que (λ P · u₁) G ∈ RED_F1^{C [P:=S]} pour toute formule G et tout candidat S. C’est par récurrence sur ν (u₁), en utilisant (CR3), puisque (λ P · u₁) G est neutre. Mais (λ P · u₁) G ne peut se réduire en une étape que vers: (λ P · u′₁) G avec u₁ →_βη u′₁, qui est dans RED_F1^{C [P:=S]} par hypothèse de récurrence; ou vers u₁ [P:=G], qui est dans RED_F1^{C [P:=S]} par hypothèse; ou vers u₂ G par (Eta), alors que u₁ est de la forme u₂ P et P n’est libre dans aucun type d’aucune variable libre de u₂ — mais alors u₂ G = u₁ [P:=G], qui est dans RED_F1^{C [P:=S]} par hypothèse.

Il ne reste plus qu’à démontrer:

où la substitution [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] qui remplace en parallèle les x_i par les v_i et les variables de types P_j par les formules G_j est définie de la façon naturelle.

On montre (♣) par récurrence structurelle sur la dérivation de typage donnée de u. Si la dernière règle est (Var), u est une variable x_i, 1≤ i≤ n, donc u [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] = v_i est dans RED_Fi^C = RED_F^C par hypothèse.

Si u est de la forme u₁ u₂, par hypothèse de récurrence u₁ [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] est dans RED_{G ⇒ F}^C pour une certaine formule G telle que u₂ [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] est dans RED_G^C, donc u [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] ∈ RED_F^C.

Si u est de la forme u₁ G, avec u₁ de type ∀ P · F₁ et F = F₁ [P:=G], alors par hypothèse de récurrence u₁ [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] ∈ RED_{∀ P · F1}^C, donc u [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] ∈ RED_F1^{C [P:=S]} pour tout candidat S. Prenons S =_def RED_G^C: par (**), u [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] ∈ RED_{F1 [P:=G]}^C = RED_F^C.

Si u est de la forme λ x · u₁, avec F = F₁ ⇒ F₂, alors par hypothèse de récurrence u₁ [x₁:=v₁, …, x_n:=v_n, x:=v, P₁:=G₁, …, P_m:=G_m] ∈ RED_F2^C pour tout v∈ RED_F1^C, mais u₁ [x₁:=v₁, …, x_n:=v_n, x:=v, P₁:=G₁, …, P_m:=G_m] = (u₁ [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m]) [x:=v]. Nous utilisons ici que x peut être prise différente de x₁, …, x_n, et non libre dans v₁, …, v_n, par α-renommage. Donc par (+) u [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] ∈ RED_F^C.

Si u est de la forme λ P · u₁, avec F = ∀ P · F₁, alors par hypothèse de récurrence u₁ [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m, P:=G] est dans RED_F1^C′, et ce pour tout contexte de candidats C′, en particulier pour C′ de la forme C [P:=S]. Comme u₁ [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m, P:=G] = (u₁ [x₁:=v₁, …, x_n:=v_n, x:=v, P₁:=G₁, …, P_m:=G_m]) [P:=G] (en α-renommant P au besoin dans u), et comme S est arbitraire, par (++) u [x₁:=v₁, …, x_n:=v_n, P₁:=G₁, …, P_m:=G_m] est dans RED_{∀ P · F1}^C = RED_F^C.

Le théorème de normalisation forte des termes typés dans le système F₂ se déduit de (♣) en prenant v_i=x_i pour tout i, 1≤ i≤ n, et m=0, en utilisant (CR3) pour justifier le choix des x_i, et (CR1) pour conclure.     ♦

Vu sous l’angle des langages de programmation, les règles (TAbs) et (TApp) offrent la notion de fonctions, et en général d’objets polymorphes. Prenons par exemple la fonction id =_def λ P · λ x · x, de type ∀ P · P ⇒ P: c’est la fonction identité sur tout type P, au sens où id nat est la fonction identité sur les entiers, id real est la fonction identité sur les réels, etc. Il s’agit de polymorphisme paramétrique, le comportement de la fonction étant indépendant du type P passé en paramètre. (L’autre forme classique de polymorphisme est le polymorphisme ad hoc, où le corps de la fonction teste d’abord le type P; c’est la forme typique de polymorphisme présent dans les langages orientés objets.)

Le polymorphisme paramétrique est typiquement le polymorphisme présent dans le langage ML, en particulier en OCaml. Le polymorphisme est cependant restreint en ML: les seules quantifications universelles sont au sommet, pas à l’intérieur, des types. Formellement, appelons monotype tout type du système F₂ dans lequel ∀ n’intervient pas (ce sont les types simples), et appelons polytype tout type de la forme ∀ α₁, …, α_n · F, où F est un monotype. Les types ML sont les polytypes. De plus, les jugements de typage en ML sont asymétriques, et sont de la forme x₁ : F₁, …, F_n ⊢ u : τ, où F₁, …, F_n sont des polytypes et τ est un monotype. À cause de cette forme de jugement, la règle (∀ I) n’a aucun sens comme règle de typage, et la construction λ P · u non plus. La création de polytypes passe par la règle de généralisation (Gen) et la construction de programmes let…in:

où α₁, …, α_n sont les variables de types libres dans τ₁ mais pas libres dans aucun polytype de Γ.

ML diffère aussi du système F₂ par d’autres points. D’abord, le polymorphisme est implicite, comme dans le système F (exercice 40): lorsque x est de type ∀ α · F, on n’écrit pas x G pour obtenir une instance de x de type F [α:=G], mais simplement x. Formellement, la règle de typage des variables est:

Enfin ML est un langage de programmation réel, et inclut donc un certain nombre de constructions moins justifiables logiquement. Par exemple, ML possède les définitions par récursion générales (la construction let rec, codable à l’aide d’une constante Y : ∀ α · (α ⇒ α) ⇒ α — ou plutôt Y : ∀ α, β · ((α ⇒ β) ⇒ (α ⇒ β)) ⇒ (α ⇒ β)), des types de données récursifs (généralisant la définition des entiers de Peano construits sur 0 et S, notamment), des effets de bord, et OCaml a en plus les objets (polymorphisme ad hoc) et encore d’autres constructions.

Exercice 39 ()   Le but de cet exercice est de montrer qu’on peut définir le récurseur sur les entiers de Church dans le système F₂. Ceci procède comme pour le prédécesseur. On pose R_∀=_def λ Q · λ x, y, n · π₁ Q (n (Q × N) (λ z · ⟨ y (π₂ N z) (π₁ Q z), S (π₂ N z) ⟩) ⟨ x, ⌈0⌉⟩). Vérifier que R_∀ est de type ∀ Q · Q ⇒ (N ⇒ Q ⇒ Q) ⇒ N ⇒ Q, et que R_∀G u v ⌈0⌉ →_βη⁺ u, R_∀G u v ⌈n+1⌉ ↔_βη^* v ⌈n⌉ (R_∀G u v ⌈n⌉), où ↔_βη^* est la clôture réflexive symétrique transitive de →_βη. (Montrer par récurrence sur n que, si l’on pose f (Q, u, v, n) =_def n (Q × N) (λ z · ⟨ v (π₂ N z) (π₁ Q z), S (π₂ N z) ⟩) ⟨ u, ⌈0⌉⟩, alors f (Q, u, v, ⌈0⌉) →_βη⁺ ⟨ u, ⌈0⌉⟩, et que si f (Q, u, v, ⌈n⌉) ↔_βη^* ⟨ w, ⌈n⌉ ⟩, alors f (Q, u, v, ⌈n+1⌉) ↔_βη^* ⟨ v ⌈n⌉ w, ⌈n+1⌉ ⟩.)

Exercice 41 ()   Montrer que le λ-calcul typé en système F (exercice 40) est fortement normalisant. (Adapter la preuve du théorème 7.) Pourquoi ceci n’est-il pas un cas particulier du théorème 7 ?

4.3  Normalisation forte de la logique d’ordre deux

Le langage des termes de la logique intuitionniste d’ordre deux est le λ∇-calcul plus les constructions d’application et d’abstraction de prédicats:

où T est l’ensemble des termes du premier ordre et F est celui des formules du second ordre. Les règles de preuve, c’est-à-dire de typage, sont (Ax), (⊥ E), (⇒ I), (⇒ E), (∀ I), (∀ E), (∀₂ I) et (∀₂ E). On normalise les preuves par les règles de réduction:

La propriété de normalisation forte des preuves de logique intuitionniste d’ordre deux est une conséquence directe de celle du système F₂. En effet, définissons comme au théorème 4 une fonction qui efface tout ce qui est du premier ordre dans les formules et les λ∇-termes. Sur les formules:

Noter que P∈ P_n sur le côté gauche est vu comme variable 0-aire sur le côté droit. On traduit aussi ⊥ en ∀ P · P, cf. exercice 31. Sur les λ∇-termes, l’effacement est défini par:

On a:

Preuve : Remarquons d’abord que: (*) E (F′ [P (k₁, …, k_n) := G]) = E (F′) [P := E (G)]. C’est une récurrence structurelle facile sur F′. Ensuite, que: (**) si P n’est pas libre dans F′, alors P n’est pas libre dans E (F′). C’est encore une récurrence structurelle facile sur F′.

On démontre le lemme par récurrence structurelle sur la dérivation donnée de x₁:F₁, …, x_m:F_m ⊢ u : F.

C’est évident si u est une variable x_i, 1≤ i≤ n, si u est de la forme u′ v′, ou λ x · u′.

Si u est de la forme ∇ u′, alors par hypothèse de récurrence on a dérivé x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u′) : ∀ P · P, donc x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u) : E (F) par (TApp).

Si u est de la forme u′ t avec t un terme du premier ordre, alors par hypothèse de récurrence on a dérivé x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u′) : E (G), où G = ∀ i · F, donc x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u) : E (F), puisque E (u) = E (u′) et E (F) = E (G).

Si u est de la forme λ i · u′, alors par hypothèse de récurrence on a dérivé x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u′) : E (G), où F = ∀ i · G, donc x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u) : E (F), puisque E (u) = E (u′) et E (F) = E (G).

Si u est de la forme u′ G, alors par hypothèse de récurrence on a dérivé x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u′) : E (∀ P · F′), où F = F′ [P (k₁, …, k_n) := G]; on en déduit que x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u′) E (G) : E (F′) [P := E (G)]: par (*), E (F) = E (F′) [P := E (G)], donc on a dérivé x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u) : E (F).

Si u est de la forme λ P · u′, alors par hypothèse de récurrence on a dérivé x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u′) : E (F′), avec F = ∀ P · F′, où P n’est pas libre dans F₁, …, F_m; par (**), on peut appliquer (TAbs) et inférer x₁:E (F₁), …, x_m:E (F_m) ⊢ λ P · E (u′) : λ P · E (F′), c’est-à-dire x₁:E (F₁), …, x_m:E (F_m) ⊢ E (u) : E (F).     ♦

Preuve : Montrons d’abord que: (*) E (u′) [x:=E (v′)] = E (u′ [x:=v′]). Aussi, que: (**) E (u′) [P:=E (G)] = E (u′ [P (k₁, …, k_n) := G]) pour tout P ∈ P_n. Enfin, que: (***) E (u′ [i:=t]) = E (u′). Les trois sont par récurrence structurelle sur u′, (**) utilisant la propriété (*) démontrée au lemme 13 dans le cas où u′ est de la forme v′ G′, où G′ est une formule.

On démontre le lemme par récurrence sur la profondeur du rédex que l’on contracte dans u. Le seul cas intéressant est celui où u est lui-même le rédex. Or E ((λ x · u′) v′) = (λ x · E (u′)) E (v′) → E (u′) [x:=E (v′)] = E (u′ [x:=v′]) (par (*)), ce qui règle le cas de (β), E ((λ P · u′) G) = (λ P · E (u′)) E (G) → E (u′) [P:=E (G)] = E (u′ [P (k₁, …, k_n):=G]) (par (**)), ce qui règle le cas de (Beta), et E ((λ i · u′) t) = E (u′) = E (u′ [i:=t]) (par (***)).     ♦

Preuve : Notons que si v → w par la règle (β₁), alors la taille |Sk (v)| du squelette de v est strictement supérieure à celle |Sk (w)| du squelette de w. Définissons le squelette d’un terme par: Sk (x) =_def x, Sk (u′v′) =_def Sk (u′) Sk (v′), Sk (λ x · u′) =_def λ x · Sk (u′), Sk (λ i · u′) =_def λ i · Sk (u′), Sk (u′ t) =_def Sk (u′), Sk (λ P · u′) =_def λ P · Sk (u′), Sk (u′ G) =_def Sk (u′) Sk (G), où le squelette de G est défini comme au théorème 4. La taille de Sk ((λ i · u′) t) = λ i · Sk (u′) est strictement supérieure à celle de Sk (u′ [i:=t]) = Sk (u′) (comme une récurrence structurelle facile sur u′ le montre).

Donc, si on mesure u par le couple (E (u), |Sk (u)|), et que l’on ordonne ces couples par l’ordre lexicographique des deux relations →⁺ et >, si v → w, alors la mesure de v est strictement supérieure à celle de w, en utilisant le lemme 14. L’ordre lexicographique étant bien fondé, le théorème est démontré.

Une preuve peut-être plus intuitive est la suivante. Supposons qu’il existe une réduction infinie partant de u: u = u₀ → u₁ → … → u_i → …. En passant aux effacements, E (u₀) →₌ E (u₁) →₌ … →₌ E (u_i) →₌ … par lemme 14, où →₌ dénote 0 ou une étape de réduction en F₂. Par le théorème 7 il n’y a qu’un nombre fini de ces symboles →₌ qui sont des →, donc il existe un entier i tel qu’à partir de l’indice i on n’ait plus que des réductions par (β₁). Mais il ne peut y avoir qu’un nombre fini consécutif de telles réductions, ce qui contredit le fait que la réduction considérée soit infinie.     ♦

Preuve : Par le théorème 8, on peut se restreindre à considérer u normal. Prenons u de taille minimale parmi les termes normaux tels que ⊢ u : ⊥ soit dérivable; u est de la forme h u₁ … u_n, où h est une variable ou le symbole ∇ (auquel cas n≥ 1), et u₁, …, u_n sont des λ∇-termes, des termes du premier ordre ou des formules. Mais h ne peut pas être une variable, parce que le contexte à gauche de ⊢ est vide. Donc h est ∇, mais alors on a ⊢ u₁ : ⊥, ce qui contredit la minimalité de la taille de u.     ♦

Exercice 43 ()   La logique classique du second ordre est la logique intuitionniste du second ordre plus l’opérateur C, autrement dit plus la règle de typage (¬¬ E). La règles de réduction sont (β), (β₁), (Beta), ( C_L) et (η C). Montrer en étendant le système F₂ au cas classique, c’est-à-dire en ajoutant la règle de typage:

et les règles de réduction ( C_L) et (η C), que la logique classique du second ordre est cohérente.

4.4  Retour sur HA₂ et PA₂

On va montrer que HA₂ est cohérent, par une extension de la technique utilisée pour HA₁. La principale innovation est le traitement de la quantification du second ordre, qui sera traitée comme dans le système F₂.

Preuve : Comme au lemme 12, on prouve que pour toute preuve π₂ de Γ, x : F₁, Δ ⊢ u : F₂ et toute preuve π₁ de Γ ⊢ v : F₁, on peut construire une preuve π de Γ, Δ ⊢ u [x:=v] : F₂ par récurrence structurelle sur π₂.     ♦

Preuve : On prouve plus généralement que pour toute preuve π de x₁:F₁, …, x_m:F_m ⊢ u : F, on peut construire une preuve π de x₁ : F₁ [P (k₁, …, k_n):=G], …, x_m : F_m [P (k₁, …, k_n):=G] ⊢ u [P (k₁, …, k_n):=G] : F [P (k₁, …, k_n):=G] par récurrence structurelle sur π.     ♦

Nous considérons les règles de réduction suivantes, qui sont celles de HA₁ plus (Beta). On ne considère pas (η) et (Eta), dont nous n’aurons pas besoin.

Preuve : Par rapport au théorème 5, le cas de la règle (β) est par le lemme 15, celui de la règle (β₁) est comme au lemme 11, et celui de la règle (Beta) est par le lemme 16. Les autres cas sont comme au théorème 5.     ♦

Preuve : Comme au théorème 6, notons que tout terme t du premier ordre termine. Appelons encore un λ∇ R-terme neutre s’il ne commence pas par λ ou ∇. Soit SN l’ensemble des λ∇ R-termes fortement normalisants. Un candidat de réductibilité est un ensemble S de λ∇ R-termes vérifiant les propriétés (CR1), (CR2) et (CR3) du théorème 7. Un contexte de candidats C est une fonction des variables de prédicats vers des candidats de réductibilité. On définit ensuite RED_⊥^C et RED_{s≈ t}^C comme étant SN, RED_{P (t1, …, tn)}^C est C (P), RED_{F ⇒ G}^C est l’ensemble des λ∇ R-termes u tels que pour tout v ∈ RED_F^C, uv ∈ RED_G^C, RED_{∀ i · F}^C est l’ensemble des λ∇ R-termes u tels que pour tous termes t du premier ordre (qui terminent), ut ∈ RED_{F [i:=t]}^C, et finalement RED_{∀ P · F}^C est l’ensemble des λ∇ R-termes u tels que pour toute formule G, pour tout candidat de réductibilité S, u G ∈ RED_F^{C [P:=S]}. Ceci est une définition de RED_F par récurrence structurelle sur le squelette Sk (F) de F, qui est défini comme au théorème 4, étendu par Sk (∀ P · F) =_def ∀ P · Sk (F).

Il est facile de vérifier que RED_F^C est un candidat de réductibilité pour tout contexte de candidats C et toute formule F, par récurrence structurelle sur Sk (F), que (*) si Q n’est pas libre dans G, alors RED_G^C = RED_G^{C [Q:=S]} pour tout candidat S (par récurrence sur Sk (G)), que (**) RED_F^{C [P := RED_GC]} = RED_{F [P (k1, …, kn):=G]}^C (par récurrence sur Sk (F)), que (+) pour tout terme u₁ tel que u₁ [x:=v] ∈ RED_F2^C pour tout v∈ RED_F1^C, alors λ x· u₁ ∈ RED_{F1 ⇒ F2}^C, et que (++) pour tout terme u₁ tel que u₁ [P (k₁, …, k_n):=G] ∈ RED_F1^{C [P:=S]} pour toute formule G et tout candidat S, alors λ P · u₁ ∈ RED_{∀ P · F1}^C. C’est comme au théorème 7.

Comme au théorème 6, on montre que (∘) 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]}.

Les propriétés (*), (**), (+), (++) et (∘) nous permettent de démontrer:

d’où l’on déduit le théorème.     ♦

Preuve : Exactement comme au corollaire 5.     ♦

L’arithmétique du second ordre et le système F₂ sont tellement proches qu’en fait les fonctions mathématiques de N vers N dont on peut démontrer qu’elles sont totales en arithmétique d’ordre deux sont exactement celles que l’on peut coder comme des λ-termes u de type N ⇒ N en système F₂. C’est le théorème de Girard, dont on pourra trouver une démonstration au chapitre 15 de [GLT89]. Mais certaines fonctions n’ont que des implémentations inefficaces. L’exemple typique est le prédécesseur, dont l’implémentation la plus efficace en système F₂ est celle de l’exercice 38, qui calcule le prédécesseur de n en temps linéaire en n. Une façon de corriger ce problème est d’ajouter à F₂ un type de base N, plus deux constantes 0 : N et S : N ⇒ N, ainsi qu’un récurseur R : ∀ Q · Q ⇒ (N ⇒ Q ⇒ Q) ⇒ N ⇒ Q tel que R u v 0 → u et R u v (S w) → v w (R u v w) — essentiellement comme en HA₂, sauf qu’en HA₂ les entiers naturels sont codés comme des termes du premier ordre et non comme des λ-termes de type N. Le prédécesseur est alors R 0 (λ n, x · n).

4.5  Logiques d’ordre supérieur

Il n’y a aucune raison de s’arrêter à l’ordre deux, et l’on peut définir des systèmes logiques d’ordre 3, 4, …, ω. La logique et l’arithmétique à tous ordres est encore cohérente. Le but de cette section est d’une part d’indiquer comment le λ-calcul est utilisé ici pour définir non seulement les preuves mais les formules elles-mêmes, et d’autre part d’avertir le lecteur qui aurait l’impression que tous les systèmes logiques que l’on peut définir intuitivement sont cohérents, qu’il existe des systèmes logiques apparemment très proches des systèmes précédents mais qui sont incohérents.

Rappelons que nous avons formalisé l’arithmétique du premier ordre par un λ-calcul dont les types étaient des formules du premier ordre modulo quelques règles de calcul pour définir l’addition et la multiplication. La logique d’ordre supérieure est définie de façon similaire en choisissant comme langage des formules un λ-calcul simplement typé enrichi de quelques constantes représentant l’implication et la quantification universelle, modulo les règles de calcul définies par la βη-conversion.

Les types simples que l’on utilise sont:

où l’on note → ce que l’on notait ⇒ auparavant, et B est un ensemble de types dit de base, contenant au moins un type Prop, le type des formules, et un autre type ι, qui servira de type des termes. On pourrait considérer plusieurs types de termes, N, R, string, etc., mais pour simplifier nous ferons comme s’il n’y en avait qu’un.

Les expressions logiques sont les λ-termes typables. Ceux de type Prop sont appelés les formules, ceux de type ι sont appelés les termes. On considère deux constantes additionnelles servant à fabriquer les formules: pour chaque type τ, ∀_τ de type (τ → Prop) → Prop, qui sert à former les quantifications universelles (∀ x : τ · F sera codé comme ∀_τ(λ x · F)), et imp de type Prop → Prop → Prop, qui sert à former les implications (et on notera F ⇒ G au lieu de imp  F  G). Les symboles de prédicats n-aires seront représentés par des variables P de type ι → … → ι → Prop, où il y a n ι: si t₁, …, t_n sont n termes (de type ι, donc), P t₁ … t_n est la formule que nous notions P (t₁, …, t_n) en logique du premier ordre. Les symboles de fonctions n-aires sont représentés par des variables f de type ι → … → ι → ι, où il y a n+1 ι en tout: si t₁, …, t_n sont n termes, f t₁ … t_n sera donc aussi un terme, celui que nous notions f (t₁, …, t_n) en logique du premier ordre.

Les règles de typage des expressions logiques sont essentiellement celles du λ-calcul simplement typé, plus les règles de typage de ∀_τ et imp:

La quantification d’ordre un est ∀_ι. Notamment, ∀ x : ι · F est ce que nous notions ∀ i · F [x:=i] auparavant. La quantification d’ordre deux est ∀_{ι → … → ι → Prop}: en somme, ∀ x : ι → … → ι → Prop · F, où il y a n ι, est ce que nous notions ∀ P · F [x:=P] avec P ∈ P_n en logique du second ordre.

La substitution du premier ordre est la substitution du λ-calcul, et la substitution du second ordre F [P (k₁, …, k_n) := G] est à βη-équivalence près la substitution F [P := λ k₁, …, k_n · G] du λ-calcul.

Dans un contexte de typage simple Γ, soient F₁, …, F_n des formules (des expressions de type Prop dans Γ), alors x₁ : F₁, …, x_n : F_n est un contexte pourvu que les x_i soient des variables différentes deux à deux et en dehors du domaine de Γ. Alors que les contextes de typage seront typiquement notés Γ, les contextes seront typiquement notés Π. Les jugements de preuves seront de la forme Γ; Π ⊢ u : F, et leur dérivabilité signifiera que dans le contexte de typage Γ, Π est un contexte et F est une formule, et que de plus u est une preuve de F à partir des hypothèses F₁, …, F_n présentes dans Π. Noter que les jugements de typage Γ ⊢ e : τ seront aussi utilisés, et sont des jugements du λ-calcul simplement typé avec les constantes ∀_τ et imp. On définit la logique d’ordre supérieure par les règles:

Les règles (∀ E), (∀ I) traitent des quantifications d’ordre un, deux, et encore d’autres. Noter la ressemblance entre les règles sur l’implication et les règles sur la quantification universelle. Il se trouve que ce système est encore cohérent, et ceci peut se démontrer en gros comme pour la logique d’ordre deux, en passant par un système similaire au système F₂ appelé F_ω. Ce dernier a aussi été inventé par Jean-Yves Girard, mais le fait qu’il normalise fortement est plus compliqué que pour F₂.

On peut concevoir des systèmes logiques encore plus expressifs. Utilisant l’égalité de Leibniz ≈ (voir exercice 44), on peut modéliser l’arithmétique HA_ω d’ordre supérieur par l’ajout de constantes 0 de type ι, S de type ι → ι, d’un récurseur R au niveau des preuves:

d’un récurseur au niveau des expressions:

et de termes de preuve vérifiant les règles:

Ce système, ainsi que sa version classique PA_ω, sont encore cohérents, pour des raisons similaires aux précédents, par des résultats de normalisation forte.

Si l’on ajoute à ce genre de systèmes des types dépendants à la LF, des types inductifs généralisant le type N des entiers naturels, plus quelques autres constructions logiques, on aboutit à des systèmes comme le calcul des constructions inductives, qui sert de fondement au système Coq [BBC⁺99], et dont le pouvoir expressif est essentiellement celui de la théorie des ensembles avec une infinité de cardinaux fortement inaccessibles [Wer97, Acz99].

Étendre petit à petit des systèmes logiques semble ainsi une activité anodine, qui produit facilement des logiques cohérentes de plus en plus puissantes. Pourtant, de nombreux mathématiciens célèbres ont été à l’origine de systèmes logiques incohérents, dont on pouvait pourtant croire qu’ils ne poseraient pas de problèmes de cohérence a priori.

L’un de ces premiers systèmes est (une partie de) la théorie naïve des ensembles. Dans ce système qui est une extension de la logique du premier ordre, on a pour tout formule F des termes de la forme {i ∣ F} dénotant l’ensemble des i vérifiant F, et dont l’ensemble des variables libres est celui de F moins i — c’est très proche de la notation λ i · F. On a aussi un symbole de prédicat binaire є dénotant l’appartenance, et deux règles de déduction nouvelles:

Preuve : Il s’agit du contre-exemple de Bertrand Russell. Considérons la formule F (i) =_def ¬ (i є i) qui exprime que i ne s’appartient pas à lui-même, où ¬ G =_def G ⇒ ⊥. Notons A le terme {i ∣ F (i)}. On a:

    ♦

En somme, toute formule est déductible dans cette théorie. Noter la ressemblance entre le terme (λ x · x (є₂ x)) (λ x · є₁ x x) et le terme (λ x · xx) (λ x · xx) qui boucle en λ-calcul pur. La ressemblance n’est pas complètement fortuite. Si on voulait démontrer que la théorie naïve des ensembles était cohérente comme nous l’avons fait jusqu’ici pour d’autres théories, nous essaierions de normaliser les preuves, et ceci se ferait naturellement en utilisant la règle є₁ (є₂ u) → u. Mais alors (λ x · x (є₂ x)) (λ x · є₁ x x) → (λ x · є₁ x x) (є₂ (λ x · є₁ x x)) → є₁ (є₂ (λ x · є₁ x x)) (є₂ (λ x · є₁ x x)) → (λ x · є₁ x x) (є₂ (λ x · є₁ x x)), qui boucle. C’est heureux, car le système est justement incohérent.

En un sens, c’est parce que {i ∈ F} agit comme un λ i · F non typé. On peut éviter le problème en le typant par des types simples, et alors on obtiendra essentiellement la logique d’ordre supérieur.

On peut se demander si on ne pourrait pas enrichir le système de types des expressions logiques de la logique d’ordre supérieur, en remplaçant les types simples par les types du système F₂, par exemple. On obtiendra ainsi le système U⁻. Définissons-le formellement. On note α, β, …, les variables de types, Π ce que nous notions ∀ en système F₂, autrement dit les types sont:

où B est un ensemble de types de base et TVar dénote l’ensemble des variables de types. Mais, bien que cette extension du langage des formules ait l’air innocente, on a:

L’argument est élaboré et ne sera pas donné ici: voir [Coq94], qui donne aussi quelques intuitions et quelques applications.