Cours 4: Normalisation du système F

Expression, dans Peano, du fait que $Re{d}_{\rho }(A)$ est un candidat de réductibilité:

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

$$P{A}_2,CR(\overrightarrow{X})⊢CR(\xi ⊩A)$$

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

On va appeler

où $\rho :Va{r}_2⟶Candidats$ et “sous $\rho$” veut dire que $M⊩A$ lorqu’on interprète les $fv(A)$ par $\rho$

• $A=X$ est immédiat, car $Re{d}_{\rho }(X)=\rho (X)$
• $A=B⟶C$

CR1

On veut démontrer que $M^{\prime }\in Re{d}_{\rho }(B\to C)=\{P\mid \forall N\in Re{d}_{\rho }(B),PN\in Re{d}_{\rho }(C)\}$

Soit $N\in Re{d}_{\rho }(B)$. Il suffit de montrer que $M^{\prime }N\in Re{d}_{\rho }(C)$.

Or, $MN\in Re{d}_{\rho }(C)$, et par hypothèse d’induction, $Re{d}_{\rho }(C)$ est clos par extension: donc $Re{d}_{\rho }(C)\ni M^{\prime }N⟶MN$

CR2

Soit $M$ normal neutre. Il suffit de prendre $N\in Re{d}_{\rho }(B)$, et montrer que $MN\in Re{d}_{\rho }(C)$.

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

Et donc

Donc par hypothèse d’induction,

et comme, toujours par induction, $Re{d}_{\rho }(C)$ est clos par extension:

$Re{d}_{\rho }(B\to C)\subseteq WN$

Soit $M\in Re{d}_{\rho }(B\to C)$. On veut démontrer que $M$ est normalisable.

Par hyp d’induction, $x\in Re{d}_{\rho }(B)$.

Donc par hypothèse :

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

Preuve: élémentaire.

Donc $M\in WN$.

Rappel:

On remarque que être CR est clos par intersection arbitraire (CR1: clôture par extension, CR2: $NN\subseteq \bullet \subseteq WN$), donc $Re{d}_{\rho }(\forall X.A)$ est un candidat.

Lemme d’adéquation: $\stackrel{\stackrel{\scriptscriptstyle\mathrm{def}}{=}\Gamma }{\overbrace{x_1:C_1,\cdots ,x_n:C_n}}⊢M:A$ dans le système $F$, avec $\overrightarrow{X}=fv(C_1,\cdots ,C_n,A)$ implique

$$P{A}_2,CR(\overrightarrow{X}),N_1⊩C_1,\cdots ,N_n⊩C_n⊢M[\overrightarrow{N}/\overrightarrow{x}]⊩A$$

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

var

lam

Posons $M^{\prime }\stackrel{\scriptscriptstyle\mathrm{def}}{=}M[\overrightarrow{N}/\overrightarrow{x}]$

Alors

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

Donc, par $(⟹I)$:

Et par définition des candidats $\forall$:

app

On procède de même, en utilisant la définition de $M^{\prime }⊩A\to B$, puis $\forall Elim$, puis $⟹Elim$.

Lam

En notant toujours $M^{\prime }$ le terme $M$ avec les substitutions, on a:

Avec $(⟹Intro)$:

Et par $\forall Intro$:

App

Lemme de substitution:

$$Re{d}_{\rho }(A[B/X])=Re{d}_{\rho [X⟼Re{d}_{\rho }(B)]}(A)$$

Preuve: élémentaire

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

Puis, avec $⟹E$ et le lemme disant que $P{A}_2,CR(\overrightarrow{X})⊢CR(\xi ⊩B)$ (i.e. $Re{d}_{\rho }(A)$ est un candidat):

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

Prop: Si $⊢M:Nat\to Nat$, alors $M$ représente une fonction dont la totalité est prouvable dans $P{A}_2$

Totalité:

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

$$P{A}_2⊢\forall x,\exists 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: ${\Delta }_0^0$)

NB: D’après un théorème de Friedman, démontrer une formule ${\Pi }_0^2$ dans $P{A}_2$, c’est la même chose que la démontrer dans $H{A}_2$. Donc cela revient au même de demander $H{A}_2⊢\forall x,\exists t,T_1(e,x,t)$ (le système F est d’ailleurs dans $H{A}_2$, mais pour la cohérence, c’est pareil de prouver les choses dans $P{A}_2$).

Donc

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)