Set-theoretic forcing over sites?

To the best of my knowledge, this has never been "officially" described in the set theoretic literature. This has been described by Blass and Scedrov in Freyd's models for the independence of the axiom of choice (Mem. Amer. Math. Soc. 79, 1989). (It is of course implicit and sometimes explicit in the topoi literature, for example Mac Lane and Moerdijk do a fair bit of the translation in Sheaves in Geometry and Logic.) There are certainly a handful of set theorists that are well aware of the generalization and its potential, but I've only seen a few instances of crossover. In my humble opinion, the lack of such crossovers is a serious problem (for both parties). To be fair, there are some important obstructions beyond the obvious linguistic differences. Foremost is the fact that classical set theory is very much a classical theory, which means that the double-negation topology on a site is, to a certain extent, the only one that makes sense for use classical set theory. On the other hand, although very important, the double-negation topology is not often a focal point in topos theory.


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.


At http://www.mathematik.tu-darmstadt.de/~streicher/forcizf.pdf one can find a paper describing a forcing semantics for IZF in Grothendieck toposes Sh(C,J) in terms of the site (C,J) where C is a Grothendieck topology on a small category C.

As mentioned in the paper for the case of presheaf toposes this was done already by D. Scott before. In my forcing interpretation the "names" for sets are coming from the cumulative hierarchy in the presheaf topos. Sheafification is built into the clauses of the forcing semantics. Instantiating C by a poset gives the usual "names" and when taking for J the double negation topology on C we get Cohen forcing.

In this context it might be worthwhile to mention that boolean Grothendieck toposes are precisely as subtoposes of presheaf toposes via the double negation topology. This is due to Freyd and is also described in Blass and Scedrov's AMS Memoir. In this booklet they relate Freyd's models refuting AC to the more traditional symmetric boolean valued models as employed by Cohen for refuting (even countable) AC. Freyd's first model coincides with the one devised by Cohen but Freyd's second modelwasn't considered before in the set-theoretic literature.

It might be worth mentioning in this context the famous result of Peter Freyd that every Grothendieck topos appears as an exponential variety within a topos boolean over the Schanuel topos (the generic permutation model used by A. Pitts in his work on "Nominal Sets"). So Grothendieck toposes are not that different from models of set theory...

Thomas

PS My above mentioned article has appeared in the Festschrift for my good old friend Mamuka Jibladze.