sheafのForcing

sheafを使った強制法の雑感。有限部分関数たちのある集合を取ることはやっぱりsheafで考えるとすっきりする。dense belowってのはdouble negation topologyのことで、古典的な二値論理を成立させるための装置だというのはよく分かった。とするとやはりgenericという条件が何なのかよく分からない。むしろこれはgeneric extentionとboolean-valued modelがどう対応するのかという話なのかもしれない。

あと、double negation topologyって何を潰しているのだろう。こないだIZF上の強制法のよさそうな論文を見つけたので読んでみることにする。IZFだったらdouble nagation topologyなんて使わないだろうし。