ZF集合論一段落

なんか、前にも一段落と書いた気がするが気にしない。

　record OD {n : Level}　: Set (suc n) where
　　field
　　　 def : (x : Ordinal {n} ) → Set n

順序数上の述語を集合と見なすのを順序数定義可能集合(Ordinal Definable Set)というわけですが、これが

　OD ≈ Ordinal

という順序同型写像を持つというのと(あと色々な仮定)を入れてZFの公理を証明してやろうというわけですが、

この写像の→は良いんだが←を集合の∈と見なすと「全部の集合が順序数になってしまう」つまり、必ずOD(+仮定)が空集合を含んでしまう。

ってので困ったので←をはずそうっていうわけですね。結構、難航してたんだけど、

　 ¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )　→ p

ってのを入れるってのを思いついたので、一通りできました。直観主義論理なので∃を使えない。なので、対偶を使ってやろうというわけ。

ちなみに証明できてないので仮定。順序数上の定理なので証明できそうな気もするが...

A のPower Set を順序数のPower Setの要素 x を A ∩ x に置換するってのを思いついたのだが、その時に、

置換公理の Elimination が ∃ を要求するのに気がついて、苦し紛れにこれを使いました。

結局、Union もこれで乗り切った。しかし、Union を使う無限公理がおかしなことに。それも適当に乗り切れた。

でも、選択公理を証明しようとしたら、正則公理の minimum がそのまま選択関数になっていることを発見。

まぁ、いろいろ変だが、空集合を含む集合のモデルは作れたみたいなので良しとするかというところですね。

あとやるとすると、

　　濃度の定義
　　連続体仮説
　　選択公理を満たさないモデルの生成(minimumはどうするんだ?)

くらいでしょう。

https://github.com/shinji-kono/zf-in-agda