Union in ZF

集合論の話。(いや、最近はCCCの方をいじってて、進捗あったようなないような状態なんですが)

Agda で書いた ZF のモデル、そういえば選択公理を分離しておいた方が良いなとか思って見直したんですが(逃避ともいう)

　Union (A , B) ⇔ A ∪ B

とかをBool代数関連で証明してるんだが、なんか選択公理を使うとある。え? それは変だろ。まぁ、右辺を左辺で定義すれば良いんですが、右辺は、

　(x ∈ A ) ∨ (x ∈ B)

で、( A , B ) は A と B の非順序対、つまり、A と B を要素とする集合だな。いや、当たり前に成立するべきでしょ。

なのだが、Union の公理は

∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))

これで、∃ を関数で書いて

　　 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
　　 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))

としてます。¬ で右辺の ∃ を逃げてる感じ。なので、Union (A , B) → A ∪ B を書き下すと

　　¬ ¬ ( x ∈ A ∨ x ∈ B )

となり二重否定を解除する必要がある。でも、

　　直観主義論理だと二重否定は解除できないが、選択公理があればできる

なので選択公理が必要ならしい。

で、なんとか手に入れた Kunen 先生の本を見直してみると、

　　 ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z

しかない。え? 片方だけ? 双方向じゃないの? どういうこと? いろいろ見直してみると、

　　田中先生の公理論的集合論は⇔
　　コーエン先生の連続体仮説は⇔
　　Wikipediaは⇔
　　シェーンフィールドは分出公理と置換公理からUnionを作る

みたいな感じ。やっぱり双方向だよな。古典論理だと二重否定は解除できるのでこれで問題ない。でも、自分のやり方は直観主義論理だから困る。

Kunen は pair と Power Set も片方向なんですが、そこで思いついた。Kunen先生の pari の公理、

　　∃ p → x ∈ p ∧ y ∈ p

だと、他にも要素が入ってることを排除できないので片方向なのだが、分出公理でさらに限定すれば良い。分出公理は双方だから逆も言える。

UnionもPower Setも同じ方法が使えるかも。で、読み進めてみると、

　{ z ∈ p | z = x ∨ z = y }

という形で使うらしい。この形は分出公理そのものなので、やっぱりそういうことか。

この方法だと、入力に使うと条件に否定が付くので自分が書いたのと同じになる。つまり、

　　Kunen先生の本の定義は、直観主義論理にも対応した形になっている

ってこと。さすがです。Kunen 先生。

https:www.amazon.com/dp/0444868399