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)

Leave a Comment