All texts I have read on set-theoretic independence proofs consider several different sorts of constructions separately, such as Boolean-valued models (equivalently, forcing over posets), permutation models, and symmetric models. However, the topos-theoretic analogues of these notions—namely topoi of sheaves on locales, continuous actions of groups, and combinations of the two—are all special cases of one notion, namely the topos of sheaves on a site. Is there anywhere to be found a direct construction, in the classical world of membership-based set theory, of a "forcing model" relative to an arbitrary site?
Thanks to the comments by Joel Hamkins, it appears that there is an even more serious obstruction. In view of the main results of Grigorieff in Intermediate submodels and generic extensions in set theory, Ann. Math. (2) 101 (1975), it looks like the forcing posets are, up to equivalence, precisely the small sites (with the double-negation topology) that preserve the axiom of choice in the generic extension.
|show 6 more comments|