naive comprehension axiom が矛盾することをCoqで実装してみた

集合論,Coq

概要

naive comprehension axiom が矛盾することをCoqで実装します.

定義と実装

定義

naive comprehension axiom

$P$を集合論の論理式, $x$以外の自由変数は$w_0, …, w_{i−1}$で, $y$は$P$の自由変数でないとする.
$\forall w_0 \ldots \forall w_{i-1} \exists y \forall x(x\in y \Leftrightarrow P(x)).$

実装

      (* 所属関係∈ *)
Axiom In : Set -> Set -> Prop.

(* naive comprehension axiom *)
Axiom naive_comprehension_axiom :
 forall P : Set -> Prop,
 exists y : Set, forall x : Set, In x y <-> P x.

(* ラッセルのパラドックス *)
Theorem Russell_paradox : False.
Proof.
destruct (naive_comprehension_axiom (fun x => ~ In x x)).
assert (~ In x x).
intro.
apply (H x).
apply H0.
apply H0.
apply H0.
apply H.
apply H0.
Qed.

(* カリーのパラドックス *)
Theorem Curry_paradox : forall Q : Prop, Q.
Proof.
intro.
destruct (naive_comprehension_axiom (fun x => In x x -> Q)).
assert (In x x -> Q).
intro.
apply (H x).
apply H0.
apply H0.
apply H0.
apply H.
apply H0.
Qed.