TD7 : 𝜆C, Non-non traduction, logique intuitionniste

Énoncé

EX 1.

\cfrac{𝛤 \vdash u: ¬¬F}{𝛤 \vdash 𝒞u : F}(¬¬E)
\cfrac{𝛤 \vdash u: A}{𝛤 \vdash 𝜄_1 u : A∨B}
\cfrac{𝛤 \vdash u: B}{𝛤 \vdash 𝜄_2 u : A∨B}
\cfrac{𝛤 \vdash u: A∨B \quad 𝛤 \vdash f: A⟹C \quad 𝛤 \vdash g: B⟹C}{𝛤 \vdash \text{case} \; u \; f \; g : C}

1.

Dans $NK_0$ :

     
$¬A \vdash ¬A$ $A \vdash A$  
$¬A \vdash (A∨¬A)$ $A \vdash (A∨¬A)$  
$¬(A∨¬A), ¬A \vdash \bot$ $¬(A∨¬A), A \vdash \bot$  
$¬(A∨¬A) \vdash ¬¬A$ $¬(A∨¬A) \vdash ¬A$ $(\bot I)$
$¬(A∨¬A) \vdash \bot$ $(¬I)$  
$\vdash ¬¬(A∨¬A)$ $(DN)$  
$\vdash A∨¬A$    

Donc :

𝒞\Big( 𝜆k_{¬(A∨¬A)}. k \big(𝜄_2 (𝜆x_A. k (𝜄_1 x_A))\big) \Big)

L’idée, c’est qu’on peut appliquer la loi de De Morgan au niveau de la sémantique :

On veut prouver par l’absurde (avec $𝒞$) que $¬¬(A∨¬A)$, i.e

¬(A∨¬A) ⟶ \bot

Or, si on se donne $¬(A∨¬A)$, on se donne (De Morgan) $¬¬A$ et $¬ A$. Pour prouver $\bot$, on n’a qu’à donner $¬A$ en argument (prémisse) de $¬¬A = ¬A ⟶ \bot$.

2.

𝒞(𝜆k. ku) ⟶ u \\ 𝒞(u v) ⟶ 𝒞(𝜆k. u (𝜆f. k (fv)))

A∨B = ¬A ⟶ ¬B ⟶ \bot \\ 𝜄_1 = 𝜆x (𝜆k, k'. k x) \\ 𝜄_2 = 𝜆x (𝜆k, k'. k' x)

case = 𝜆f_{A∨B}, a'_{A⟶C}, b'_{B⟶C}. 𝒞\Bigg( 𝜆 c_{C⟶\bot}. f \big(𝜆a_A. c(a'_{A⟶C} \; a_A)\big) \, \big(𝜆b_B. c(b'_{B⟶C} \; b_B)\big)\Bigg)
case \; (𝜄_1 \, u) (𝜆x. v_1) \, (𝜆x. v_2) \\ ⟶ 𝒞\Bigg( 𝜆 c. (𝜄_1 \, u) \big(𝜆a_A. c((𝜆x. v_1) \; a_A)\big) \, \big(𝜆b_B. c((𝜆x. v_2) \; b_B)\big)\Bigg) \\ ⟶ 𝒞\Bigg(\big(𝜆a_A. c((𝜆x. v_1) \; a_A)\big) u\Bigg) \\ ⟶ 𝒞\Bigg(c((𝜆x. v_1) u)\Bigg) \\ ⟶ (𝜆x. v_1) u \\ ⟶ v_1[x:=u]

EX 2

1.

Par induction structurelle sur $F$, on montre que $F \vDash F^{¬¬}$ et $F^{¬¬} \vDash F$, puis on conclut par complétude.

2.

a).

Si $u : F$,

𝜆 u'_{¬F}. \; u' u \quad : ¬¬F

b).

Si $u: F⟹G, v: ¬G$,

u \bullet v ≝ 𝜆 u'_F. v (u u') \quad: ¬F

c).

Si $u: ¬¬¬F$,

u^\circ ≝ 𝜆 u'_F. u u'^- \quad: ¬F

d).

Si $u: ¬¬(F⟹G), \; v: ¬¬F$,

u \star v ≝ 𝜆 g_{¬G}. u (𝜆 i_{F⟶G}. v(𝜆 f_F. g (i \, f))) \quad: ¬¬F

3.

  • Si $F=A$ ou $F=\bot$ est atomique :

    u_A ≝ 𝜆x_A. x^- \quad : A ⟹ ¬¬A \\ v_A ≝ 𝜆x_{¬¬A}. 𝒞(x) \quad : ¬¬A ⟹ A
  • Puis : récurrence simultanée sur $\bullet^\circ$ et $\bullet^{¬¬}$

Leave a Comment