0
大学数学基礎解説
文献あり

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

127
0
$$$$

概要

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.
    

注意

ZFCなどは naive comprehension axiom を弱めて上記のような証明ができないように制限されたバージョンの公理が採用されています。

参考文献

投稿日:202113

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。

投稿者

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中