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.

$$