Generic Filter

順序構造P上の Generic Filter 作って、集合論のモデルを作り、連続体仮説とか選択公理の否定をやるあれですね。

ブール代数を使う方が良いらしいんですが、公理的集合論とKunenとかの古い本はそうではなくて。

Generic Filterの方向が割と謎で、いろいろ間違ってる。結局、反対方向のIdealでやることに。さらに、

　　位相空間論で使う ideal と、少し定義が違う

いや、違ってても同じだろと思ってたんですが、ideal ⊆ L ⊆　Power P でやるんですが、

　　　 ideal1 : { p q : HOD } →　L ∋ q　→ ideal ∋ p →　q ⊆ p　→ ideal ∋ q
　　　 ideal2 : { p q : HOD } → ideal ∋ p →　ideal ∋ q　→ L ∋ (p ∪ q) → ideal ∋ (p ∪ q)

なんですが、二つ目に差があって

　　　 ある ideal e　があって、 p ⊆ e ∧　q ⊆ e

になってる。位相空間論だと L = Power P でやるので、p ∪ q がL に必ず入るので、(p ∪ q) ⊆ e から ideal ∋ (p ∪ q)がでる。
なので両者は同じなんですが、L ⊆　Power P だと、L ∋ (p ∪ q) とは限らないので、そうならない。ひどい。

それがわかれば、割と簡単に書けた。所詮、可算モデルな集合Mから作る可算集合G ⊆ L なので、自然数Nの入力する関数だからな。

Generic Filter は稠密な集合と必ず交わるという性質があるけど、そっちは影響を受けない。けど、部分関数なPを使って、

　　　¬ ( M ∋　G)

を示そうと思うと二つ目の条件の差が効いてくるという感じなので少しはまりました。

Ideal なのは要素毎の補集合をとれば filter になるので、まぁ、いいかってところです。