Russell's paradox についての形式化を行います。この記事においては Russell's paradox とは、以下の命題のことを指します。
Russel's_paradox
任意の集合 x について x ∈ V が成り立つような集合 V は存在しない。
この命題の Coq における形式化についての証明を本記事では紹介します。
Proof
Axiom classic: forall P:Prop, P \/ ~P.
Axiom Univ: Type.
Definition set := Univ.
Axiom set_in : set -> set -> Prop.
Notation "x \in y" := (set_in x y) (at level 20, no associativity).
Axiom AxExt:
forall x y: set, (forall z: set, z \in x <-> z \in y) -> x = y.
Axiom Separation_Scheme: (set -> Prop) -> set -> set.
Notation "P \and x" :=
(Separation_Scheme P x) (at level 15, no associativity).
Axiom AxSS:
forall (P: set -> Prop) (x: set),
forall z: set, z \in (P \and x) <-> z \in x /\ P z.
Definition is_small (P: set -> Prop): Prop :=
exists x: set, forall y: set, (y \in x <-> P y).
Definition full_set (x: set) : Prop := True.
Definition Russell_check (x: set) : Prop :=
(x \in x) -> False.
Theorem there_is_no_fullset:
is_small full_set -> False.
Proof.
unfold full_set.
unfold is_small.
intro.
destruct H.
assert (forall y: set, y \in x).
unfold iff in H. intro.
specialize (H y). destruct H. apply H0. trivial.
clear H.
assert (exists z: set, z = Russell_check \and x).
exists (Russell_check \and x). trivial.
destruct H.
pose proof AxSS as AxSS.
specialize (AxSS Russell_check x). unfold iff in AxSS.
specialize (AxSS x0).
destruct AxSS as (AxSS1 & AxSS2).
assert (x0 \in x0 -> ~ x0 \in x0).
intro.
assert (x0 \in x /\ Russell_check x0).
apply AxSS1. rewrite <- H. exact H1.
destruct H2.
unfold Russell_check in H3.
unfold not. trivial.
assert (~ x0 \in x0 -> x0 \in x0).
assert (x0 \in x). apply H0.
unfold not. intro.
assert (Russell_check x0). unfold Russell_check. trivial.
rewrite <- H in AxSS1.
rewrite <- H in AxSS2.
clear AxSS1 H1 H3.
apply AxSS2. split. trivial. trivial.
assert (x0 \in x0 \/ ~ x0 \in x0). apply classic.
destruct H3.
assert (~ x0 \in x0). apply (H1 H3).
unfold not in H4. contradiction.
assert (x0 \in x0). apply (H2 H3).
unfold not in H3. contradiction.
Qed.