Timeline for A better way to explain forcing?
Current License: CC BY-SA 4.0
40 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 24, 2023 at 0:05 | comment | added | Mike Shulman | @JamesHanson I don't know enough about fancier versions of forcing to answer questions like that. David Roberts has thought some about class forcing in topos theory. | |
| Nov 23, 2023 at 5:13 | comment | added | James E Hanson | @MikeShulman Do you expect class forcing to be straightforward to develop in ETCS+R? I don't know that much about class forcing and I don't have explicit experience with ETCS+R, but it seems to me that things involving the large-scale structure of proper classes (e.g., most of inner model theory) would be easier to formalize in a context where the large-scale structure of models is rigidly controlled. | |
| May 1, 2022 at 0:26 | comment | added | Mike Shulman | Functoriality is a bit tricky to make sense of, since you have to specify what a "map of models of ZFC is" which isn't necessarily obvious. Mitchell claimed that the constructions are adjoint functors in some sense. | |
| May 1, 2022 at 0:24 | comment | added | Mike Shulman | @user40276 The original proofs were due to Cole, Mitchell, and Osius. Maybe I can be forgiven for pointing to my own arxiv.org/abs/1808.05204v2, which includes all those citations, and which does the same constructions in a more general context using a version of the replacement axiom that I think is more useful in practice. | |
| Apr 30, 2022 at 19:09 | comment | added | user40276 | Sorry for commenting two years later. Still, where can I find a proof that of such bijection between models of ZFC and ETCS+R? Also is such construction functorial isomorphism or just a bijection? | |
| Sep 1, 2020 at 0:23 | comment | added | Mike Shulman | @TimCampion Yeah, there's definitely room for a nice expository article there. | |
| Aug 31, 2020 at 23:34 | comment | added | Tim Campion | I have not attempted to read all the comments; this might be redundant: I'd love to see an article implementing this overview in detail. It would be nice to carry it to the point of looking at a few specific famous examples of posets to force over (e.g. the one Cohen used for $\neg CH$) and see how the properties whose consistency they prove follow from the universal property of an appropriate classifying topos, and "compute" that these posets are the correct ones to use. I think this is almost done in Mac Lane and Moerdijk, but maybe they're not explicit about the universal properties? | |
| Aug 28, 2020 at 0:53 | comment | added | Mike Shulman | To wrap up this overly-long comment thread, then, let me emphasize that I didn't mean to deny that the traditional perspective on forcing has important insights and uses (despite my own ignorance of what those might be). My point was that I think the algebraic perspective is a better way to explain forcing to a newcomer (as the original question asked), and in particular solves the specific issue asked about by the OP. After one is no longer a newcomer, one should certainly learn other ways of thinking about it as well. | |
| Aug 27, 2020 at 23:38 | comment | added | David Roberts♦ | @AsafKaragila Touché. Will do. | |
| Aug 27, 2020 at 22:58 | comment | added | Asaf Karagila♦ | @DavidR: You can email me as well. Normally that's how it works, if you have a question, you send an email. :-) | |
| Aug 27, 2020 at 22:11 | comment | added | Asaf Karagila♦ | Mike, $\Bbb P$ is a proper forcing is for every large enough regular $\kappa$, if $M$ is a countable elementary submodel of $H(\kappa)$ and $\Bbb P\in M$, then every condition in $\Bbb P\cap M$ can be extended to a condition which is $M$-generic, in the sense that every dense open $D\in M$ satisfies that $D\cap M$ is predense below the extension. Equivalently, this means that if we do the Mostowski collapse, add a generic to the model, and undo the collapse, we get "what we'd expect". A forcing is improper if it is not proper. Now, every proper forcing preserves $\omega_1$, for example. | |
| Aug 27, 2020 at 22:05 | comment | added | David Roberts♦ | @Asaf I'd be be interested to learn more about this phenomenon, but not here. You have my email address... | |
| Aug 27, 2020 at 19:01 | comment | added | Mike Shulman | Well, I don't have the time to actually understand all that right now, and I can't even get the Internet to tell me what "improper forcing" is. But I'll register my skepticism that anything mathematical can actually fail to be invariant under isomorphism, for a correct definition of "isomorphism". (-: | |
| Aug 27, 2020 at 17:30 | comment | added | Asaf Karagila♦ | @Mike: And this is exactly the problem you'll find yourself in when you're trying to deal with improper forcing and "the usual finitary approach", where we take an countable elementary submodel of some $H(\kappa)$ and force over it. If the forcing is improper, then the generic extension is not going to commute with the transitive collapse. Which exactly tells you that something is not invariant under isomorphism (or that the Mostowski collapse is somehow the wrong isomorphism, or that the generic filter is somehow "wrong", I guess). | |
| Aug 27, 2020 at 15:50 | comment | added | Mike Shulman | Maybe we are seeing the same problem at a meta-level. We "algebraists" are used to the idea that isomorphic objects are indistinguishable. So since "algebraic forcing" is isomorphic to ordinary forcing, we don't understand why anyone would feel the need to distinguish between them. Ultimately, this idea of isomorphism-invariance is probably one that can only be learned through experience, so continuing to try to justify it verbally is unlikely to get anywhere. | |
| Aug 27, 2020 at 14:40 | comment | added | David Roberts♦ | @Asaf see my comment about tensors above. Two approaches to the same thing, in different fields of research, with vastly different notation, practice, aim etc. | |
| Aug 27, 2020 at 14:31 | comment | added | Asaf Karagila♦ | @David: But the question is what does it mean "to explain forcing", when you take the method, change its setting, change its setup, change its environment, and change its language? Theseus had less problems with maintaining his ship. | |
| Aug 27, 2020 at 14:30 | comment | added | David Roberts♦ | @Asaf the point at hand is not "how do you prove such-and-such a theorem", but how to explain forcing to someone that isn't already trained in its mysteries. Bringing up the practice of professionals in this space is a red herring. | |
| Aug 27, 2020 at 13:39 | comment | added | Asaf Karagila♦ | @DavidR: I'm not complaining that the answer was given. I agree, it's illuminating. But it also feels to me that it is written to people who understand sheaves and toposes much more than "generic mathematicians". Yes, it's probably a new, wider audience whose intersection with set theorists is small, and that's great. I'm not here to take this away from Mike, or anyone else. I'm just trying to point out that it's not exactly "generic mathematicians" either. | |
| Aug 27, 2020 at 13:35 | comment | added | Asaf Karagila♦ | @Mike: How do you prove preservation theorems for countable support iterations of proper forcings? How do you deal with the machinery of proper forcings to begin with? Yes, there is a template that lets you copy-paste standard arguments into algebraic ones, which means it is probably impossible to point at something "you can't do", but if you try to understand forcing with side conditions, suddenly well-founded models become an important tool. | |
| Aug 27, 2020 at 13:28 | comment | added | David Roberts♦ | @AsafKaragila "tell me that forcing should be seen through an algebraic lens" I'm not we are telling you that, the question asked for something that would make sense for people who aren't set theorists. This answer is really not meant for people who understand ZF(C) inside out and force six impossible things before breakfast, but for 'generic mathematicians', in the sense that Kevin Buzzard talks about. At best they know what a category is, and what sets are, but are specialists in neither. | |
| Aug 27, 2020 at 12:57 | comment | added | Mike Shulman | @AsafKaragila I'm still waiting to hear something concrete that you can do with nonalgebraic forcing that you can't do with algebraic forcing. If it's just an aesthetic preference, there's nothing a priori wrong with that, but I look at the other answers to this question and I see people struggling to use that perspective to give intuition for something that in the algebraic picture is much simpler and obvious, so it's hard for me to see what's "nicer" about it other than that you're used to it or haven't put the effort in to become familiar with the algebraic approach. | |
| Aug 27, 2020 at 10:36 | comment | added | Asaf Karagila♦ | @DavidC: I'm sorry, I'm being a bit defensive here, perhaps because I feel ganged up by people who try to tell me that forcing should be seen through an algebraic lens. I mean, why does the first thing we prove about forcing is that it preserves transitivity and does not add ordinals if it's not important? You know, I mean, who cares about transitive models? Well, apparently set theorists do. Why? Because they are very nice. That's why we call them "standard models". Why do algebraists care so much about the "universal property" everywhere? Because it's nice and they like it... | |
| Aug 27, 2020 at 10:33 | comment | added | David Corfield | @AsafKaragila Sure, any series of requests as to why someone wants something will only go so far, ending perhaps with "I just like it". I'm surprised here it's reached so soon. Even a vague "I have the sense that it may be useful for the next step the field should take" adds something more. And now while writing this I see you are adding such content. | |
| Aug 27, 2020 at 10:33 | comment | added | Asaf Karagila♦ | @DavidR: Also, why do you need the Dedekind-completeness property? You can just as well work with any field that has sufficiently structure if you look at analysis from an algebraic lens. You just want certain types to be realised, and you want to ensure that the types you get from "things that interest you" are included in these certain types. You can recast a lot of analysis in terms that would make sense in higher up models. So let's ditch these fields and move on to wilder models that lie to the west, and have a real wild west vibe in freshman Calculus I. | |
| Aug 27, 2020 at 10:25 | comment | added | Asaf Karagila♦ | @DavidR: Hilbert spaces, Banach spaces, fine, you get my point, find a good example. That's not the point. The point is that there is some "nice property" that we are interested in, because it interacts well with the universe, or with how we perceive that the universe "should" interact with our objects. Algebra is not about interactions with the universe, and that's fine, but not all mathematics is about viewing things through that lens. It's just not always that useful. | |
| Aug 27, 2020 at 10:21 | comment | added | David Roberts♦ | @AsafKaragila I think analysis is not a good example. There's only one Dedekind-complete ordered field, and that's what analysts work with. Note that you definitely don't always want an extension of your category such that the original one is full in it, since that is not true for the category of sets of a model M and the category of sets of M[G]. :-) | |
| Aug 27, 2020 at 10:03 | comment | added | Asaf Karagila♦ | @DavidCorfield: I can't see why this is a problem. Would you tell analysts to work in some hyperreal extension of size $(2^{\aleph_{\omega_1}})^+$? No. They work with the real numbers because they have nice properties. If you want to be concrete, transitive models are those that agree with the ambient universe on the membership relation and on the actual elements. I understand that in algebra none of this matter, but much to the dismay of some people, I suppose, not all of mathematics is algebra... | |
| Aug 27, 2020 at 10:00 | comment | added | David Corfield | @Asaf: I can't see how the word 'nice' by itself explains very much. Surely you must be able to finish off this sentence without using it, "And the reason we set theorists look to preserves the well-foundedness (and transitivity) of the ground model is..." | |
| Aug 27, 2020 at 8:25 | comment | added | Asaf Karagila♦ | @Mike: In other words, constructions that preserve "niceness" are not uncommon in mathematics. You want extensions of a category such that your original one is full in them, or you want compactifications of your space such that the space does not lose too many of its properties. There's a reason why the study of algebraic number theory is on finite algebraic extensions, and not in $\Bbb C$ as a field extension of $\Bbb Q$ (even though we sometimes go there, for clarity of thought), we want to have nice things. Set theorists want to have nice things as well. | |
| Aug 27, 2020 at 8:22 | comment | added | Asaf Karagila♦ | @Mike: This is very much reflected in the fact that forcing preserves transitivity and does not add ordinals. A striking contrast with other model theoretic methods (ultraproducts, saturated models, compactness methods) which tend to modify the original model completely. There's a reason we do forcing with transitive models, and there's a reason proper forcing is called proper: it is forcing where you can take "nice models of nice fragments of ZFC and the generic extension commutes with the Mostowski collapse", in some sense, that is the proper way to approach forcing. | |
| Aug 27, 2020 at 1:22 | comment | added | David Roberts♦ | @Asaf Maybe one should view it as the difference between knowing about tensor products, their universal property and multilinear algebra, and knowing about tensors as physicists do, all concrete symbol manipulation and efficient calculation. These two viewpoints are inherently different and achieve different viewpoints. Ideally one learns both! | |
| Aug 26, 2020 at 23:54 | comment | added | Mike Shulman | @AsafKaragila The usual/original motivation for forcing is, I believe, to prove that a certain statement is unprovable in ZFC, and for that purpose it doesn't matter what kind of model you end up with. I can believe that for other purposes the details might matter more, although I'd be surprised if there weren't also an algebraic version in that case. Can you explain why one might care that forcing preserves the well-foundedness and transitivity of the ground model? | |
| Aug 26, 2020 at 22:48 | comment | added | Asaf Karagila♦ | @DmitriPavlov: But ETCS(+R) is not a theory where one thinks about transitive models, this is in contrast to ZFC. Exactly like if you're a number theorist, $\Bbb Q(\pi)$ is just a field; but if you're doing combinatorial semigroup theory, it is an ordered subfield of $\Bbb R$ (as per Carl-Fredrik's comment below my answer). There is a point where abstraction is not necessarily more illuminating. | |
| Aug 26, 2020 at 22:27 | comment | added | Dmitri Pavlov | @AsafKaragila: I am not sure I understand your claims about well-foundedness. Mike's answer explicitly points out that the resulting model is well-founded when he says “well-founded extensional relations can be defined in ETCS+R, and the relations of this sort in any model of ETCS+R form a model of ZFC”. | |
| Aug 26, 2020 at 20:38 | comment | added | Asaf Karagila♦ | Mike, it seems to me that if you're trying to understand forcing like this, then you're not trying to understand forcing, but rather a similar technique in algebraic set theory, which could be perhaps described as "algebraic forcing". This is, at the end, not really Cohen's argument, to the point where forcing is important because it preserves the well-foundedness (and transitivity) of the ground model. This is exactly the point where we care that the model is not abstract, but concrete. | |
| Aug 26, 2020 at 20:04 | comment | added | Mike Shulman | @AsafKaragila The point is that if you instead put in the effort to get over the "universal hump" of learning category theory, you end up at a high enough place that you can see over all other humps without any extra effort. (-:O | |
| Aug 26, 2020 at 15:32 | comment | added | Asaf Karagila♦ | @JacquesCarette: Quite the opposite for me, to be honest. If Timothy was lamenting how non set theorists get confused and wonder why do you need all these complex machinery for forcing; Mike's answer (interesting and illuminating as it may be) makes me wonder why these things are even necessary, yes, there's a "learning hump" (as with everything else in mathematics), but once you get over it, forcing is pretty easy to understand. If you feel like Mike's answer is "easier" that just means that you don't want to put the effort getting over the hump from the set theory side (which is fine). | |
| Aug 26, 2020 at 12:25 | comment | added | Jacques Carette | This answer gives me a faint, but still better, hope of understanding forcing from a type-theoretic point of view than I've ever had before. Thanks. | |
| Aug 26, 2020 at 1:18 | history | answered | Mike Shulman | CC BY-SA 4.0 |