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^{¬¬}$