集合論(無限の公理)

無限公理、少し苦労したんですが終わりました。AgdaのInternal Errorに泣いたがバグレポしたら最新版でテストしろと。まぁ、そうだよな。でも、最新版についていくのはつらい。

置換公理は仮定で入れてしまったので、残りはPower Setだけです。他も苦労したので、これも苦労するはずです。

順序数の方程式としての順数定義可能集合OD(本来はその推移的な部分集合)でZFのモデルを作るわけですが細かいところが面白かった。

順序数には直後順序数というのがある。つまり、Suc ですね。Suc を積み重ねても次のレベルにはいけないがどの順序数にもある。

Suc には割り込めない。つまり、x と Suc x の間にある元はない。ということは、

　　Suc x ∋ y なら x ≡ y ∨ x ∋ y

なるほど。つまり、これを順序数のSucについて証明して間にある元がないということを証明できました。そうしないで、順序数から割り込みがないことを示すのは難しい。

でも、そこで順序数の定義を複雑にし過ぎてきたことに気がついた。レベルのある自然数で十分らしい。

　　data OrdinalD {n : Level} :　(lv : Nat) → Set n where
　　　 Φ : (lv : Nat) → OrdinalD　lv
　　　 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv

　　record Ordinal {n : Level} : Set n where
　　　 field
　　　　 lv : Nat
　　　　 ord : OrdinalD {n} lv

　　data _d<_ {n : Level} :　 {lx ly : Nat} → OrdinalD {n} lx　→　OrdinalD {n} ly　→ Set n where
　　　 Φ<　: {lx : Nat} → {x : OrdinalD {n} lx}　→　Φ lx d< OSuc lx x
　　　 s<　: {lx : Nat} → {x y : OrdinalD {n} lx}　→　x d< y　→ OSuc　lx x d< OSuc　lx y

　　_o<_ : {n : Level} ( x y : Ordinal ) → Set n
　　_o<_ x y =　(lv x < lv y )　∨ ( ord x d< ord y )

これだけで十分らしい。レベル間の相互作用がまったくないけど、それでいいのか。

なんとなく、ZFの公理に引きずられてUnionとかを論理式で定義ししそうになるんですが、それではだめらしい。あくまでも、

　　集合の構成は順序数の大小関係で定義する

方式。 x ∈ Union X は、Suc x < X みたいな感じ。Pair も実は、

　　Max ( Suc x , Suc y )

だった。無限公理には、x ∈ infinite →　 x ∪ { x } ∈ infinite というのが出てくるけど、

　　{ x } (xだけを含む集合) は、pair で ( x , x )

要素二つの A ∪ B は Union (A , B) なので、結局、

　　Union (x , ( x , x )) ∈ infinite

と言う形に。z ∈ Union (x , ( x , x ))

　　 Suc z < Suc ( Max ( Suc x , Suc x ) )

になるので、結局、

　　 z < Suc x

に。そして、z < y という条件のODは、y という順序数に対応する集合そのものなので、Union (x , ( x , x ))　は、

　　 Suc x という順序数に対応する集合

ということになり、無限集合の公理は、x が含まれていれば Suc x が含まれている集合が存在するということになるということでした。

ただ、これを Agda で丁寧に変換していくので、結構、大変でした。残りは冪集合(Power Set)だけだが....

-