(; An expression of Russell Paradox.
sets represented as trees with arbitrary branching (indexed by a type).
def term : type -> Type.
Not : type -> type.
[A] term (Not A) --> term A -> false.
Eq : A : type -> term A -> term A -> type.
[A,a,b] term (Eq A a b) --> eq A a b.
refl : A : type -> a : term A -> eq A a a.
P : (term A -> type) -> term (P a) -> term (P b).
[A,a,P,H] leibnitz _ _ _ (refl A a) P H --> H.
Ex : A : type -> (term A -> type) -> type.
[A,B] term (Ex A B) --> ex A B.
pair : A : type -> B : (term A -> type) -> a : term A -> term (B a) -> ex A B.
def fst : A : type -> B : (term A -> type) -> ex A B -> term A.
def snd : A : type -> B : (term A -> type) -> e : ex A B -> term (B (fst A B e)).
[a] fst _ _ (pair _ _ a _) --> a.
[b] snd _ _ (pair _ _ _ b) --> b.
C : A : type -> (term A -> set) -> set.
def In : set -> set -> type.
[x,A,f] In x (C A f) --> Ex A (a => Eq Set (f a) x).
def in (A : set) (B : set) := term (In A B).
def NotIn (A : set) (B : set) := Not (In A B).
def Notinself (A : set) := NotIn A A.
def Notinselfs := Ex Set Notinself.
def R : set := C Notinselfs (fst Set Notinself).
def eqR (a : term Notinselfs) := Eq Set (fst Set Notinself a) R.
hence H2 H : false.
leibnitz Set (fst Set Notinself (fst Notinselfs eqR H)) R (snd Notinselfs eqR H) Notinself (snd Set Notinself (fst Notinselfs eqR H)) H.
pair Notinselfs eqR (pair Set Notinself R r1) (refl Set R).
def r3 : false := r1 r2.