ZF集合論

これも、そのうちやろうと思ってたんですが、なんとなく手を付けてしまいました。Agda で書くわけですが、

　　ZFって、なんでもかんでも集合で型とかない

おいおい。しかも一階述語論理なので∀とか∃とかが出まくりで良くわからない。Agda に慣れすぎたかも。

　　Agda の集合は型があるので a : A と b : B を a : A ∪ B とかすることはできない

Stackoverflow にも「AgdaのSetは、集合論のSetとは別もの」とか書いてある。まぁ、Type だよね。本来は。

なので、方針的には

　　Agda のrecord ZFで、ZFSet と演算子∋, ∪, ⊆などを定義する
　　record IsZFで、ZFの公理を定義する
　　その時に∃xは関数で置き換える

例えば

　　 ZFSet : Set n
　　 _∋_ : ( A x : ZFSet　) → Set m
　　 _≈_ : ( A B : ZFSet　) → Set m
　　 ∅　: ZFSet

こんな感じ。正則の公理、

　　 ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )

は、

　　 minimul : ZFSet → ZFSet
　　 regularity : ∀( x : ZFSet　) → ¬ (x ≈ ∅) → (　minimul x ∈ x ∧　( minimul x　∩ x　≈ ∅ ) )

と関数にわけます。

あとは、このrecordを満たすモデルを作ればよい。本によると、順序数(Ordinal)を作って、それから関数で部分集合を作り、それを
構成可能集合とする。とあるな。Ordinal は自然数の二重ループみたいな data で良いんじゃないかな。関数で部分集合とるのは
Agda は得意。

構成可能集合まではできたが、これからZF record を作るのは大変そう。まだ、できるかどうかわからないな。

あと、( y ∈ x ) ∨ ( ¬ y ∈ x ) なのを使うみたいなんだけど、直観主義論理な Agda だとそれは使えないんだけど。どーするの?

しばらく楽しめそうです。

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/ZF-in-agda/file/tip/zf.agda