A-traduction et théorème de Kreisel-Friedman

5 A-traduction et théorème de Kreisel-Friedman

Nous avons souvent parlé des versions classiques des systèmes logiques intuitionnistes que nous avons étudié: PA₁ correspondant à HA₁, PA₂ à HA₂, etc. Les systèmes intuitionnistes étaient plus faciles à étudier, notamment ils nécessitaient moins de règles de normalisation des preuves. Cependant, les systèmes classiques correspondants sont cohérents eux aussi, et de plus ils sont d’un usage beaucoup plus courant en mathématiques. On peut donc se demander quels sont les rapports précis entre les variantes intuitionnistes et classiques des systèmes logiques étudiés.

5.1 Non-non traductions et style par passage de continuations

Une partie claire du rapport entre logiques intuitionnistes et classiques est que toute preuve intuitionniste est une preuve classique, mais qu’il existe des preuves classiques non intuitionnistes. Cependant, ceci n’entame en rien le pouvoir expressif des logiques intuitionnistes comparées à leurs variantes classiques. Ce résultat est dû à Kurt Gödel, mais les traductions que nous utiliserons se rapprochent davantage de traductions dues à Kolmogorov ou à Kuroda.

Commençons par la logique propositionnelle avec ⇒ et ⊥ comme connecteurs logiques. Pour toute formule F, on définit sa ¬¬-traduction F^¬¬ comme suit:

F^¬¬	=_def	¬ ¬ F^∘
A^∘	=_def	A	(A type de base, y compris ⊥)
(F ⇒ G)^∘	=_def	F^∘⇒ G^¬¬

Ceci peut se justifier comme suit: en logique classique, F ⇒ G est non F ou G, c’est-à-dire aussi ¬ (F ∧ ¬ G); or F ∧ ¬ G est équivalent à (F ⇒ ¬ G ⇒ ⊥) ⇒ ⊥ = ¬ (F ⇒ ¬ ¬ G). Ceci mène à l’idée que l’on peut définir F^¬¬ en remplaçant récursivement tous les F ⇒ G par quelque chose ressemblant à ¬ ¬ (F ⇒ ¬ ¬ G).

Rappelons que ¬ F est défini comme F ⇒ ⊥. En particulier, ( ¬ F )^¬¬ = ¬ ¬ (F^∘⇒ ¬ ¬ ⊥).

Lemme 18 En logique propositionnelle classique, F et F^¬¬ sont logiquement équivalentes pour toute formule F. De plus, F est prouvable en logique classique si et seulement si F^¬¬ est prouvable en logique intuitionniste.

Autrement dit, modulo l’ajout de suffisamment de doubles négations saupoudrées dans F, on obtient une formule qui signifie la même chose que F en classique et qui est prouvable en intuitionniste dès que F est prouvable en classique. Par exemple, ¬ ¬ A ⇒ A n’est pas prouvable en intuitionniste, mais ( ¬ ¬ A ⇒ A )^¬¬ = ¬ ¬ (((A ⇒ ¬ ¬ ⊥) ⇒ ¬ ¬ ⊥) ⇒ ¬ ¬ A) l’est. (On notera au passage que cette traduction n’est pas particulièrement économe en négations. Il en existe des plus économes.)

Preuve : Il peut servir de s’exercer à construire quelques preuves intuitionnistes de base. D’abord, si u : G, alors u⁻ =_def λ k · ku est de type ¬ ¬ G. Ensuite, si u : ¬ ¬ ¬ G, alors u⁰ =_def λ y · u (λ z · zy) est de type ¬ G. Et si u : ¬ ¬ (G ⇒ H) et v : ¬ ¬ G, alors u * v =_def λ k · u (λ x · v (λ y · k (xy))) est de type ¬ ¬ H (où k : ¬ H, x : G ⇒ H, y : G).

L’équivalence entre F et F^¬¬ en classique signifie qu’il existe un λ C-terme clos u_F de type F ⇒ F^¬¬ et un λ C-terme clos v_F de type F^¬¬ ⇒ F. On définit ces termes par récurrence structurelle sur F: pour tout type de base A, u_A =_def λ x · x⁻, v_A =_def λ x · C x; enfin u_{F ⇒ G} =_def λ x · λ k · k (λ y · u_G (x (v_F y⁻))) (où x : F ⇒ G, k : ¬ (F^∘⇒ G^¬¬), y : F^∘); et v_{F ⇒
G} =_def λ x · λ y · v_G (( x * u_F y )⁰) (où x : ¬ ¬ (F^∘⇒ G^¬¬), y : F; ceci est bien défini car x * u_F y est de type ¬ ¬ G^¬¬ = ¬ ¬ ¬ (¬ G^∘), donc ( x * u_F y )⁰ est bien défini).

Si F^¬¬ est prouvable en intuitionniste, autrement dit s’il existe un λ∇-terme clos u de type F^¬¬, alors on peut considérer u comme un λ C-terme en posant ∇ v =_def C (λ z · v) pour tout v, avec z non libre dans v. Donc v_F u est un λ C-terme clos de type F: F est prouvable en classique.

Réciproquement, montrons que si F est prouvable en classique, alors F^¬¬ est prouvable en intuitionniste. Pour ceci, considérons un λ C-terme u quelconque tel que ⊢ u : F, et construisons un λ∇-terme u′ tel que ⊢ u′ : F^¬¬. Plus généralement, construisons par récurrence structurelle sur le λ C-terme u tel que x₁ : F₁, …, x_n : F_n ⊢ u : F, un λ∇-terme u^* tel que x₁ : F₁^∘, …, x_n : F_n^∘⊢ u^* : F^¬¬. Comme F^¬¬ = ¬ ¬ F^∘, on va construire u^* comme ⟨ u ⟩^∘ k, où x₁ : F₁^∘, …, x_n : F_n^∘, k : ¬ F^∘⊢ ⟨ u ⟩^∘ k : ⊥.

Si u est une variable, alors c’est un x_i, 1≤ i≤ n, et on pose ⟨ u ⟩^∘ k =_def ku.

Si u est de la forme λ x · v de type G ⇒ H, alors par hypothèse de récurrence on a pu dériver x₁ : F₁^∘, …, x_n : F_n^∘, x : G^∘⊢ v^* : H^¬¬, donc ⟨ u ⟩^∘ k =_def k (λ x · v^*) = k (λ x · λ k′ · ⟨ v ⟩^∘ k) convient.

Si u est de la forme vw avec v de type G ⇒ H et w de type G, alors par hypothèse de récurrence dans le contexte x₁ : F₁^∘, …, x_n : F_n^∘, v^* est de type ¬ ¬ (G^∘⇒ H^¬¬) et w^* est de type G^¬¬ = ¬ ¬ G^∘, donc u^* peut être défini comme ( v^* * w^* )⁰. Plus explicitement, comme λ y · (λ k · v^* (λ x · w^* (λ y · k (xy)))) (λ z · zy), qui se réduit en λ k · v^* (λ x · w^* (λ y · xyk)) (à α-conversion près). On pose donc ⟨ u ⟩^∘ k =_def ⟨ v ⟩^∘ (λ x · ⟨ w ⟩^∘ (λ y · xyk)).

Si u est de la forme C v avec v de type ¬ ¬ F, alors par hypothèse de récurrence dans le contexte x₁ : F₁^∘, …, x_n : F_n^∘, v^* est de type ¬ ¬ ((F^∘⇒ ¬ ¬ ⊥) ⇒ ¬ ¬ ⊥). Donc si k : ¬ F^∘, v^* (λ x · x (λ y, k′ · ky) (λ z · z)) est de type ⊥ (où x : (F^∘⇒ ¬ ¬ ⊥) ⇒ ¬ ¬ ⊥, y : F^∘, k′ : ¬ ⊥, z : ⊥). On pose donc ⟨ u ⟩^∘ k =_def ⟨ v ⟩^∘ (λ x · x (λ y, k′ · ky) (λ z · z)).

♦

Le terme ⟨ u ⟩^∘ k est défini par:

⟨ x ⟩^∘ k	=_def	kx
⟨ λ x · u ⟩^∘ k	=_def	k (λ x · λ k′ · ⟨ u ⟩^∘ k′)
⟨ uv ⟩^∘ k	=_def	⟨ u ⟩^∘ (λ x · ⟨ v ⟩^∘ (λ y · xyk))
⟨ C u ⟩^∘ k	=_def	⟨ u ⟩^∘ (λ x · x (λ y, k′ · ky) (λ z · z))

Les trois premières lignes sont connues comme la traduction par valeur de Plotkin [Plo76].

Dans cette définition, k est toujours d’un type de la forme ¬ F^∘, et joue le rôle d’une continuation acceptant des valeurs de retour de type F^∘. La traduction u ↦ u^* = λ k · ⟨ u ⟩^∘ k est ce qu’on appelle une traduction en style de passage de continuations (continuation-passing style ou CPS en anglais). Elle exprime en fait directement une sémantique par continuations (comparer avec la section 5.2 en partie I): pour évaluer une variable x dans une continuation k, on retourne (la valeur de) la variable par k; pour évaluer une abstraction λ x · u, on retourne par la continuation k la fonction qui prend (la valeur de) l’argument x et la continuation k′ qui sera courante au moment de l’application de l’abstraction à son argument, et qui retourne la valeur du corps u de l’abstraction dans la continuation k′; pour évaluer une application uv dans la continuation k, on évalue u dans une continuation qui récupère la valeur x de u, évalue ensuite v dans une continuation qui récupère la valeur y de v, enfin applique x à y et la continuation courante k; pour évaluer C u dans la continuation k, on évalue u dans la continuation qui récupère la valeur x de u: x est censée être une fonction prenant une continuation en argument, ici λ y, k′ · ky qui jette la continuation courante k′ pour renvoyer y par l’ancienne continuation courante k capturée par C; l’argument λ z · z est la continuation fournie à x, qui est triviale car l’application de x est obligé d’appliquer une autre continuation et ne retourne pas.

La traduction u, k ↦ ⟨ u ⟩^∘ k a donc non seulement un sens logique (le plongement de la logique classique en logique intuitionniste), mais aussi un sens calculatoire. Les exercices suivants précisent cette remarque. (On pourra s’inspirer des résultats de la partie I.)

Exercice 48 Montrer que ⟨ u ⟩^∘ k est bien défini, au sens où deux termes α-équivalents u et v donnent deux termes α-équivalents ⟨ u ⟩^∘ k et ⟨ v ⟩^∘ k. (Montrer que ⟨ u [x:=y] ⟩^∘ k = ⟨ u ⟩^∘ k [x:=y] dès que ni x ni y n’est libre dans k.)

Exercice 49 Rappelons qu’une P-valeur V est une variable ou une abstraction. Montrer que pour toute continuation k, pour tout λ C-terme u, pour toute P-valeur V, ⟨ u [x:=V] ⟩^∘ k ^*← ⟨ V ⟩^∘ (λ x · ⟨ u ⟩^∘ k). (On pourra d’une part s’aider de l’exercice précédent, d’autre part lorsque V = λ y · v, montrer que ⟨ u ⟩^∘ k [x:=λ y, k′ · ⟨ v ⟩^∘ k′] = ⟨ u [x:=λ y · v] ⟩^∘ k.)

Exercice 50 Rappelons que la règle (β_v) est: (λ x · u) V → u [x:=V], où V est une P-valeur. Montrer que la traduction u, k ↦ ⟨ u ⟩^∘ k interprète correctement (β_v), au sens où, si u → v par la règle (β_v), alors ⟨ u ⟩^∘ k →⁺ ⟨ v ⟩^∘ k pour toute continuation k. On montrera d’abord en s’aidant des exercices précédents que ⟨ (λ x · u) V ⟩^∘ k →⁺ ⟨ u [x:=V] ⟩^∘ k pour tout λ C-terme u et toute P-valeur V.

Exercice 51 (

) On rappelle les règles suivantes:

( C_L)	C u v	→	C (λ k′ · u (λ f · k′ (f v)))
( C_R)	V ( C u)	→	C (λ k′ · u (λ x · k′ (V x)))
(η C)	C (λ k · k u)	→	u (k∉fv(u))

Montrer que si u → v par ( C_L) ou ( C_R) ou (η C), alors ⟨ u ⟩^∘ k =_βη ⟨ v ⟩^∘ k. Peut-on se passer de la règle (η) ?

Exercice 52 Montrer qu’en général le fait que u se réduise en v par (β) ou (η) n’implique pas que ⟨ u ⟩^∘ k =_βη ⟨ v ⟩^∘ k. (On considérera le (β)-rédex (λ x, y · x) (zz′) et l’(η)-rédex λ x · yzx, où x, y, z, z′ sont des variables distinctes.)

Exercice 53 La traduction par nom de Plotkin est définie sur les formules par:

F^* =_def ¬ ¬ F^• A^•=_def A (A type de base) ( F ⇒ G )^•=_def F^* ⇒ G^*

On a donc ( ¬ F )^•= F^* ⇒ ¬ ¬ ⊥, donc ( ¬ ¬ F )^•= ¬ ¬ (F^* ⇒ ¬ ¬ ⊥) ⇒ ¬ ¬ ⊥. Montrer que le lemme 18 est encore valide en remplaçant F^¬¬ par F^*. Vérifier en particulier que la traduction obtenue des λ C-termes en λ∇-termes est:

⟨ x ⟩^• k	=_def	xk
⟨ λ x · u ⟩^• k	=_def	k (λ x · λ k′ · ⟨ u ⟩^• k′)
⟨ uv ⟩^• k	=_def	⟨ u ⟩^• (λ f · f (λ k′ · ⟨ v ⟩^• k′) k)
⟨ C u ⟩^• k	=_def	⟨ u ⟩^• (λ x · x (λ k′ · k′ (λ y, k″ · yk)) (λ z · z))

Exercice 54 (

) Montrer, en s’inspirant de l’exercice 48, que ⟨ u ⟩^• k est bien défini modulo α-conversion; en s’inspirant de l’exercice 49, que ⟨ u ⟩^• k [x:=λ k′ · ⟨ v ⟩^• k′] →^* ⟨ u[x:=v] ⟩^• k pour tous termes u, v; en s’inspirant de l’exercice 51, montrer que si u → v par (β) ou par (η C), alors ⟨ u ⟩^• k →⁺ ⟨ v ⟩^• k (même si v n’est pas une P-valeur), si u → v par ( C_L), alors ⟨ u ⟩^• k =_β⟨ v ⟩^• k, mais que les règles ( C_R) et (η) ne donnent en général pas lieu à des égalités valides à travers la traduction.

On peut étendre ces ¬¬-traductions et les traductions en style par passage de continuations correspondantes à la logique et à l’arithmétique du premier ordre. La traduction par valeur F^¬¬ s’étend ainsi comme suit (mais il y a de nombreuses autres possibilités) aux autres constructions de la logique du premier ordre:

( F ∧ G )^∘	=_def	F^∘∧ G^∘
( F ∨ G )^∘	=_def	F^∘∨ G^∘
( ∀ i · F )^∘	=_def	∀ i · F^¬¬
( ∃ i · F )^∘	=_def	∃ i · F^∘

et la traduction en style par passage de continuations u, k ↦ ⟨ u ⟩^∘ k s’étend alors en:

⟨ ⟨ u, v ⟩ ⟩^∘ k	=_def	⟨ u ⟩^∘ (λ x · ⟨ v ⟩^∘ (λ y · k ⟨ x, y ⟩))
⟨ π₁ u ⟩^∘ k	=_def	⟨ u ⟩^∘ (λ x · k (π₁ x))
⟨ π₂ u ⟩^∘ k	=_def	⟨ u ⟩^∘ (λ x · k (π₂ x))

pour le fragment conjonctif (∧), en:

⟨ ι₁ u ⟩^∘ k

=_def

⟨ u ⟩^∘ (λ x · k (ι₁ x))

⟨ ι₂ u ⟩^∘ k

=_def

⟨ u ⟩^∘ (λ x · k (ι₂ x))

⟨ case u

⎧
⎨
⎩

ι₁ x₁ ↦ v₁

ι₂ x₂ ↦ v₂

⎫
⎬
⎭

⟩

^∘ k

=_def

⟨ u ⟩^∘ (λ x · case x

⎧
⎨
⎩

ι₁ x₁ ↦ ⟨ v₁ ⟩^∘ k

ι₂ x₂ ↦ ⟨ v₂ ⟩^∘ k

⎫
⎬
⎭

)

pour le fragment disjonctif (∨), en:

⟨ λ i · u ⟩^∘ k	=_def	k (λ i · λ k′ · ⟨ u ⟩^∘ k′)
⟨ ut ⟩^∘ k	=_def	⟨ u ⟩^∘ (λ x · xtk)

pour la quantification universelle du premier ordre, en:

⟨ ι t u ⟩^∘ k

=_def

⟨ u ⟩^∘ (λ x · k (ι t x))

⟨ case u

⎧
⎨
⎩

ι i x ↦ v

⎫
⎬
⎭

⟩

^∘ k

=_def

⟨ u ⟩^∘ (λ y · case y

⎧
⎨
⎩

ι i x ↦ ⟨ v ⟩^∘ k

⎫
⎬
⎭

)

pour la quantification existentielle du premier ordre.

Désormais, nous considérerons les versions des logiques classique et intuitionniste, ainsi que des arithmétiques PA₁ et HA₁ qui incluent ∧, ∨, et ∃, obéissant aux règles de déduction (∧ I), (∧ E₁), (∧ E₂), (∨ I₁), (∨ I₂), (∨ E), (∃ I), (∃ E).

Exercice 55 Montrer que, en logique classique du premier ordre, F et F^¬¬ sont logiquement équivalentes. De plus, F est prouvable en logique classique du premier ordre si et seulement si F^¬¬ est prouvable en logique intuitionniste du premier ordre. (Étendre la preuve du lemme 18, et utiliser la traduction en CPS ci-dessus.)

Pour passer à l’arithmétique, il nous faut étendre notre traduction en CPS pour traiter de r₀ : 0 ≈ 0 et le récurseur:

⟨ r₀ ⟩^∘ k	=_def	kr₀
⟨ R u v t ⟩^∘ k	=_def	⟨ v ⟩^∘ (λ x · R (λ k′ · ⟨ u ⟩^∘ k′) (λ j · λ y, k″ · x j (λ x′ · y (λ y′ · x′y′k″))) t k)

Lemme 19 F est prouvable en PA₁ si et seulement si F^¬¬ est prouvable en HA₁.

Preuve : On a déjà la traduction en CPS, il suffit de vérifier qu’elle définit des objets des bons types. Dans le cas de r₀, on doit vérifier que si k : ¬ (0 ≈ 0), alors k r₀ : ⊥; c’est évident. Dans le cas du récurseur, dans la formule pour ⟨ R u v t ⟩^∘ k ci-dessus, on a par hypothèse k : ¬ ( F [i:=t] )^∘, et en supposant que x : ∀ j · ¬ ¬ (( F [i:=j] )^∘⇒ ( F [i:=S (j)] )^¬¬), que y : ( F [i:=j] )^¬¬, que k″ : ¬ ( F [i:=S (j)] )^∘, que x′ : ( F [i:=j] )^∘⇒ ( F [i:=S (j)] )^¬¬, que y′ : ( F [i:=j] )^∘, on a: x′y′k″ est de type ⊥, donc λ y′ · x′y′k″ est de type ¬ ( F [i:=j] )^∘, donc y (λ y′ · x′y′k″) est de type ⊥, donc λ x′ · y (λ y′ · x′y′k″) est de type ¬ (( F [i:=j] )^∘⇒ ( F [i:=S (j)] )^¬¬). Comme x j est de type ¬ ¬ (( F [i:=j] )^∘⇒ ( F [i:=S (j)] )^¬¬), x j (λ x′ · y (λ y′ · x′y′k″)) est de type ⊥, donc λ k″ · x j (λ x′ · y (λ y′ · x′y′k″)) est de type ¬ ¬ ( F [i:=S (j)] )^∘= ( F [i:=S (j)] )^¬¬ = F^¬¬ [i:=S (j)]. (Une récurrence structurelle facile montre en effet que G^¬¬ [i:=t] = ( G [i:=t] )^¬¬.) Comme y est supposé de type ( F [i:=j] )^¬¬ = F^¬¬ [i:=j], le terme v′ =_def λ j · λ y, k″ · x j (λ x′ · y (λ y′ · x′y′k″)) est de type ∀ j · F^¬¬ [i:=j] ⇒ F^¬¬ [i:=S (j)]. D’autre part le terme u′ =_def λ k′ · ⟨ u ⟩^∘ k′ est de type ( F [i:=0] )^¬¬ = F^¬¬ [i:=0]. Donc R u′ v′ t est de type F^¬¬ [i:=t] = ( F [i:=t] )^¬¬. Comme k : ¬ ( F [i:=t] )^∘, R u′ v′ t k est de type ⊥, donc λ x · R u′ v′ t k est de type ¬ (∀ j · ¬ ¬ (( F [i:=j] )^∘⇒ ( F [i:=S (j)] )^¬¬)). On en déduit que ⟨ v ⟩^∘ (λ x · R u′ v′ t k) est de type ⊥; or ⟨ v ⟩^∘ (λ x · R u′ v′ t k) est exactement ⟨ R u v t ⟩^∘ k. ♦

Exercice 56 (

) La démonstration du lemme 19 est incomplète, et le manque le plus flagrant est que nous n’avons pas traité la règle (↔_N^*). La traiter directement est difficile, et nous transformons d’abord la preuve de F en PA₁:

On dit qu’une instance Γ, F ⊢ F de (Ax) est atomique si F est une formule de la forme s≈ t (une formule atomique, à l’exclusion de ⊥). On dit qu’une preuve en PA₁ est η-longue si tous ses axiomes sont atomiques. Montrer que pour tout séquent Γ, F ⊢ F est prouvable par une preuve η-longue. (On effectuera une récurrence sur F.)
En déduire que tout séquent prouvable en PA₁ l’est par une preuve η-longue.
Une preuve en PA₁ est spéciale si les seules instances utilisées de (↔_N^*) le sont sur les conclusions des règles (⊥ E) ou (Ax). Montrer qu’on peut transformer n’importe quelle preuve π en PA₁ d’un séquent en une preuve spéciale π′ du même séquent. De plus, si π est η-longue, alors π′ est η-longue.
Reprendre la preuve du lemme 19, en montrant que si π est une dérivation spéciale η-longue de x₁:F₁, …, x_n:F_n ⊢ u : F en PA₁, alors x₁:F₁^∘, …, x_n:F_n^∘, k:¬ F^∘⊢ ⟨ u ⟩^∘ k : ⊥ est dérivable en HA₁.

Exercice 57 Redémontrer que PA₁ est cohérente (cf. exercice 29) en utilisant le lemme 19.

Exercice 58 Étendre la ¬¬-traduction au second ordre (on démontrera au passage que F^¬¬ [P (k₁, …, k_n) := G^∘] = ( F [P (k₁, …, k_n) := G] )^¬¬), et déduire du théorème 10 que PA₂ est cohérente. Comparer avec la preuve de l’exercice 47.

Exercice 59 (Glivenko) Par une traduction en CPS modifiée, montrer que si x₁:F₁, …, x_n:F_n ⊢ u : F est prouvable en logique propositionnelle classique, alors x₁ : ¬ ¬ F₁, …, x_n : ¬ ¬ F_n ⊢ u^* : ¬ ¬ F pour un certain terme u^* à trouver. (Traiter aussi le cas de ∧, ∨. Montrer que ceci s’étend aux quantifications existentielles mais pas aux quantifications universelles.) En déduire le théorème de Glivenko: pour toute formule ne contenant que des quantifications existentielles, ¬ F est prouvable en logique classique si et seulement si elle est prouvable en logique intuitionniste.

5.2 Formules décidables et classiques

En arithmétique de Heyting, les formules atomiques (les types de base) sont des égalités s ≈ t. Il se trouve que ces égalités sont démontrables en PA₁ si et seulement si elles le sont en HA₁ — on n’a pas besoin de ¬¬-traduction. Une question naturelle est alors: quelles sont les formules de l’arithmétique qui sont prouvables en PA₁ si et seulement si elles le sont en HA₁ ? Georg Kreisel a montré dans les années soixante que les formules Π₂⁰ ont cette propriété, et sa démonstration a été simplifiée par la suite par Harvey Friedman [Fri78]. Les formules Π₂⁰ (prononcer: “pi zéro deux”) sont les formules de la forme ∀ i₁, …, i_m · ∃ j₁, …, j_n · F, où F est sans quantificateur, ou du moins n’a que des instances bénignes des quantificateurs. En général:

Définition 2 On définit l’ordre ≤ sur les entiers en HA₁ en posant que la notation s ≤ t abrège ∃ k · k+s ≈ t. Les quantifications bornées ∀ i ≤ t · F et ∃ i ≤ t · F, lorsque i n’est pas libre dans t, sont des abréviations pour ∀ i · i ≤ t ⇒ F et ∃ i · i ≤ t ∧ F.

On définit les classes de formules Δ₀⁰, Σ_n⁰ et Π_n⁰ par récurrence sur n ≥ 0: Δ₀⁰ = Σ₀⁰ = Π₀⁰ est la classe des formules dont toutes les quantifications sont bornées. Σ_n+1⁰ est la classe des formules de la forme ∃ i₁, …, i_m · F avec m≥ 0, F ∈ Π_n⁰; Π_n+1⁰ est la classe des formules de la forme ∀ i₁, …, i_m · F avec m≥ 0, F ∈ Σ_n⁰.

Ces classes ainsi que leurs inclusions (sous formes de flèches) sont représentées en figure 1.

Figure 1: La hiérarchie arithmétique

Nous allons établir au lemme 22 que toute formule Δ₀⁰ est décidable en HA₁:

Définition 3 Une formule F est décidable en HA₁ si et seulement si F ∨ ¬ F est prouvable en HA₁. Une formule F est classique en HA₁ si et seulement si ¬ ¬ F ⇒ F est prouvable en HA₁.

Notons que:

Lemme 20 Toute formule décidable est classique en HA₁.

Preuve : Soit F une formule décidable, et soit u un λ∇ R-terme clos de type F ∨ ¬ F. Alors cl_F (u) =_def λ x · case u {

ι₁ x₁ ↦ x₁

ι₂ x₂ ↦ ∇ (xx₂)

} est une preuve de ¬¬ F ⇒ F. ♦

Lemme 21 Toute égalité s ≈ t est décidable en HA₁.

Preuve : On démontre ∀ i · i ≈ t ∨ ¬ i ≈ t par récurrence sur t, puis sur i. Définissons:

a	=_def	ι₁ r₀	: 0 ≈ 0 ∨ ¬ 0 ≈ 0
b(j)	=_def	ι₂ (λ x · x)	: S (j) ≈ 0 ∨ ¬ S (j) ≈ 0
c	=_def	λ i · R a (λ j · λ x · b(j)) i	: ∀ i · i ≈ 0 ∨ ¬ i ≈ 0
d(j)	=_def	ι₂ (λ x · x)	: 0 ≈ S (j) ∨ ¬ 0 ≈ S (j)
e(j)	=_def	λ x · λ i · R (d(j)) (λ j′ · λ y · xj′) i	: (∀ i · i ≈ j ∨ ¬ i ≈ j) ⇒ (∀ i · i ≈ S (j) ∨ ¬ i ≈ S (j))
u	=_def	R c (λ j · e (j)) t	: ∀ i · i ≈ t ∨ ¬ i ≈ t

Pour aider à vérifier les types annoncés, vérifier que dans la définition de e(j), xj′ est de type j′ ≈ j ∨ ¬ j′ ≈ j, donc aussi S (j′) ≈ S (j) ∨ ¬ S (j′) ≈ S (j). Le terme us est la preuve souhaitée de s≈ t ∨ ¬ s ≈ t. ♦

Lemme 22 Toute formule F de HA₁ ne contenant que des quantifications bornées est décidable.

Preuve : () Par récurrence structurelle sur Sk (F), on construit un terme d_F de type F ∨ ¬ F.

Si F est une égalité s ≈ t, alors on définit d_{s≈ t} comme étant le terme us de la preuve du lemme 21.

Si F = ⊥, alors d_⊥=_def ι₂ (λ x · x).

Dans les cas des connecteurs ⇒, ∧, ∨, l’idée est de décrire leurs tables de vérité. Par exemple, on G₁ ⇒ G₂ est décidable pour la raison suivante: comme G₁ est décidable par hypothèse de récurrence, G₁ est soit vrai soit faux, de même G₂ est soit vrai soit faux; mais si G₁ est vrai et G₂ faux, alors G₁ ⇒ G₂ est faux, et G₁ ⇒ G₂ est vrai dans les trois autres cas. Formellement:

d_{G₁⇒ G₂}

=_def

case d_G₁

⎧
⎪
⎨
⎪
⎩

ι₁ x₁ ↦ case d_G₂

⎧
⎨
⎩

ι₁ y₁ ↦ ι₁ (λ x · y₁)

ι₂ y₂ ↦ ι₂ (λ x · y₂ (xx₁))

⎫
⎬
⎭

ι₂ x₂ ↦ ι₁ (λ x · ∇ (xx₂))

⎫
⎪
⎬
⎪
⎭

: (G₁ ⇒ G₂) ∨ ¬ (G₁ ⇒ G₂)

d_{G₁∧ G₂}

=_def

case d_G₁

⎧
⎪
⎨
⎪
⎩

ι₁ x₁ ↦ case d_G₂

⎧
⎨
⎩

ι₁ y₁ ↦ ι₁ ⟨ x₁, y₁ ⟩

ι₂ y₂ ↦ ι₂ (λ x · y₂ (π₂ x))

⎫
⎬
⎭

ι₂ x₂ ↦ λ x · x₂ (π₁ x)

⎫
⎪
⎬
⎪
⎭

: (G₁ ∧ G₂) ∨ ¬ (G₁ ∧ G₂)

=_def

λ k, k′, x · case x

⎧
⎨
⎩

ι₁ x₁ ↦ kx₁

ι₂ x₂ ↦ k′x₂

⎫
⎬
⎭

: ¬ G₁ ⇒ ¬ G₂ ⇒ ¬ (G₁ ∨ G₂)

d_{G₁∨ G₂}

=_def

case d_G₁

⎧
⎪
⎨
⎪
⎩

ι₁ x₁ ↦ ι₁ (ι₁ x₁)

ι₂ x₂ ↦ case d_G₂

⎧
⎨
⎩

ι₁ y₁ ↦ ι₁ (ι₂ y₁)

ι₂ y₂ ↦ ι₂ (ax₂y₂)

⎫
⎬
⎭

⎫
⎪
⎬
⎪
⎭

: (G₁ ∨ G₂) ∨ ¬ (G₁ ∨ G₂)

Les cas des quantifications bornées F sont plus difficiles. L’idée est que F ne quantifiant que sur les entiers de 0 à t, on peut prouver F par récurrence, en énumérant tous les entiers de 0 à t. Définissons d’abord quelques termes de preuve auxiliaires démontrant quelques évidences dont nous aurons besoin (on note G (i) une formule quelconque et G (t) la formule G (i) [i:=t] pour plus de clarté). Rappelons (exercice 27) qu’il existe en HA₁ un terme de preuve rep_{k · H(k)} pour toute formule H (k), de type ∀ i, j · i ≈ j ⇒ H (i) ⇒ H (j).

nlS0 (s)

=_def

λ x · case x

⎧
⎨
⎩

ι k, y ↦ y

⎫
⎬
⎭

: ¬ S (s) ≤ 0

rep0S (s)

=_def

λ x · R (λ y · x) (λ j · λ y, z · ∇ (nlS0 (j) z)) s

: G (0) ⇒ s ≤ 0 ⇒ G (s)

repS0 (s)

=_def

R (λ x, y · x) (λ j · λ x, y, z · ∇ (nlS0 (j) z)) s

: G(s) ⇒ s ≤ 0 ⇒ G(0)

=_def

ι 0 r₀

: 0 ≤ 0

n0 (s)

=_def

R r₀ (λ j · λ x · x) s

: 0 + s ≈ s

lrefl(s)

=_def

ι 0 (n0 (s))

: s ≤ s

refl

=_def

λ i · R r₀ (λ j · λ x · x) i

: ∀ i · i ≈ i

nS (s,t)

=_def

R (refl (S (s))) (λ j · λ x · x) t

: S (s) + t ≈ S (s + t)

com (s, t)

=_def

R (n0 (t)) (λ j · λ x · rep_{k · S (j) + t ≈ S (k)} (j + t) (t + j) x (nS (j, t))) s

: s + t ≈ t + s

lch₀ (k,s,t)

=_def

R (λ x · ι₂ (x)) (λ j · λ x, y · ι₁ (ι j (rep_{k · S (k) ≈ t} (s + j) (j + s) (com (s, j)) y))) k

: s + k ≈ t ⇒ S (s) ≤ t ∨ s ≈ t

lch₁ (s,t)

=_def

λ x · case x

⎧
⎨
⎩

ι k y ↦ lch₀ (k,s,t) (rep_{i · i ≈ t} (k + s) (s + k) (com (k, s)) y)

⎫
⎬
⎭

: s ≤ t ⇒ S (s) ≤ t ∨ s ≈ t

lch (s, t)

=_def

lch₁ (s,S (t))

: s ≤ S (t) ⇒ s ≤ t ∨ s ≈ S (t)

sym

=_def

λ i,j · λ x · rep_{k · k ≈ i} i j x (refl i)

: ∀ i, j · i ≈ j ⇒ j ≈ i

reps_k · H(k)

=_def

λ i, j · λ x · rep_k · H(k) j i (sym i j x)

: ∀ i, j · i ≈ j ⇒ H (j) ⇒ H (i)

lS (s, t)

=_def

λ x · case x

⎧
⎨
⎩

ι k y · ι (S (k)) (reps_{i · i≈ S (t)} (S (k) + s) (S (k + s)) (nS (k, s)) y)

⎫
⎬
⎭

: s ≤ t ⇒ s ≤ S (t)

Lorsque F = ∀ i ≤ t · G(i), on démontre que F est décidable par récurrence sur t. Le cas de base est démontré par le terme u₁:

u₁₁

=_def

λ x · λ i · rep0S (i) x

: G(0) ⇒ ∀ i ≤ 0 · G(i)

u₁₂

=_def

λ x, y · x (y 0 l0)

: ¬ G(0) ⇒ ¬∀ i ≤ 0 · G(i)

u₁

=_def

case d_G(0)

⎧
⎨
⎩

ι₁ x₁ ↦ ι₁ (u₁₁ x₁)

ι₂ x₂ ↦ ι₂ (u₁₂ x₂)

⎫
⎬
⎭

: (∀ i ≤ 0 · G(i)) ∨ ¬ (∀ i ≤ 0 · G(i))

Le cas inductif demande à montrer que, sous l’hypothèse h : (∀ i ≤ j · G(i)) ∨ ¬ (∀ i ≤ j · G(i)), on a (∀ i ≤ S (j) · G(i)) ∨ ¬ (∀ i ≤ S (j) · G(i)). On considère deux cas. Dans le cas h₁ : ∀ i ≤ j · G(i), ceci est montré par le terme u₂ (j) ci-dessous:

u₂₁ (h₁,j)

=_def

λ x · λ i · λ y ·

case lch (i,j) y

⎧
⎨
⎩

ι₁ x₁ ↦ h₁ i x₁

ι₂ x₂ ↦ reps_k · G(k) i (S (j)) x₂ x

⎫
⎬
⎭

: G (S (j)) ⇒ ∀ i ≤ S (j) · G(i)

u₂₂ (j)

=_def

λ x, y · x (y (S (j)) (lrefl (S (j))))

: ¬ G (S (j)) ⇒ ¬ ∀ i ≤ S (j) · G(i)

u₂(h₁,j)

=_def

case d_G(S (j))

⎧
⎨
⎩

ι₁ x₁ ↦ ι₁ (u₂₁ (h₁,j) x₁)

ι₂ x₂ ↦ ι₂ (u₂₂ (j) x₂)

⎫
⎬
⎭

: (∀ i ≤ S (j) · G(i)) ∨ ¬ (∀ i ≤ S (j) · G(i))

Dans le cas h₂ : ¬ ∀ i ≤ j · G(i), ceci est montré par le terme u₃ (j) ci-dessous:

u₃₁ (j)	=_def	λ x · λ i · λ y · x i (lS (i,j) y)	: (∀ i ≤ S (j) · G(i)) ⇒ ∀ i ≤ j · G(i)
u₃ (h₂,j)	=_def	ι₂ (λ x · h₂ (u₃₁ (j) x))	: (∀ i ≤ S (j) · G(i)) ∨ ¬ (∀ i ≤ S (j) · G(i))

On pose donc:

d_{∀ i ≤ t · G(i)}

=_def

R u₁ (λ j · λ h · case h

⎧
⎨
⎩

ι₁ h₁ ↦ u₂ (h₁,j)

ι₂ h₂ ↦ u₃ (h₂,j)

⎫
⎬
⎭

) t

: (∀ i ≤ t · G(i)) ∨ ¬ (∀ i ≤ t · G(i))

Lorsque F = ∃ i ≤ t · G, avec i non libre dans t, on construit:

v₁₁

=_def

λ x · ι 0 ⟨ l0, x⟩

: G(0) ⇒ ∃ i ≤ 0 · G(i)

v₁₂

=_def

λ x, y · x (case y

⎧
⎨
⎩

ι i z ↦ rep0S(i) (π₂ z) (π₁ z)

⎫
⎬
⎭

)

: ¬ G(0) ⇒ ¬ ∃ i ≤ 0 · G(i)

v₁

=_def

case d_G(0)

⎧
⎨
⎩

ι₁ x₁ ↦ ι₁ (v₁₁ x₁)

ι₂ x₂ ↦ ι₂ (v₁₂ x₂)

⎫
⎬
⎭

: (∃ i ≤ 0 · G(i)) ∨ ¬ (∃ i ≤ 0 · G(i))

Sous l’hypothèse h₁ : ∃ i ≤ j · G(i), on a:

v₂ (h₁,j)

=_def

ι₁ (case h₁

⎧
⎨
⎩

ι i x ↦ ι i ⟨ lS (i,j) (π₁ x), π₂ x ⟩

⎫
⎬
⎭

)

: (∃ i ≤ S (j) · G(i)) ∨ ¬ ∃ i ≤ S (j) · G(i)

Sous l’hypothèse h₂ : ¬ ∃ i ≤ j · G (i), on a:

v₃₁ (j)

=_def

λ x · ι (S (j)) ⟨ lrefl (S (j)), x ⟩

: G (S (j)) ⇒ ∃ i ≤ S (j) · G(i)

v₃₂ (h₂,j)

=_def

λ x, y · case y

⎧
⎨
⎩

ι i z ↦ case lch (i,j) (π₁ z)

⎧
⎨
⎩

ι₁ z₁ ↦ h₂ (ι i ⟨ z₁, π₂ z ⟩)

ι₂ z₂ ↦ x (rep_k · G(k) i (S (j)) z₂ (π₂ z))

⎫
⎬
⎭

: ¬ G (S (j)) ⇒ ¬ ∃ i ≤ S (j) · G (i)

v₃ (h₂,j)

=_def

case d_G(S (j))

⎧
⎨
⎩

ι₁ x₁ ↦ ι₁ (v₃₁ (j) x₁)

ι₂ x₂ ↦ ι₂ (v₃₂ (h₂,j) x₂)

⎫
⎬
⎭

: (∃ i ≤ S (j) · G(i)) ∨ ¬ ∃ i ≤ S (j) · G(i)

Donc on pose:

d_{∃ i ≤ j · G(i)}

=_def

R v₁ (λ j · λ h · case h

⎧
⎨
⎩

ι₁ h₁ ↦ v₂ (h₁, j)

ι₂ h₂ ↦ v₃ (h₂, j)

⎫
⎬
⎭

) t

: (∃ i ≤ t · G(i)) ∨ ¬ ∃ i ≤ t · G(i)

♦

Lemme 23 En HA₁, pour toute formule F dans Δ₀⁰, les formules F, F^¬¬ et F^∘ sont prouvablement équivalentes. Autrement dit, n’importe quelle implication d’une de ces formules vers n’importe quelle autre est prouvable en HA₁.

Preuve : Notons d’abord que, pour toute formule G dans Δ₀⁰, si d_G est le terme de type G ∨ ¬ G construit au lemme 22, alors c_G =_def cl_G (d_G) (cf. lemme 20) est de type ¬¬ G ⇒ G. On démontre ensuite que F et F^¬¬ sont équivalentes en HA₁, comme au lemme 18 mais en utilisant le terme c_G à la place de C. Nous devons cependant étendre le résultat aux constructions ∧, ∨, ∃. Pour ceci, nous allons construire par récurrence structurelle sur F des termes clos u_F^∘ : F ⇒ F^∘ et v_F : F^¬¬ ⇒ F. Comme d’autre part w_F =_def λ x, k · kx : F^∘⇒ F^¬¬, ceci suffira pour démontrer le lemme.

En convenant du fait que A dénote n’importe quelle égalité ou ⊥, on définit (par exemple, il y a de nombreux autres choix possibles):

u_A^∘

=_def

λ x · x

v_A

=_def

λ x · c_A x

u_F ⇒ G^∘

=_def

λ x, y, k · k (u_G^∘ (x (v_F (λ k′ · k′y))))

v_F ⇒ G

=_def

λ x · c_F ⇒ G (λ k · x (λ y · k (λ z · v_G (y (u_F^∘ z)))))

u_F ∧ G^∘

=_def

λ x · ⟨ u_F^∘ (π₁ x), u_G^∘ (π₂ x) ⟩

v_F ∧ G

=_def

λ x · c_F ∧ G (λ k · x (λ z ·

k ⟨ v_F (λ k′ · k′ (π₁ z)), v_G (λ k′ · k′ (π₂ z)) ⟩))

u_F ∨ G^∘

=_def

λ x · case x

⎧
⎨
⎩

ι₁ x₁ ↦ ι₁ (u_F^∘ x₁)

ι₂ x₂ ↦ ι₂ (u_G^∘ x₂)

⎫
⎬
⎭

v_F ∨ G

=_def

λ x · c_F ∨ G (λ k · x (λ y ·

case y

⎧
⎨
⎩

ι₁ y₁ ↦ k (ι₁ (v_F (λ k′ · k′y₁)))

ι₂ y₂ ↦ k (ι₂ (v_G (λ k′ · k′y₂)))

⎫
⎬
⎭

))

u_{∀ i≤ t · F}^∘

=_def

λ x · λ i · λ k · k (λ y, k′ · k′ (u_F^∘ (xiy)))

v_{∀ i≤ t · F}

=_def

λ x · c_{∀ i≤ t · F} (λ k · x (λ y · k (

λ i · λ z · v_F (λ k′ · yi(λ y′ · y′zk′)))))

u_{∃ i≤ t · F}^∘

=_def

λ x · case x

⎧
⎨
⎩

ι i y ↦ ⟨ π₁ y, u_F^∘ (π₂ y) ⟩

⎫
⎬
⎭

v_{∃ i≤ t · F}

=_def

λ x · c_{∃ i≤ t · F} (λ k · x (λ y ·

case y

⎧
⎨
⎩

ι i z ↦ k (ι i ⟨ π₁ z, v_F (λ k′ · k′ (π₂ z)) ⟩)

⎫
⎬
⎭

))

♦

Lemme 24 En HA₁, pour toute formule Σ₁⁰ F, on peut prouver F^∘⇒ F.

Preuve : Observons que si on peut prouver G^∘⇒ G, alors on peut prouver ( ∃ i · G )^∘⇒ ∃ i · G. En effet, si u : G^∘⇒ G, alors λ x · case x {ι i y ↦ ι i (uy)} est de type ( ∃ i · G )^∘⇒ ∃ i · G. Le lemme se déduit ainsi de cette remarque et du lemme 23 par récurrence sur le nombre de quantificateurs ∃ au début de F. ♦

Mais on ne peut pas prouver en général F^¬¬ ⇒ F, car F^∘ n’est pas décidable en général lorsque F est une formule Σ₁⁰ — ce qui revient à dire que F elle-même n’est pas en général décidable. Nous ne développerons pas l’argument ici, qui fait appel à la théorie des fonctions calculables.

5.3 A-traduction et théorème de Kreisel-Friedman

On peut en fait aller un peu plus loin. L’astuce de Friedman est de modifier la ¬¬-traduction en observant que le type ⊥ dans F^¬¬ = ¬ ¬ F^∘= (F^∘⇒ ⊥) ⇒ ⊥ (deux occurrences de ⊥ dans cette dernière formule) pourrait être remplacé par n’importe quelle formule: rien n’oblige à utiliser ⊥ ici. Du point de vue de la traduction en CPS, le type ⊥ est utilisé comme type des réponses fournies par le programme traduit en CPS (cf. le domaine Ans de la partie I). Or on peut utiliser le type de réponses que l’on souhaite, pas seulement ⊥.

La A-traduction de Friedman est ainsi l’analogue de la ¬¬-traduction, mais avec ⊥ remplacé par une formule quelconque φ (que Friedman notait A, d’où le nom de A-traduction). Noter ¬_φF =_def F ⇒ φ pour rappeler la négation, et redéfinissons la ¬¬-traduction relativisée à φ par:

^φF^¬¬	=_def	¬_φ¬_φ^φF^∘
^φ⊥^∘	=_def	φ
^φA^∘	=_def	A ∨ φ	(A type de base, sauf ⊥)
^φ(F ⇒ G)^∘	=_def	^φF^∘⇒ ^φG^¬¬
^φ( ∀ i · F )^∘	=_def	∀ i · ^φF^¬¬
^φ( ∃ i · F )^∘	=_def	∃ i · ^φF^∘

et la traduction en CPS correspondante est:

⟨ x ⟩^φ k

=_def

⟨ λ x · u ⟩^φ k

=_def

k (λ x · λ k′ · ⟨ u ⟩^φ k′)

⟨ uv ⟩^φ k

=_def

⟨ u ⟩^φ (λ x · ⟨ v ⟩^φ (λ y · xyk))

⟨ C u ⟩^φ k

=_def

⟨ u ⟩^φ (λ x · x (λ y, k′ · ky) (λ z · ∇ z))

⟨ λ i · u ⟩^φ k

=_def

k (λ i · λ k′ · ⟨ u ⟩^φ k′)

⟨ ut ⟩^φ k

=_def

⟨ u ⟩^φ (λ x · xtk)

⟨ ι t u ⟩^φ k

=_def

⟨ u ⟩^φ (λ x · k (ι t x))

⟨ case u

⎧
⎨
⎩

ι i x ↦ v

⎫
⎬
⎭

⟩

^φ k

=_def

⟨ u ⟩^φ (λ y · case y

⎧
⎨
⎩

ι i x ↦ ⟨ v ⟩^φ k

⎫
⎬
⎭

)

⟨ r₀ ⟩^φ k

=_def

kr₀

⟨ R u v t ⟩^φ k

=_def

⟨ v ⟩^φ (λ x · R (λ k′ · ⟨ u ⟩^φ k′) (λ j · λ y, k″ · x j (λ x′ · y (λ y′ · x′y′k″))) t k)

Exercice 60 Noter que la seule différence entre la définition de ⟨ u ⟩^∘ k et celle de ⟨ u ⟩^φ k est un ∇ en plus dans le cas C u de la dernière: pourquoi ? Vérifier que pour tout u : F (via une preuve spéciale η-longue, cf. exercice 56), pour tout k : ¬_φF^∘, ⟨ u ⟩^φ k est de type φ.

Exercice 61 Étendre la traduction u, k ↦ ⟨ u ⟩^φ k aux cas des conjonctions et des disjonctions, de sorte que ⟨ u ⟩^φ k soit toujours de type φ pour tout u : F (via une preuve spéciale η-longue, cf. exercice 56) et pour tout k : ¬_φF^∘.

La version relativisée du lemme 22 est:

Lemme 25 Pour toute formule Δ₀⁰ F, F est φ-décidable: F ∨ ¬_φF est démontrable en HA₁.

Preuve : Par le lemme 22, d_F est un terme clos de type F ∨ ¬ F, donc ^φd_F =_def case d_F {

ι₁ x₁ ↦ ι₁ x₁

ι₂ x₂ ↦ ι₂ (λ y · ∇ (x₂ y))

} est un terme clos de type F ∨ ¬_φF. ♦

De même, on relativise le lemme 20:

Lemme 26 Toute formule F φ-décidable est φ-classique: ¬_φ¬_φF ⇒ F ∨ φ est prouvable en HA₁.

Preuve : Soit u un terme clos de type F ∨ ¬_φF. Alors ^φcl_F (u) =_def λ x · case u {

ι₁ x₁ ↦ ι₁ x₁

ι₂ x₂ ↦ ι₂ (xx₂)

} est de type ¬_φ¬_φF ⇒ F ∨ φ. ♦

On peut alors démontrer la version relativisée du lemme 23 — c’est le lemme 28 plus bas —, mais ceci demande de nombreuses preuves auxiliaires:

Lemme 27 Si F est φ-décidable, alors ¬_φ(∀ i≤ t · F) ⇒ ∃ i ≤ t · ¬_φF est démontrable en HA₁.

Preuve : En reprenant les termes de preuve fabriqués dans la preuve du lemme 22, et en écrivant F(i) à la place de F, posons:

ae₁

=_def

λ x · ι 0 ⟨ l0, λ y · x (λ i · λ z · rep0S (i) y z) ⟩

: ¬_φ(∀ i≤ 0 · F(i)) ⇒ ∃ i≤ 0 · ¬_φF(i)

allS (t)

=_def

λ x, y · λ i · λ z ·

case lch (i,t) z

⎧
⎨
⎩

ι₁ z₁ ↦ x i z₁

ι₂ z₂ ↦ reps_k · F(k) i (S (t)) z₂ y

⎫
⎬
⎭

: (∀ i≤ t · F(i)) ⇒ F (S (t)) ⇒ ∀ i≤ S (t) · F(i)

ll0 (s)

=_def

ι s (refl s)

: 0 ≤ s

ae₂(t)

=_def

λ x, y · case ^φd_{∀ i≤ t · F(i)}

⎧
⎪
⎪
⎨
⎪
⎪
⎩

ι₁ x₁ ↦ case ^φd_F (S (t))

⎧
⎨
⎩

ι₁ y₁ ↦ ι 0 ⟨ ll0 (S (t)), λ z · x (allS (t) x₁ y₁) ⟩

ι₂ y₂ ↦ ι (S (t)) ⟨ lrefl(S (t)), y₂ ⟩

⎫
⎬
⎭

ι₂ x₂ ↦ case xx₂

⎧
⎨
⎩

ι i z ↦ ι i ⟨ lS (i,t)(π₁ z), π₂ z⟩

⎫
⎬
⎭

⎫
⎪
⎪
⎬
⎪
⎪
⎭

: (¬_φ(∀ i≤ t · F(i)) ⇒ ∃ i≤ t · ¬_φF(i)) ⇒ ¬_φ(∀ i≤ S (t) · F(i)) ⇒ ∃ i≤ S (t) · ¬_φF(i)

ae(t)

=_def

R ae₁ (λ j · ae₂ (j)) t

: ¬_φ(∀ i≤ t · F(i)) ⇒ ∃ i≤ t · ¬_φF(i)

♦

Lemme 28 En HA₁, pour toute formule F dans Δ₀⁰, les formules F ∨ φ, ^φF^¬¬ et ^φF^∘ sont prouvablement équivalentes.

Preuve : Pour toute formule G dans Δ₀⁰, notons ^φc_G =_def ^φcl_G (^φd_G) de type ¬_φ¬_φG ⇒ G ∨ φ, où ^φcl_G est défini au lemme 26 et ^φd_G est défini au lemme 25. Construisons par récurrence structurelle sur F des termes clos ^φu_F^∘ : F ∨ φ ⇒ ^φF^∘ et v_F : ^φF^¬¬ ⇒ F ∨ φ. Le lemme se déduira de ces termes, et du terme ^φw_F =_def λ x, k · kx : ^φF^∘⇒ ^φF^¬¬.

Si k : ¬_φF et u : F ∨ φ, on pose [k] u =_def case u {

ι₁ x₁ ↦ kx₁

ι₂ x₂ ↦ x₂

} de type φ.

Ensuite, pour tout opérateur f (π₁, π₂, ι₁, ι₂) tel que fu : G dès que u:F on pose ^φf v =_def case v {

ι₁ x₁ ↦ ι₁ (fx₁)

ι₂ x₂ ↦ ι₂ x₂

}: dès que v:F ∨ φ, ^φf v est de type G ∨ φ. De même, on pose ^φ⟨ u, v ⟩ =_def case u {

ι₁ x₁ ↦ case v

⎧
⎨
⎩

ι₁ y₁ ↦ ι₁ ⟨ x₁, y₁ ⟩

ι₂ y₂ ↦ ι₂ y₂

⎫
⎬
⎭

ι₂ x₂ ↦ ι₂ x₂

} de type (F ∧ G) ∨ φ dès que u : F ∨ φ et v : G ∨ φ.

Si v₁ : F ∨ φ ⇒ H et v₂ : G ∨ φ ⇒ H, et u : (F ∨ G) ∨ φ, on pose ^φcase u {

v₁

v₂

} le terme case u {

ι₁ x₁ ↦ case x₁

⎧
⎨
⎩

ι₁ y₁ ↦ v₁ (ι₁ y₁)

ι₂ y₂ ↦ v₂ (ι₁ y₂)

⎫
⎬
⎭

ι₂ x₂ ↦ ι₂ x₂

} de type H.

Soit A n’importe quelle égalité ou ⊥, on définit:

^φu_A^∘

=_def

λ x · x

^φv_A

=_def

λ x · case ^φc_A x

⎧
⎨
⎩

ι₁ x₁ ↦ x₁

ι₂ x₂ ↦ ι₂ x₂

⎫
⎬
⎭

u_F ⇒ G^∘

=_def

λ x, y, k · k (

^φv_F ⇒ G

=_def

λ x · ^φc_F ⇒ G (λ k · x (λ y ·

^φu_G^∘ (x @ (^φv_F (λ k′ · k′y))))

^φa_F, G k (λ z · ^φv_G (y (^φu_F^∘ z)))))

^φu_F ∧ G^∘

=_def

λ x · ⟨ ^φu_F^∘ (^φπ₁ x), ^φu_G^∘ (^φπ₂ x) ⟩

^φv_F ∧ G

=_def

λ x · ^φc_F ∧ G (λ k · x (λ z ·

[k] ^φ⟨ ^φv_F (λ k′ · k′ (π₁ z)), ^φv_G (λ k′ · k′ (π₂ z)) ⟩))

^φu_F ∨ G^∘

=_def

λ x · ^φcase x

⎧
⎨
⎩

λ x₁ · ι₁ (^φu_F^∘ x₁)

λ x₂ · ι₂ (^φu_G^∘ x₂)

⎫
⎬
⎭

^φv_F ∨ G

=_def

λ x · ^φc_F ∨ G (λ k · x (λ y ·

case y

⎧
⎨
⎩

ι₁ y₁ ↦ [k] (^φι₁ (^φv_F (λ k′ · k′y₁)))

ι₂ y₂ ↦ [k] (^φι₂ (^φv_G (λ k′ · k′y₂)))

⎫
⎬
⎭

))

^φu_{∀ i≤ t · F}^∘

=_def

λ x · λ i · λ k · k (λ y, k′ · k′ ( ^φu_F^∘ (x @ i @ y)))

^φv_{∀ i≤ t · F}

=_def

λ x · case ^φd_{∀ i≤ t · F}

⎧
⎪
⎪
⎨
⎪
⎪
⎩

ι₁ x₁ ↦ ι₁ x₁

ι₂ x₂ ↦ case ae (t)

⎧
⎪
⎨
⎪
⎩

ι i y ↦ x (λ x′ · x′i (λ z · z (ι₁ (π₁ y)) (λ z′ ·

case ^φv_F (λ k · kz′)

⎧
⎨
⎩

ι₁ y₁ ↦ π₂ y y₁

ι₂ y₂ ↦ y₂

⎫
⎬
⎭

)))

⎫
⎪
⎬
⎪
⎭

⎫
⎪
⎪
⎬
⎪
⎪
⎭

^φu_{∃ i≤ t · F}^∘

=_def

λ x · case x

⎧
⎪
⎨
⎪
⎩

ι₁ x₁ ↦ case x₁

⎧
⎨
⎩

ι i y ↦ ι i ⟨ π₁ y, ^φu_F^∘ (ι₁ (π₂ y)) ⟩

⎫
⎬
⎭

ι₂ x₂ ↦ ι 0 ⟨ ll0 (t), ^φu_F[i:=0]^∘ (ι₂ x₂)⟩

⎫
⎪
⎬
⎪
⎭

^φv_{∃ i≤ t · F}

=_def

λ x · ^φc_{∃ i≤ t · F} (λ k · x (λ x′ · case x′

⎧
⎨
⎩

ι i y ↦ case ^φv_F (λ k′ · k′ (π₂ y))

⎧
⎨
⎩

ι₁ y₁ ↦ k (ι i ⟨ π₁ y, y₁⟩)

ι₂ y₂ ↦ y₂

⎫
⎬
⎭

))

♦

Si F est une formule Σ₁⁰ prouvable en PA₁, par l’exercice 60 ^φF^¬¬ = ¬_φ¬_φ^φF^∘ est prouvable en HA₁, par une preuve λ k · ⟨ u ⟩^φ k. Ceci est vrai pour tout φ, en particulier pour φ = F. Donc (^φF^∘⇒ F) ⇒ F est prouvable en PA₁ pour φ = F. Mais par le lemme 28, il existe un terme de preuve en HA₁ de ^φF^∘⇒ F, à savoir la continuation k_F =_def λ x · case ^φv_F (λ k · kx) {

ι₁ x₁ ↦ x₁

ι₂ x₂ ↦ x₂

}. Donc ⟨ u ⟩^φ k_F est une preuve de F en PA₁. On en déduit:

Théorème 12 (Kreisel-Friedman) Pour toute formule Π₂⁰ de l’arithmétique F, si F est prouvable en PA₁, alors F est prouvable en HA₁.

Preuve : Écrivons F =_def ∀ i₁, …, i_m · G où G est une formule Σ₁⁰. En utilisant (∀ E), si F est prouvable en PA₁, alors G aussi. Comme G est Σ₁⁰, G est prouvable en HA₁ par la remarque ci-dessus. En utilisant (∀ I), on en déduit que F est elle aussi prouvable en HA₁. ♦

Il se trouve que ce résultat ne peut pas être étendu au-delà de Π₂⁰, et il existe des formules Σ₂⁰ prouvables en PA₁ mais pas en HA₁. Ceci sort cependant du cadre de ce cours.

La signification calculatoire de ce résultat, qui est contenue dans le cas où F est Σ₁⁰, est qu’on peut toujours extraire d’une preuve classique u de F une preuve intuitionniste ⟨ u ⟩^φ k_F de F, en calculant la traduction en CPS de u et en l’appliquant à une continuation k_F bien choisie.

Une application informatique est la suivante. Considérons pour simplifier une formule de la forme ∀ i · ∃ j · P (i, j) sans variable libre. Une preuve intuitionniste d’une telle formule, écrite en forme normale, décrit nécessairement pour tout i une valeur de j tel que P (i, j) soit vrai. Autrement dit, une formule de cette forme est une spécification d’une fonction qui envoie tout entier i vers un entier j tel que P (i, j). Prouver ∀ i · ∃ j · P (i, j) en HA₁, c’est donc essentiellement trouver une fonction de i vers j satisfaisant la spécification. En effet, considérons un terme de preuve normal u tel que ⊢ u : ∀ i · ∃ j · P (i, j). Pour tout entier m, posons [m] le terme S (S (… (S (0)) … )), où il y a m symboles S. Alors on a ⊢ u [m] : ∃ j · P ([m], j). Soit v une forme normale de u [m] (par une stratégie de réduction donnée, disons; en fait, la réduction de preuves en HA₁ est confluente, et il n’y a donc qu’une forme normale). Alors v est tel que ⊢ v : ∃ j · P ([m], j). Comme v est normal et clos, v ne peut qu’être de la forme ι t w, pour un certain terme clos normal t et un certain terme de preuve w. Or un terme clos normal t est nécessairement de la forme [n] pour un certain entier n; et w est une preuve de P ([m], [n]): la preuve u définit donc bien une fonction totale des m vers les n tels que P ([m], [n]) soit vraie. De plus, cette fonction est calculable: il existe un programme informatique qui calcule n en fonction de m; en effet, il suffit de construire u [m], de normaliser et d’extraire [n] de la forme normale. On dit que HA₁ est une logique constructive, car d’une preuve d’une spécification de la forme ∀ i · ∃ j · P (i, j) on peut toujours extraire un programme qui calcule j en fonction de i. (Attention, le terme “constructif” a de nombreux autres sens.)

Exercice 62 Montrer cette affirmation formellement. L’étendre au cas des formules ∀ i₁, …, i_p · ∃ j₁, …, j_q · P (i₁, …, i_p, j₁, …, j_q).

En revanche, si ∀ i · ∃ j · P (i, j) est prouvable en PA₁, l’argument ci-dessus ne fonctionne pas: le terme v de type ∃ j · P ([m], j) peut être de la forme ι t w comme ci-dessus, ou bien de la forme C v′; dans ce dernier cas, on ne peut pas extraire de v une valeur de v telle que P ([m], j) soit prouvable. La fonction qui aux i associe des j tels que P (i, j) est donc en général partielle dans le cas de PA₁, alors que HA₁ permet de produire une fonction totale. Ce que le théorème 12 montrer ici est que lorsque ∀ i · ∃ j · P (i, j) est Π₂⁰, autrement dit quand P (i, j) est décidable, alors il y a toujours moyen de transformer cette fonction partielle en une fonction totale calculable qui satisfait la propriété P (i, j): PA₁ est donc aussi une logique constructive, si on la restreint aux formules Π₂⁰.

On notera que le programme extrait de la preuve est automatiquement correct, au sens où il calcule nécessairement ce que la spécification P (i, j) prescrit. De plus, on n’a pas eu à l’écrire, il suffit de l’extraire de la preuve. Cette idée s’étend naturellement — dans un cadre intuitionniste — à l’utilitaire d’extraction de programme à partir d’une preuve dans Coq [BBC⁺99].

Exercice 63 Étendre le théorème 12 au cas des formules de la forme de la forme F =_def ∀ X₁, …, X_m, x₁, …, x_p · ∃ Y₁, …, Y_n, y₁, …, y_q · G, où G est sans quantificateur, X₁, …, X_m, Y₁, …, Y_n sont des variables du second ordre et x₁, …, x_p, y₁, …, y_q sont des variables du premier ordre: autrement dit, montrer que si F est prouvable en PA₂, alors F est prouvable en HA₂. (On considérera les versions de PA₂ et HA₂ avec les connecteurs ⇒, ⊥, ∧, ∨, les quantifications universelles ∀ et existentielles ∃ tant du premier que du second ordre. Les règles de déduction sur le ∃ du second ordre sont celles de l’exercice 36. On posera ( ∀ P · F )^∘=_def ∀ P · F^¬¬, ( ∃ P · F )^∘=_def ∃ P · F^∘ et on montrera que F^∘[P (k₁, …, k_n) := G^∘] = ( F [P (k₁, …, k_n) := G] )^∘.)

PA₁ et HA₁ sont expressives; notamment on peut définir toute fonction calculable en PA₁ [Joh87], mais c’est difficile et peu naturel à montrer. On peut améliorer ceci en enrichissant le langage de calcul à l’intérieur des formules. L’exercice suivant donne un exemple. De nombreuses autres solutions sont envisageables, et l’on peut (presque) utiliser le langage de programmation que l’on souhaite à l’intérieur des formules.

Exercice 64 Le langage des termes de PA₁^ω et de HA₁^ω est similaire à celui de HA_ω: il est formé des λ-termes simplement typés construits à partir des trois constantes 0 : N, S : N → N et R_τ: τ → (N → τ → τ) → N → τ (le récurseur de type τ), les types étant donnés par τ ::= N ∣ τ → τ. PA₁^ω et HA₁^ω (d’ordre 1 mais portant sur des termes d’ordre supérieur) sont définies comme PA₁ et HA₁ respectivement, mais avec le langage de termes ci-dessus, et la réduction suivante sur les formules au lieu de →_N:

(0≈S)	0 ≈ S t	→₊	⊥
(S≈S)	S s ≈ S t	→₊	s ≈ t
(R0)	R_τs₁ s₂ 0	→₊	s₁
(RS)	R_τs₁ s₂ (S s₃)	→₊	s₂ s₃ (R_τs₁ s₂ s₃)
(β)	(λ i · s) t	→₊	s [i:=t]

Montrer qu’on peut définir l’addition et la multiplication respectivement par s + t =_def R_Ns (λ i, j · S j) t et s * t =_def R_N0 (λ i, j · j+ s) t. Comment définiriez-vous t^s, s!, s- t (répondant s−t si s≥ t, 0 sinon), if s then t₁ else t₂ (répondant t₁ si s≠ 0 et t₂ sinon), s div t (la partie entière de s/t, que vous prendrez égale à 0 quand t ↔₊^* 0), s modt?

Exercice 65 Montrer le théorème de normalisation forte de PA₁^ω et HA₁^ω. En déduire que ces logiques sont cohérentes.

Exercice 66 Montrer le théorème de Kreisel-Friedman pour PA₁^ω et HA₁^ω.

Exercice 67 (

) En utilisant les définitions trouvées à l’exercice 64, montrer que s≈ t et s - t ≈ 0 ∧ t - s ≈ 0 sont prouvablement équivalentes en HA₁^ω. (Faites-le informellement, et produisez les termes de preuve si vous en avez le courage.) Montrer d’autre part que les paires de formules suivantes sont aussi prouvablement équivalentes en PA₁^ω:

s ≈ 0 ∧ t ≈ 0 et s+ t ≈ 0;
s ≈ 0 ∨ t ≈ 0 et s* t ≈ 0;
¬ s≈ 0 et if s then 0 else S0 ≈ 0;
s ≈ 0 ⇒ t ≈ 0 et ¬ s ≈ 0 ∨ t ≈ 0;
∀ i ≤ t · s(i) ≈ 0 et R_N(s(0)) (λ i, j · s(S i) + j) t ≈ 0;
∃ i ≤ t · s(i) ≈ 0 et R_N(s(0)) (λ i, j · s(S i) * j) t ≈ 0;

En déduire que toute formule Δ₀⁰ de PA₁^ω est prouvablement équivalente en HA₁^ω à une formule de la forme s ≈ 0. En conclure qu’on peut redémontrer le théorème de Kreisel-Friedman sans utiliser de CPS et en remplaçant le lemme 28 par un lemme plus simple à démontrer.

Il existe de nombreux autres outils que l’on peut utiliser pour analyser les systèmes de preuve; consulter [Koh98] pour plus de détails.