1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:
31:
32:
33:
34:
35:
36:
37:
38:
39:
40:
41:
42:
43:
44:
45:
46:
47:
48:
49:
50:

(* Gewährt, von Mengen zu sprechen *)
Axiom Menge: Type.

(* Gewährt, von Elementbeziehungen zu sprechen *)
Axiom In: Menge -> Menge -> Prop.

(* Gewährt, von Komprehension zu sprechen *)
Axiom comp: Menge -> (Menge -> Prop) -> Menge.

(* Axiom der Aussonderung *)
Axiom comp_ax: forall (X: Menge ) (P: Menge -> Prop) (x: Menge),
  In x (comp X P) <-> In x X /\ P x.

(* Die »Allmenge« *)
Axiom All: Menge.
Axiom all_ax: forall x: Menge, In x All.

(* Die Russelmenge *)
Definition Rpred := fun x => ~In x x.
Definition R := comp All Rpred.

(* Aussagenlogik *)
Theorem iff_contra (A: Prop): ~(A <-> ~A).
Proof.
  intro h. destruct h as (f, g).
  assert (na := (fun a => (f a) a)).
  exact (na (g na)).
Qed.

(* Aussagenlogik *)
Theorem iff_simplify (A B C: Prop):
  A -> (B <-> A /\ C) -> (B <-> C).
Proof.
  intro a. intro h. destruct h as (f, g).
  split.
  * intro b. exact (proj2(f b)).
  * intro c. exact (g (conj a c)).
Qed.

(* Ableitung der Kontradiktion *)
Theorem paradox: False.
Proof.
  assert (p := comp_ax All Rpred R).
  unfold Rpred in p.
  replace (comp All (fun x => ~ In x x)) with R in p
    by reflexivity.
  apply (iff_simplify _ _ _ (all_ax R)) in p.
  exact (iff_contra _ p).
Qed.