Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Started literature section with several references at forcing.
Aigh, this thread on MathOverflow makes me want to shoot myself. All these people are struggling to find ways to explain forcing more clearly in the archaic “generic filter” style instead of recognizing how much more intuitive it is in topos-theoretic language. I’ve been trying to think of some way to contribute productively to the discussion (going beyond David’s brief comment), but so far I’ve been unable to find a polite way to say “y’all are putting lipstick on a pig.”
Yes, it’s incredible. The fact the difficulty comes from simulating material sets in a filterquotient topos should be much better known. I think you should write something. It would be much more authoritative than my offhand comment, and would emphasise it’s not just one minor player’s viewpoint.
Perhaps creating a filterquotient article (currently it does not exist) could be a good start.
That would indeed be good. I’ve always been slightly unsatisfied with the treatment in Mac Lane and Moerdijk, and Johnstone put off writing a more full account to volume 3 of the Elephant.
Well, I wrote something. I didn’t bring in the filterquotients, partly because I don’t entirely understand exactly how a filterquotient construction corresponds to the use of filters in traditional membership-based forcing (mainly because I don’t really understand the latter), and partly because I preferred to make the point that it isn’t really necessary to bring in filters at all. But if you want to add something about filterquotients that would be great.
Nice. And I would write something about filterquotients if I was more confident about it past more of an analogy.
Interesting that Mike compares forcing to the extension of rings in view of the analogy Anel and Joyal elaborate in Topo-logie:
The structural analogy between topos/logos theory and affine schemes/commutative rings has been a folkloric knowledge among experts for a long time. However, this point of view is conspicuously absent from the main references of the theory. When it is mentioned in the literature, it is only as a small remark. (p. 4, n5)
Who was it who first understood that forcing can be understood topos theoretically? It is quite an amazing insight!
The first account we list (here) is way back from 1977.
Also these discussions as on MO seem to keep re-occuring every few years. I gather the set theory community is exerting effort to not appreciate the message.
Thanks! It’d be great if we could pin down the history a bit more exactly. The introduction to ’First order categorical logic’ attributes the insight somewhat vaguely to Joyal and Reyes in the early 70s. Does the following article mention it (I do not have access)?
https://www.tandfonline.com/doi/abs/10.1080/01445340.2018.1554471?af=R&journalCode=thpl20
I have extracted the relevant passage of the article to the Sandbox.
Not sure if that’s useful. It ends up pointing to Johnstone’s “Topos Theory”.
added these references:
Myles Tierney, Forcing Topologies and Classifying Topoi, pages 211-219 in: Alex Heller, Myles Tierney (eds.) Algebra, Topology, and Category Theory: A Collection of Papers in Honor of Samuel Eilenberg, Academic Press 1976 (doi:10.1016/C2013-0-10841-0)
Peter Johnstone, pages 270, 273, 348, 353 of: Topos theory, London Math. Soc. Monographs 10, Acad. Press 1977, xxiii+367 pp. (Available as Dover Reprint, Mineola 2014)
It’s in Lawvere’s 1970 ICM talk Quantifiers and sheaves, reporting on joint work with Tierney.
You mean on p. 5 here?
Interesting, thanks! The history of forcing (which I don’t know much about, though I’ve looked at the topos theoretic account of the continuum hypothesis in the past) itself seems complicated. The insights of Joyal seem to come from one strand (Kripke semantics), whilst the Lawvere-Tierney work seems more directly related to Cohen’s work. Maybe all that can be said is that the insight was up in the air and emerged in Canada at the end of the 60s/early 70s.
I just read that MO thread and it seems maximally cursed LOL — but thank you Mike for the beautiful and very detailed answer on that page. Posts like that are one of the reasons I love MO.
Part of me wants to understand what it is that the set theorists are actually studying when they say they are doing something that is not isomorphism-invariant! On the face of it this sounds really impossible (if it really is true, then it must be true after all that set theory / logic is not real mathematics after all!), but it seems like there must be some other way to understand what they are interested in. The other part of me is not sure I want to know.
After a private email discussion, Asaf has backpedaled his claim at the MO discussion and now agrees that even “standard” forcing is isomorphism-invariant.
What a relief! Sounds like progress.
1 to 21 of 21