Cours 2: cohérence de $PA_2$, Girard et Takeuti

Imprédicativité:

$∀X.A$ car circularité: quand on quantifie sur toutes les formules, on quantifie aussi sur la formule qui est en train d’être définie

Ex:

\[Red(∀X. A) ≝ \lbrace M \mid ∀B. MB ∈ Red(A[B/X]) \rbrace\]

Elimination des coupures au second ordre ⟶ ne fonctionne pas comme au premier ordre, puisque que $A[X/B]$ n’est pas “plus petite” que $∀X. A$ (comme c’est le cas au premier ordre).

Difficulté de la normalisation du système F

Girard:

Normalisation du système F ⟹ cohérence de $PA_2$

G. Takeuti:

Elimination des coupures de $LK_2$ ⟹ cohérence de $PA_2$

G.Takeuti a montré que l’élimination des coupures dans $LK_2$ (calcul des séquents au 2nd ordre) ⟹ cohérence de $PA_2$.

Calcul des séquents au 2nd ordre $LK_2$

(avec tout à droite, pour n’avoir qu’une seule règle par connecteur plutôt que 2)

\[\cfrac{⊢ Γ, A}{⊢ Γ, ∀X.A}∀X∉fv(Γ)\] \[\cfrac{⊢ Γ, A[B/X(x_1, ⋯, x_n)]}{⊢ Γ, ∃X.A}∃\]

Schéma de compréhension pour toute formule $A(x_1, ⋯, x_n)$

\[∃Z. ∀x_1, ⋯, x_n. Z(x_1, ⋯, x_n) ⟺ A(x_1, ⋯, x_n)\]

(il existe un ensemble d’individus $Z$ tel que …)

Déduction naturelle ⟶ but: se débarrasser des axiomes, et les “ajouter” dans des règles

  • $PA_2$ = $PA_1$ + schéma de compréhension

Ce que Takeuti a fait: coder ce schéma dans une règle

\[\cfrac{⊢ ∀\vec{x}. A(\vec{x})⟺ A(\vec{x})}{⊢ ⊢ ∃Z. ∀\vec{x}. Z(\vec{x})⟺ A(\vec{x})}∃\]

Puis: Schütte a démontré l’élimination des coupure de $LK_2$ (par des méthodes sémantiques: la coupure est admissible ⟶ existence non constructive d’une preuve sans coupure équivalente)

Puis: Girard démontre que la norm. du système F, impliquant la cohérence de $PA_2$

Elimination des coupures de $LJ_2$ ⟹ cohérence $HA_2$

Gödel:

coh. $HA_2$ ⟺ coh. $PA_2$

Preuve: avec la non-non-traduction

Arithmétique de Peano / Heyting

Arithmétique élémentaire classique (EA) (nom donné par Girard dans “Proof Theory and Logical Complexity”) (notée IEA dans le cas intuitioniste)

Termes:
\[t, u ≝ x \mid f(t_1, ⋯, t_n) \text{ pour toute } f \text{ prim. récursive}\]
Formules:
\[A, B ≝ t=u \mid ⊥ \mid A⟹B \mid A ∧ B \mid A ∨ B \mid ∀x. A \mid ∃x. A\]
\[¬A ≝ A ⟹ ⊥\]
Axiomes:
  • Réflexivité: \(E_r ≝ ∀x. x=x\)
  • Contextualité: \(E_c[t, u] ≝ ∀x, y. x=y ⟹ t[x/z] = u[x/z] ⟹ t[y/z] = u[y/z]\)

  • toutes les déf. primitives récursives (quantifiées universellement)

    • ex: Addition $+$

      • $∀x. x+0 = x$
      • $∀x, y. x+ Sy = S(x+y)$
  • 4e axiome de Peano: \(P_4 ≝ ∀x. Sx ≠ 0\)

Propriété (Symmétrie):

\[∀x, y. x=y ⟹ y=x\]

Preuve:

\[E_c[z, x] ≝ ∀x, y. x=y ⟹ \underbrace{z[x/z]}_{=x} = \underbrace{x[x/z]}_{=x} ⟹ \underbrace{z[y/z]}_{=y} = \underbrace{x[y/z]}_{=x}\]

Propriété (3e “axiome” de Peano: injectivité du successeur):

\[P_3: ∀x, y. Sx=Sy ⟹ x=y\]

est dérivable

Preuve:

Prédécesseur (est prim. réc.):
  • $P0 = 0$
  • $∀x. P(Sx) = x$

$Sx = Sy$ et $Pz = Pz$

Puis contextualité: $P(Sx) = P(Sy)$

Puis définition du préd.: $x=y$

Méta-théorème: Les règles de $LJ_1$ (ou $LK_1$ dans le cas classique) sont dérivables

Proposition (Takeuti, Girard dans PTLC) \(PRA ⊢ Coh(EA)\) et donc \(PA_2 ⊢ Coh(IEA)\)

$PA$/$HA$:

EA/IEA + schéma d’induction

$PA_2$/$HA_2$:
  • EA/IEA
  • induction
  • contextualité au 2nd ordre de l’égalité
  • schéma de compréhension
Egalité de Leibniz:
\[t=_L u ≝ ∀Z. Z(t) ⟹ Z(u)\]
Egalité de la syntaxe ⟹ égalité de Leibniz:
\[E_L ≝ ∀x, y. x=y ⟹ x=_L y\]

NB: donc $E_c$ est inutile, car l’égalité de la syntaxe est plus forte

Formule “$x$ est entier”:
\[Int(x) = ∀X. X(0)⟹ (∀y. X(y) ⟹ X(Sy)) ⟹ X(x)\]

NB: car $x$ appartient à tout ensemble contenant $0$ et clos par successeur (i.e. contenant les entiers), donc $x$ appartient à leur intersection: les entiers

Le calcul (=règles logiques) utilsé pour démontrer (= métathéorie):

$LK_2$ (classique) ou $LJ_2$ (intuitioniste)

Au second ordre, on ajoute l’induction:

\[I ≝ ∀x. Int(x)\]

Et dans la syntaxe, on ajoute $∀X. A$ et $∃X. A$

But final: montrer que

Elimination des coupures $LJ_2$ ⟹ $Coh(HA_2)$

Pour ce faire, on va montrer:

Prop:

\[PA_2 ⊢ Coh(IEA) ⟹ CutElim(LJ_2) ⟹ Coh(HA_2)\]

d’où

Corollaire de $PA_2 ⊢ Coh(IEA)$

\[PA_2 ⊢ CutElim(LJ_2) ⟹ Coh(HA_2)\]

NB 1: comme $PA_2$ ne démontre pas sa propre cohérence, $CutElim(LJ_2)$ n’est pas démontrable dans $PA_2$ (si c’était $ZF$ à la place de $PA_2$, on ne pourrait rien dire)

NB 2: en fait, des théories beaucoup plus faibles que $PA_2$ suffisent, mais on se contentera de $PA_2$

Preuve de Prop:

$X$ est un ensemble extensionnel:
\[Ext(X) ≝ ∀x, y. x=y ⟹ X(x) ⟹ X(y)\]

NB: dès que deux choses sont égales, si $X$ en contient une, il contient aussi l’autre ⟶ extensionnalité

Traduction $(-)^{Int}$

Relativise (restreint) tous les quantificateurs du 1er ordre aux entiers

  • $(t=u)^{Int} ≝ t=u$
  • $(A ⟹ B)^{Int} ≝ A^{Int} ⟹ B^{Int}$
  • $(∀x. A)^{Int} ≝ ∀x. Int(x) ⟹ A^{Int}$
  • $(∀X. A)^{Int} ≝ ∀X. A^{Int}$

Traduction $(-)^{Ext}$

Relativise (restreint) tous les quantificateurs du 2e ordre aux ensembles extensionnels

  • $(t=u)^{Ext} ≝ t=u$
  • $(A ⟹ B)^{Int} ≝ A^{Ext} ⟹ B^{Ext}$
  • $(∀x. A)^{Ext} ≝ ∀x. A^{Ext}$
  • $(∀X. A)^{Ext} ≝ ∀X. Ext(X) ⟹ A^{Ext}$

Rappel: \(HA_2 = IEA + E_L + I + \text{Sch. de compréhension}\)

  • La traduction $Int$ va se débarrasser de $I$
  • La traduction $Ext$ va se débarrasser de $E_L$

Lemme 1: $\vec{x} ≝ fv_1(Γ, A)$

\[\underbrace{HA_2}_{\text{nb fini d'axiomes de } HA_2}, Γ ⊢_{LJ_2} A ⟹ IEA, E_L, Int(\vec{x}), Γ^{Int} ⊢_{LJ_2} A^{Int}\]

Lemme 2: $\vec{X} ≝ fv_2(Γ, A)$

\[HA_2, Γ ⊢_{LJ_2} A ⟹ IEA, Ext(\vec{X}), Γ^{Ext} ⊢_{LJ_2} A^{Ext}\]

Preuve de Prop:

On procède par contraposée: si $HA_2$ est incohérent, on montre que $IEA$ aussi.

Supposons que $HA_2$ est incohérent:

\[HA_2 ⊢_{LJ_2} 0=1\]

Par Int (comme il n’y a pas de var libres):

\[\underbrace{IEA, E_L}_{HA_2} ⊢_{LJ_2} 0=1\]

Et par Ext:

\[IEA ⊢_{LJ_2} 0=1\]

Mais on n’a pas fini: on n’a pas utilisé l’élimination des coupures! En fait, on veut démontrer l’incohérence de $IEA$, i.e:

\[IEA ⊢_{LJ_1} 0=1\]

Comme on a $IEA ⊢_{LJ_2} 0=1$, on aurait pu utiliser les coupures! Donc il y a soit une incohérence dans $LJ_2$ (avec le schéma de compréhension), soit directement dans $LJ_1$.

Mais si $LJ_2$ admet l’élimination des coupures, on peut supposer

\[IEA ⊢_{LJ_2} 0=1\]

prouvé sans coupures.

Donc par la propriété de la sous-formule, on a que du premier ordre dans toute la preuve, donc:

\[IEA ⊢_{LJ_1} 0=1\]

Propriété de la sous-formule: si on peut dériver $Γ ⊢ Δ$ de $Γ’ ⊢ Δ’$, chaque formule qui apparaît dans la preuve est sous-formule des conclusions, i.e. $Γ’, Δ’$ est sous-formule de $Γ, Δ$.

NB: seule la coupure n’a pas la propriété de la sous-formule: dans

\[\cfrac{Γ ⊢ A \qquad Δ, A ⊢ C}{Γ, Δ ⊢ C}\]

$A$ peut venir de n’importe où.

Pour montrer

\[PA_2 ⊢ Norm(F) ⟹ Coh(HA_2)\]

il nous suffit donc de montrer que

\[PA_2 ⊢ Norm(F) ⟹ CutElim(LJ_2)\]

Or

\[CutElim(LJ_2) ⟺ Norm(LJ_2)\]

où la normalisation de $LJ_2$ est l’élimination des patterns “élimination-introduction”

\[Norm(F) \overset{\text{Curry-Howard}}{⟺} Norm(NJ_2^{prop}) ⟺ Norm(NJ_2)\]
Système F avec premier ordre (va avec $NJ_2$ par Curry-Howard):
\[M, N ≝ \underbrace{x^A}_{\text{var du } λ\text{-calcul}} \mid λx^A. M \mid MN \mid ΛX. M \mid MA \mid Λ_1 \underbrace{ξ}_{\text{var. de la logique du 1er ordre}}. M \mid Mt\]
\[(Λ_1 ξ. M)t ⟶ M[t/ξ]\] \[A, B ≝ X(t_1, ⋯, t_n) \mid A → B \mid ∀X. A \mid ∀ξ. A\]

Traduction “oubli” $(-)^-$

\[(\_)^-: \begin{cases} NJ_2 \overset{\text{Curry-H}}{\sim} Syst. F+ \text{1er ordre} ⟶ NJ_2^{prop} \overset{\text{Curry-H}}{\sim} Syst. F \\ \end{cases}\]

Oubli des variables du 1er ordre

  • $X(t_1, ⋯, t_n)^- ≝ X$
  • $(A→B)^- ≝ A^- → B^-$
  • $(∀X. A)^- ≝ ∀X. A^-$

  • $(∀ξ. A)^- ≝ A^-$

  • $(x^A)^- ≝ x^{A^-}$
  • $(λx^A. M)^- ≝ λx^{A^-}. M^-$
  • $(MN)^- ≝ M^- N^-$
  • $(ΛX. M)^- ≝ ΛX. M^-$
  • $(MA)^- ≝ M^- A^-$
  • $(Λ_1 ξ. M)^- ≝ M^-$
  • $(Mt)^- ≝ M^-$

Lemme: $x_1:C_1, ⋯, x_n:C_n ⊢ M:A$ dans sys F + 1er ordre ⟹ $x_1:C_1^-, ⋯, x_n:C_n^- ⊢ M:A^-$ dans sys F

Lemme:

  1. Si $M^-$ est normal, alors $M$ est normalisable
  2. $M^- ⟶ N$ implique $M ⟶^+ P$ tq $P^- = N$

Attention: termes du 1er ordre $t ≝ ξ \mid F(t_1, ⋯, t_n)$ n’interagissent pas du tout avec les $λ$-termes $M$

Ex en Coq: $X:Prop, ξ:Nat, x: Λ, M:Λ$

Rédex:

\[sys F \begin{cases} (λx^A. M)N \\ (ΛX. M)A \end{cases} \\ \text{1er ordre : } (Λ_1 ξ. M)t ⟶ M[t/ξ]\]

  1. Si $N^-$ est normal (i.e. il n’y a pas de syst F-rédex), alors $N$ est normalisable, puisque $(Λ_1 ξ. M)t ⟶ M[t/ξ]$ ne crée pas de nouveaux sys F-rédex.

  2. Car $(M[t/x])^- = M^-$

    \[\begin{xy} \xymatrix{ (Λ_1 ξ. λx^A. M)t N \ar[r]^{\text{2 étapes}} \ar[d]_{(\_)^-} & M[t/ξ][N/x] \ar[d]^{(\_)^-} \\ (λx^A. M) N \ar[r]_{\text{1 étape}} & M[N/x] } \end{xy}\]

Prop:

\[Norm(F) ⟹ Norm(F+\text{1er ordre})\]

Preuve:

Soit $M$ dans F+1er ordre.

En sachant que le sys F normalise, on a $M^- ⟶^\ast N$ avec $N$ normal.

Par lemme partie 2, on a

\[M ⟶^\ast P \text{ avec } P^- = N\]

Donc par le lemme partie 1:

\[P ⟶^\ast P' \text{ avec } P' \text{ normal}\]

Leave a comment