Cohen Model

順序構造P(Power Set)から Generifc Filterを作るところまではできたので、モデル作ろうってわけですけどね。

valuation とか指標空間とかを使うんですが...

　 val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }

とか書いてある。これが定義だと。いや、だって val の定義に val 使ってるし... data で再帰的定義なのかとか
思ったんですが ( M は可算だから )、どうも、超限帰納法による定義らしい。

学部の時には、まったくわからなかったんですが、まぁ、いろいろやったからな。

val は集合なので、{} から始まって、{{}} 、さらに{{},{{}}} と進む。つまり、

　　x を V にそって分解して、val x G を再構成する

らしい。この時に、G ∋ p がくっついたものだけが、再構成されるわけね。そのまま Agda / HOD で書けたんですが、

そこからが進まない。だって、HOD だと、V=L じゃないから。なので、Vで再構成するためには、

　　順序数をVで作る必要がある

それはいやだな。できないことはないんですが。それをいうなら、ZFに沿って全部やることも可能だが

　　それでは、Agda に向いた集合論にならない

だよな。ここから、

　　M[G] : HOD
　　M ⊆ M[G]
　　M[G] ∋ G
　　M[G] ∋ ∪G

となる可算モデルM[G}を構成できれば勝ちなんですが、

　 M[G] = { val x G |　M ∋ ∃ x }

なので、そう簡単にはいかないらしい。

ところが、Mは可算モデルだから、その要素は数え上げて取ってこれる。つまり、M=Lとしてもよい。

　　¬ ( M ∋ G )

は示しているので、L に含まれない G がある、つまり、非構成的な実数があるまでは終わってるらしい。
(全体のLがMだと思えば)

M[G} の構成は、M[G]のLとMのLが同じなことを示すのに必要なだけなので、もしかして要らない?

M[G}をHODで作れないわけでもないらしいので、まだ、先は長そうです。
-