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?
$\begingroup$
$\endgroup$
1
asked Jan 30, 2010 at 16:39
-
$\begingroup$ Mike, you might want to add the "forcing" tag. $\endgroup$– Joel David HamkinsCommented Jan 30, 2010 at 18:01
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
12
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.
answered Jan 30, 2010 at 17:44
-
$\begingroup$ Thanks! I agree that such crossovers are sorely lacking. Is it really true, though, that the double-negation topology is the only one that makes sense for classical set theory? I mean, there are other topologies which still give rise to Boolean topoi, aren't there? Anyway, even double-negation topologies on arbitrary categories are a larger common generalization of those on posets and groups which seem to mostly pervade the set-theoretic literature. $\endgroup$ Commented Jan 30, 2010 at 17:54
-
2$\begingroup$ Isn't it also true even that the work on symmetric and permutation models is a relatively minor part of the applications of forcing? Indeed, I class the symmetric model/permutation model ideas along with the many methods of describing inner models (which are numerous and highly developed), rather than as particularly connected with forcing. Most of the interest in forcing among set theorists has been in a fully classical, full ZFC context, exploring the ubiquity of ZFC independence. I would guess that more than 95% of the forcing arguments in the literature use the axiom of choice. $\endgroup$ Commented Jan 30, 2010 at 18:16
-
1$\begingroup$ @Joel: There is more to the site approach than just the unification of forcing models and symmetric models, it is a natural and much more general framework which happens to contain both as special cases. To transpose the chicken and the egg, wouldn't it be possible that the fact that there are so few symmetric models compared to forcing models is a result of the division of the two? I think the fact that symmetrizing is commonly viewed as an extra step after forcing makes it less accessible as a tool. $\endgroup$ Commented Jan 30, 2010 at 18:58
-
4$\begingroup$ My point instead is that we are simply less interested in the models that symmetry/permutation give rise to, as by design Ac fails in them. There are such deep applications of forcing, which seem to reveal fundamental aspects of the nature of sets, which don't require us to give up AC or classical logic. (e.g. cardinal invariants, proper forcing axiom, large cardinals and forcing, etc. etc.). $\endgroup$ Commented Jan 30, 2010 at 19:27
-
4$\begingroup$ So, from an opposingly biased perspective, one might say that the reason for set-theorists' focus on poset-based forcing is their addiction to the axiom of choice? (-:O $\endgroup$ Commented Feb 1, 2010 at 2:06
$\begingroup$
$\endgroup$
1
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.
$\begingroup$
$\endgroup$
1
Are you familiar with this paper : Relating first order set theories and elementary toposes from Awodey,Butz,Simpson and Streicher. I haven't read in detail yet, but it really seems to provide a machinery that answer your question.
I would also add that if such "general" theory as not been developed much is because (this is my personal opinion) it would be essentially useless:
For model theorist, because of the various representation theorems for toposes and boolean toposes, it is know that all the eventual model of set theory you could get this way can be obtained by first taking a permutation model and then taking a boolean valued model model inside of it. What I mean is that any boolean Grothendieck topos is localic over the classyfing group of a pro-discrete topological group, and even worst, any Grothendieck topos satisfying the axiom of choice admit an etale covering by a boolean locale.
And for topos theorist, well the main difference between a model of set theory and a topos is the possibility of comparing two arbitrary object for the membership relation, and I hardly see how this feature can be relevant for topos theory.
answered Jan 22, 2015 at 8:47
-
3$\begingroup$ I am familiar with that paper, and it doesn't answer my question. But thanks! (I do know about the representation theorems for toposes, but I personally find the general notion of site to be very helpful conceptually, and I'm slightly surprised if there are no set theorists in the world who feel similarly.) $\endgroup$ Commented Jan 23, 2015 at 7:32