Cours 4: Normalisation du système F

Expression, dans Peano, du fait que $Red_ρ(A)$ est un candidat de réductibilité:

Lemme: Pour tout $A$ et $\vec{X} = fv(A)$

\[PA_2, CR(\vec{X}) ⊢ CR(ξ \Vdash A)\]

Preuve: Par induction sur $A$ (on pourrait faire toute la preuve en déduction naturelle).

On va appeler

\[Red_ρ(A) ≝ \lbrace M \mid M \Vdash A \text{ sous } ρ \rbrace\]

où $ρ: Var_2 ⟶ Candidats$ et “sous $ρ$” veut dire que $M \Vdash A$ lorqu’on interprète les $fv(A)$ par $ρ$

• $A = X$ est immédiat, car $Red_ρ(X) = ρ(X)$
• $A = B ⟶ C$

CR1

\[CR_1: M ∈ Red_ρ(B → C) \text{ et } M' ⟶ M\]

On veut démontrer que \(M' ∈ Red_ρ(B → C) = \lbrace P \mid ∀N ∈ Red_ρ(B), PN∈ Red_ρ(C) \rbrace\)

Soit $N ∈ Red_ρ(B)$. Il suffit de montrer que $M’N ∈ Red_ρ(C)$.

Or, $MN ∈ Red_ρ(C)$, et par hypothèse d’induction, $Red_ρ(C)$ est clos par extension: donc $Red_ρ(C) \ni M’N ⟶ MN$

CR2

\[CR2: \underbrace{NN}_{\text{non-rédex et non-abstractions}} ⊆ Red_ρ(B ⟶ C)\]

Soit $M$ normal neutre. Il suffit de prendre $N ∈ Red_ρ(B)$, et montrer que $MN ∈ Red_ρ(C)$.

Par hypothèse d’induction, $N ∈ WN$, donc il existe $N_0$ normal tel que

\[N ⟶^\ast N_0\]

Et donc

\[MN ⟶^\ast MN_0 ∈ NN\]

Donc par hypothèse d’induction,

\[MN_0 ∈ Red_ρ(C)\]

et comme, toujours par induction, $Red_ρ(C)$ est clos par extension:

\[MN ∈ Red_ρ(C)\]

$Red_ρ(B → C) ⊆ WN$

Soit $M ∈ Red_ρ(B → C)$. On veut démontrer que $M$ est normalisable.

Par hyp d’induction, $x ∈ Red_ρ(B)$.

Donc par hypothèse :

\[Mx ∈ Red_ρ(C) ⊆ WN\]

Lemme: Si $Mx$ est normalisable, alors $M$ est normalisable

Preuve: élémentaire.

Donc $M ∈ WN$.

Rappel:

\[M \Vdash ∀X. A ≝ ∀X. CR(X) ⟹ M \Vdash A\] \[Red_ρ(∀X. A) ≝ \lbrace M \mid ∀ C \text{ candidat}, \; M ∈ Red_{ρ[X ⟼ C](A)} \rbrace \\ = \bigcap_{C \text{ candidat}} Red_{ρ[X ⟼ C]}(A)\]

On remarque que être CR est clos par intersection arbitraire (CR1: clôture par extension, CR2: $NN ⊆ \bullet ⊆ WN$), donc $Red_ρ(∀X. A)$ est un candidat.

---

Lemme d’adéquation: $\overbrace{x_1: C_1, ⋯, x_n: C_n}^{≝ \, Γ} ⊢ M: A$ dans le système $F$, avec $\vec{X} = fv(C_1, ⋯, C_n, A)$ implique

\[PA_2, CR(\vec{X}), N_1 \Vdash C_1, ⋯, N_n \Vdash C_n ⊢ M[\vec{N}/\vec{x}] \Vdash A\]

Preuve: par induction sur la dernière règle dans la dérivation $δ$ de $Γ ⊢ M:A$.

var

\[δ = \cfrac{}{Γ, x:A ⊢ x:A} (var)\\ ⟹ \text{ immédiat}\]

lam

\[δ = \cfrac{Γ, x:\overset{⋮ δ'}{B} ⊢ M:C}{Γ ⊢ λx. M: B → C} (var)\]

Posons $M’ ≝ M[\vec{N}/\vec{x}]$

Alors

\[PA_2, CR(\vec{X}), N \Vdash B ⊢ M'[N/x] \Vdash C\]

Par le lemme CR1 (clôture par extension), on dérive donc:

\[PA_2, CR(\vec{X}), N \Vdash B ⊢ (λx.M')N \Vdash C\]

Donc, par $(⟹ I)$:

\[PA_2, CR(\vec{X}) ⊢ N \Vdash B ⟹ (λx.M')N \Vdash C\]

Et par définition des candidats $∀$:

\[PA_2, CR(\vec{X}) ⊢ \underbrace{(λx.M')}_{= (λx.M)[N/x]} \Vdash B → C\]

app

\[δ = \cfrac{Γ ⊢ \overset{⋮ δ_1}{M: A → B} \qquad Γ ⊢ \overset{⋮ δ_2}{N: A}}{Γ ⊢ MN: B} (app)\]

On procède de même, en utilisant la définition de $M’ \Vdash A → B$, puis $∀ Elim$, puis $⟹ Elim$.

Lam

\[δ = \cfrac{Γ ⊢ M:\overset{⋮ δ'}{A}}{Γ ⊢ λx. M: ∀X. A} (Lam) X ∉ fv(Γ)\]

En notant toujours $M’$ le terme $M$ avec les substitutions, on a:

\[PA_2, CR(\vec{X}), CR(X), \vec{N} \Vdash Γ ⊢ M' \Vdash A\]

Avec $(⟹ Intro)$:

\[PA_2, CR(\vec{X}), \vec{N} \Vdash Γ ⊢ CR(X) ⟹ M' \Vdash A\]

Et par $∀Intro$:

\[PA_2, CR(\vec{X}), \vec{N} \Vdash Γ ⊢ M' \Vdash ∀X.A\]

App

\[δ = \cfrac{Γ ⊢ M:\overset{⋮ δ'}{∀X.A}}{Γ ⊢ M: A[B/X]} (∀E)\] \[PA_2, CR(\vec{X}), CR(\vec{Y}), \vec{N} \Vdash Γ ⊢ \underbrace{M' \Vdash ∀X.A}_{= ∀X. CR(X) ⟹ M' \Vdash A}\]

Lemme de substitution:

\[Red_ρ(A[B/X]) = Red_{ρ[X ⟼ Red_ρ(B)]}(A)\]

Preuve: élémentaire

Il vient qu’on peut dériver, avec $∀E$:

\[PA_2, CR(\vec{X}), CR(\vec{Y}), \vec{N} \Vdash Γ ⊢ CR(ξ \Vdash B) ⟹ (M' \Vdash A)\Big[(ξ \Vdash B)/X\Big]\]

Puis, avec $⟹ E$ et le lemme disant que $PA_2, CR(\vec{X}) ⊢ CR(ξ \Vdash B)$ (i.e. $Red_ρ(A)$ est un candidat):

Enfin, d’après le lemme de substitution:

\[PA_2, CR(\vec{X}), CR(\vec{Y}), \vec{N} \Vdash Γ ⊢ \underbrace{(M' \Vdash A)\Big[(ξ \Vdash B)/X\Big]}_{= M' \Vdash A[B/X]}\]

---

---

Prop: Si $⊢ M: Nat → Nat$, alors $M$ représente une fonction dont la totalité est prouvable dans $PA_2$

Totalité:

i.e. ce sont des fonctions $f$ telles que

\[PA_2 ⊢ ∀x, ∃t, T_1(e, x, t)\]

tel que

• $e$ est le code de $f$
• Prédicat de Kleene $T_1$: $e$ termine sur $x$, et $t$ est une preuve de terminaison de $e$ appliqué à $x$ (prédicat qu’on peut exprimer avec des quantificateurs bornés: $Δ_0^0$)

NB: D’après un théorème de Friedman, démontrer une formule $Π_0^2$ dans $PA_2$, c’est la même chose que la démontrer dans $HA_2$. Donc cela revient au même de demander $HA_2 ⊢ ∀x, ∃t, T_1(e, x, t)$ (le système F est d’ailleurs dans $HA_2$, mais pour la cohérence, c’est pareil de prouver les choses dans $PA_2$).

\[\cfrac{⊢ M: Nat → Nat \qquad ⊢ \underline{n}: Nat}{⊢ M \underline{n}: Nat}\]

Donc

\[\cfrac{PA_2 ⊢ M \underline{n} \Vdash Nat}{PA_2 ⊢ Norm(M \underline{n})}\]

NB: Pour chaque $n$, on a une preuve, mais on n’a pas une preuve générale pour tout $n$ (Gödel nous en empêche, d’ailleurs)