HOD

順序数方程式である Ordinal Definable てっのを使う ZF Set Theory の Model を Agda 内で作るってのをやってたわけですが、
OD には「全部の順序数」という自明な最大があり、最大のない順序数に対応させるのは変だなと思ってたのだが、

<-osuc (c<→o< { record {　def = λ x → One } } )

とすると⊥が出てしまう。これは大変よろしくない。つまり最大のODの次の順序数に対応するODが撮れて矛盾してしまう。

sup でも osuc を返す関数という自明にsupのない関数があって、定義域を狭める必要があるらしい。

つまり、ODの解がある順序数で抑えられないと、よろくないらしい。古典集合論では

　HOD { x | TC x ⊆ OD } Hereditarily Ordinal Definable

ってのを使う。TC は推移閉包で、つまりxの要素は全部ODっていう性質を持つものらしい。ここで x は V つまり宇宙を動く。

でわかったんですが、OD ってのは解が順序数の中で抑えられてない場合があって、それは集合でなくてクラスなわけだ。

ということは逆に解が上限を持つことが HOD の条件になる。つまり、

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

　　record HOD : Set (suc n) where
　　　field
　　　　od : OD
　　　　odmax : Ordinal
　　　　<odmax : {y : Ordinal} → def od y → y o< odmax

としてやれば良い。これで矛盾は避けられる。順序数との対応はHODだけにするってのでいけるみたい。

この方がクラスと集合の区別もはっきりする。順序数の縮小写像を使うと集合の中でOD/HODを使ったモデルを作ることも可能。なるほど。
中から見るとクラスだが外から見ると集合ってのもわかりやすい感じ。

　　record ODAxiom : Set (suc n) where　　　
　　 field
　　　od→ord : HOD　→ Ordinal
　　　ord→od : Ordinal　→ HOD　
　　　c<→o<　:　{x y : HOD　}　 → def (od y) ( od→ord x ) → od→ord x o< od→ord y
　　　⊆→o≤　:　 {y z : HOD　}　 → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
　　　oiso　 :　{x : HOD }　　　→ ord→od ( od→ord x ) ≡ x
　　　diso　 :　{x : Ordinal }　→ od→ord ( ord→od x ) ≡ x
　　　==→o≡ : { x y : HOD　}　　→ (od x == od y) → x ≡ y
　　　sup-o　:　(A : HOD) → (( x : Ordinal ) → def (od A) x →　Ordinal ) →　Ordinal
　　　sup-o< :　(A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →　Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<　sup-o A ψ

Power Set の odmax が良くわからなかったんですが、⊆ が集合の順序を制約するとすると良い。この方が自然。ただし、⊆→o≤ から c<→o<　はでないらしい。

Union / Replace の上限も「そういえば教科書にそういうの載ってたな」的に証明できる。

最後に無限公理で行き詰まったのですが、

　　Union (x , (x , x))

は順序数との対応で特に上限が指定されてない。なので、どんどん大きくなる可能性がある。濃度とかで抑える方法も考えたんだけど、

　　面倒くさいので、ωはあるってことで仮定

で、治ったようです。ちょっとださいがまあ良い。

sup の定義域にも制限が付いたので、気になっていた(気にしてたならなおせよ)ところはなくなったみたい。

他の部分の証明(ブール代数や filiter、順序対)も大した修正でなく終わりました。

選択公理から排中律が出るところ、その逆、ε induction から正則公理も HOD で問題ないらしい。

超限帰納法のレベルが合わなくて n と suc n と二つあるが、まぁ、いいか。

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