minimum, ε-induction, choice

ZF と ZFC は分離するべきだよなと思って、少しいじったんですが、

sup は常に ord→od の形で使っていることに気がついた。OD は順序数方程式なので「全部が解」という最大値があるので、ord→od には最大値がある。

なので、常にsupがあるわけね。なのでそう書き直しましたが

ZFSet : OD

には変わりはない。ZFSet には最大値つまり順序数全体は入らないわけですが、ここだと入りそうな気がする。しかし、仮定からは OD の最大値がある。

この辺は少し変。でも、そういうものなのだろう。

正則公理の存在記号を関数に置き換えると、実は選択公理と同じになってしまう。その代わり、ε-induction が使えるんですが、

正則公理を 、ε-induction から出すには選択公理が必要。でも実際にやってはいなかった。なので、やってみることに。

が、いがいにかたい。ε-inductionはすべての集合で、自分の要素で成立している仮定で証明できれば全部の集合で成り立つというもの。

OD ではもちろん TransFinite から出るんですが、それより制限がきつい。正則公理の minmam は共通集合なので TransFinite では使えるが、ε-induction　ではだめ。

なので、ちょっとチートしてぐぐったら、

　自分を含む集合で成立するのを induciton すれば良い

ってのが出てて、それでできました。なるほどね。これだと自分を含むから空集合でないのは自明だし。

ただし、選択公理は使いまくり。まぁ、選択公理の別形式を証明しているようなものだからな。排中律も使うし。

圏論は、この手の構成的でない推論を区別しながら展開できる。そのたのツールなのかも。

コーエン先生の本には「選択公理や連続体仮説を仮定しない数学が展開されるようになる」と書いてますが、圏論がそういうものだったんだろうな。

集合は扱いづらいしね。集合論は残りは Cardinals と Filterを使ったモデルだが、どこまでやるかは謎。

そういえば、Agda で構成した ZF は選択公理抜き。ただし、ODは整列されてる。しかし、排中律抜きには、そこから順序を取り出すことはできない、そんな感じみたい。

順序数は全順序だからな。