ZF 一段落

順序数のの sup (上界 ∀x∈X ψ(x)<sup ψ) だけでは足りなくて、

　　x<sup ψ → ∃y x≦ψ(y)

を入れたら Power Set までできました(これはなんだろう?)。5/8から始めたらしいのでだいたい1ヶ月だな。

最初は inductive record で書こうとしていたようですが、ZFは一階述語論理だから平坦なrecordで十分。

これで Agda で定義された順序数Ordinalと順序数定義可能集合OD、そして、若干の仮定(ODとOrdinalの順序同型と上界と上のやつ)
で、ZFのモデルを作るところまでできた。

集合論の本だと構成可能集合を使ってZFのモデルを作るあたりまでに相当します。その後、選択公理と連続体仮説やって、
さらに強制法で選択公理と連続体仮説の成立しないモデルを作るわけだな。まぁ、そのうちにやるかも。

一階述語論理だと有限個のAxiomでは記述できないとか、ψ(x,a1,a2,a3,...,an) とかの不便があるんですが、高階直観論理なAgdaだと、

　　その辺の問題は全部普通に有限な関数で記述できる

すごい。高階論理偉大すぎる。数学の本と違って構文がはっきり決まってるし。「明らかに」とか省略されているところないし。

ZFを仮定して、その仮定を絶対性とか言いながら、対象となるZFの方を <v,∈> |= ψ x みたいに書くとか、やっぱりつらい。

というわけで全体的に簡単になってます。それでいて、元の集合論のモデル構築の基本的な筋には沿っている。
なので集合論の復習にもなりました。

選択公理は順序数との順序同型があるのでいけるはずですが、 結局、L は使わなかったので、連続体仮説はどうかな。

Twitter を振り返ってみると「わからん」とか「できない」とか言ってる翌日に「わかった」とか「できた」とか書いてる。そんなものらしいです。