ε-induction

ちょっと、blog お休みしてました。

まだ、しつこくやってる Agda → ZF ですが、正則公理の minimum が選択公理の choice function になってしまう問題だけど、正則公理

　　∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )

の ∃ y ∈ x が論理式の中に閉じてる時には独立選択公理といって、選択公理よりは弱い公理ならしい。これを、

　　 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
　　 regularity : ∀( x : ZFSet　) → (not : ¬ (x ≈ ∅)) → (　minimul x not　∈ x ∧　(　minimul x not　∩ x　≈ ∅ ) )

みたいにスコーレム関数として要求してしまうと、選択公理になってしまうので、minimulが choice functionなのは正しい。

でも、これでは困るわけですが、直観主義論理用の別な正則公理の表現があって、ε-induction と呼ばれているらしい。

　　 ( ∀ x y → ( x ∋ y → ψ y ) → ψ x ) → (∀ x → ψ x)

古典論理で変形すると普通の正則公理になるらしいです。で、こっちは証明できた。この induction は要するに、

　　集合を空集合から ∋ を逆にたどって任意の集合にたどり着ける

というもの。確かに∋の列には終わりがあるのと似てる。今は OD と順序数の対応があるので、x y に対応する順序数のinductionで証明すれば良い。

なかなかできなかったんですが、順序数は要するに二次元配列なので、それを展開してinductionしてやるとできました。

で、前に power→ 仮定したのは少し気まずくて直観主義論理では禁止されている ¬ ¬ A → A に相当するらしい。

なので、そこは諦めて、

　　power→ :　( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)

ここまでかな。 少し弱いけどAgdaだとここまでらしい。これで、正則公理と選択公理を分離できて全部終了という感じらしいです。

少し文献を探してみると、1974 の Osius and Lawevre の Categorical Set Theory というのがあって、Elementary well-pointed topos (EWPT) ってので、集合論のモデルを作れるとある。こっちは、

　　P : A → Ω

という CCC 上の Power Set Function を使って、Transitive Set Object を作り、それとさらに、A との A ∩ (P A)を取ってSet Object を作ると言う方式らしい。使っている公理が圏論で書かれてるので読みづらいです...

自分のは

　　Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )

なので、近いっちゃ近いかな。Def は transitive なので。

でも Oisus のはモデル論なので、実際に公理の論理式を証明してみせているわけではないけど、
証明論的なのもできるとは書いてあったので、それを確認したと言うこところかな。