TD8 : Paradoxe de Russel

EX 1

u ≝ 𝜆 x_{S \in S} . \underset{: \neg (x \in x) [x := S] = \neg (S \in S)}{\underset{⏟}{E_{\in} (x)}}

Or : en posant $F ≝ x ⟶ \neg x$ ,

\frac{⊢ u : F [x := S] = \neg (S \in S)}{⊢ I_{\in} (u) : S \in {x ∣ \neg (x \in x)}}

Donc

v ≝ I_{\in} (\underset{: \neg (S \in S)}{\underset{⏟}{𝜆 x_{S \in S} . u x}}) : S \in S

u v v : ⊥

\begin{aligned} u v v & = (𝜆 x . E_{\in} (x)) v v \\ ⟶_{𝛽} E_{\in} (v) v \\ ⟶_{𝛽} E_{\in} (I_{\in} (𝜆 x_{S \in S} . u x)) v \\ ⟶_{𝛽} (𝜆 x_{S \in S} . u x) v \\ ⟶_{𝛽} u v v \end{aligned}

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

Pour le schéma de récurrence :

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

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