TD8 : Paradoxe de Russel

Énoncé

EX 1

1.

u ≝ 𝜆x_{S∈S}. \underbrace{E_{∈} (x)}_{: ¬(x∈x)[x:=S] = ¬(S∈S)}

2.

Or : en posant $F≝ x ⟶ ¬x$,

\cfrac{\vdash u : F[x:=S]= ¬ (S∈S)}{\vdash I_∈(u) : S∈ \lbrace x \mid ¬(x∈x) \rbrace}

Donc

v ≝ I_∈(\underbrace{𝜆x_{S∈S}. ux}_{:¬(S∈S)}) : S∈S

et

uvv : \bot

3.

\begin{align*} uvv & = (𝜆x. E_∈(x))vv \\ & ⟶_𝛽 E_∈(v)v \\ & ⟶_𝛽 E_∈(I_∈(𝜆x_{S∈S}. ux))v \\ & ⟶_𝛽 (𝜆x_{S∈S}. ux)v \\ & ⟶_𝛽 uvv \end{align*}

EX 2.

1.

   
  $x: j ≃ j \vdash x: j≃j$
  $x: j ≃ j \vdash x: s(j)≃s(j)$
  $\vdash 𝜆x. x : j≃j ⟶ s(j)≃s(j)$
  $\vdash 𝛬j. 𝜆x. x : ∀j. j≃j ⟶ s(j)≃s(j)$
$\vdash r_0 : 0≃0$ $\vdash 𝛬j. 𝜆x. x : ∀j. j≃j ⟶ s(j)≃s(j)$
$\vdash R_{r_0, 𝛬j. 𝜆x. x, s} : 0≃0$  

2.

 
$x: 0 ≃ S(i) \vdash x: 0 ≃ S(i)$
$x: 0 ≃ S(i) \vdash x: \bot$
$\vdash 𝜆x. x: 0 ≃ S(i) ⟶ \bot$
$\vdash 𝛬i. 𝜆x. x: ∀i. 0 ≃ S(i) ⟶ \bot$

Pour les règles (4-8) : on procède de même.

Pour le schéma de récurrence :

𝜆x_{F[i:=0]}, \, h_{∀j. F[i:=j] ⟶ F[i=S(j)]} \, 𝛬i. R_{x, h, i}

1 bis.

𝜆x.x : s≃t ⟶ S(s)≃S(t)

2 bis.

$$

Leave a comment