11 ms·
Great article. Since it looks like a lot of folks are interested in this article, some extra background. First, what is forcing? The article actually has a gre
by pavpanchekha 5y ago
Great article. Since it looks like a lot of folks are interested in this article, some extra background.
First, what is forcing? The article actually has a great description of ultrapowers (a key part of the construction) but it goes by a little fast, so you might like Tim Chow's "A beginner's guide to forcing" [1] which does a good job not only laying out the mathematical details at a high level, but also really clearly explaining the philosophy of how you prove something independent of the axioms. I found it very illuminating.
Second, the article has some interesting notes on how mathematicians go about what axioms to select and which not to. Penelope Maddy's "Believing the Axioms" [2] is the classic on this topic (it has two parts). It is focused on set theory, so it has a nice description of Martin's axiom and the arguments for and against. It was nice to read because it is a deeply technical argument (set theory is hard!) but at the same time there is no "right answer"—all of these axioms, after all, are independent of ZFC, and it's "ok" to add any of them. The arguments are sometimes aesthetic ("rules" versus "surprises"), sometimes pragmatic (what they can and cannot prove), and sometimes involve deep values of what the universe should be like (should higher cardinalities be like lower ones? weirder? simpler?).
It might all seem abstract, but if your day job is programming, imagine an argument over how to architect a large and complex system. Perhaps both architectures are possible, but which one is "right"? What arguments would you deploy? Set theorists are also building a large and complex system (the universe of sets) and are having arguments over how it should be built, which things it should make easy and which hard, which technologies should be supported natively (forcing?) and which should not.
[1] http://timothychow.net/forcing.pdf http://timothychow.net/forcing.pdf
[2] https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf
- BoiledCabbage 5y agoWhy does forcing work? To me it seems flawed (which obviously means I don't understand it fully). For diagonalization argument: 1) Assume every real can be assigned a natural number. 2) Do a bunch of steps that essentially find a new real that differs from any real you have listed from step 1. 3) Conclude that either your steps are flawed, or your initial assumption is wrong 4). Because your steps aren't flawed then your initial assumption (that every real can map to a natural number) is flawed. That all makes sense to me. Forcing seems broken though: 1) Capture of list/set of all real numbers 2) Do a bunch of steps that essentially find a new real that differs from any real you have listed from step 1. 3) Conclude that either your steps are flawed, or your initial assumption is wrong 4). Because your steps aren't flawed then your initial assumption (that you can produce a list of every real number) is flawed. Now you're left in an odd situation. Didn't you just conclude that it's impossible to have a set of all real numbers? Which isn't what you're trying to prove at all.
- jerf 5y ago"Didn't you just conclude that it's impossible to have a set of all real numbers?" Cantor's diagonalization proof proves that it's impossible to list all the real numbers with a list of size aleph-0, which is the cardinality of the set of natural numbers. The forcing proof is an attempt to prove you also can't do it with the a list of the size aleph-1, which is the size of the power set of aleph-0. It purports to prove that you need a list of size aleph-2, which is the size of the powerset of aleph-1. You can kind of think of this not so much as whether "Can Crysis run?" ("can you have a set of all real numbers?") but "Can Crysis run on this machine?" Do the real numbers need aleph-1 "resources", or aleph-2 "resources" to list?
- glial 5y agoI think this is a typo: > aleph-0, which is the cardinality of the set of real numbers. aleph-0 is the cardinality of the set of natural numbers, and (as you say) is not the cardinality of the real numbers.
- jerf 5y agoYes, thank you, that was a typo.
- BoiledCabbage 5y agoThanks for the reply. Question though. in Cantor's argument we explicitly mapped the reals to aleph-0 so it makes sense that our conclusion decides that mapping to aleph-0 is too small so it's size must be larger. Where in the forcing process do we even "use" aleph-1? If we used aleph-1 then it could see the parallels and the argument would make sense - but all I see in the forcing process is "start with a set of all reals". Nothing about trying to map them to aleph-1. Maybe it's implicit, but couldn't I have just changed step 1 to instead be "start with a list of size aleph-90, then use forcing to prove that the reals are larger than aleph-90." In Cantor's argument it feels like we "used" the natural numbers. Here it seems more like we said take an arbitrary number of them and see this one isn't in it. But that arbitrary number of them (aleph-1) could've been any arbitrary number of them because we never really used any property of the set being aleph-1 vs aleph-90.
- rssoconnor 5y ago> but at the same time there is no "right answer"—all of these axioms, after all, are independent of ZFC, and it's "ok" to add any of them. Minor quible: Just because a potential axiom is independent of ZF(C) doesn't make it necessarily "okay" to add. Potential axioms can be unsound, for example if they prove new / untrue Sigma_1 statements. As an example, even in the likely circumstance that ¬Con(ZFC) is independent of ZFC, it wouldn't be "okay" to add ¬Con(ZFC). While the resulting system would be consistent, and does have models, the resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). That said, Martin's axiom, like the CH (or the axiom of choice), does not have any arithmetic consequences, and thus doesn't fall into this category of problematic axioms.
- tgflynn 5y ago> he resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). Isn't that basically the definition of the natural numbers, ie. if you write down any natural number (say n) I can always construct a natural number that is larger than it (like n+1) ?
- chongli 5y agoIf you can write down the natural number n, you can write down n+1. Of course, you can't write down the entire set of natural numbers but that is not a natural number.
- skybrian 5y agoOn any storage system you will eventually run out of memory, so there will always be a maximum integer that you can write down with what you have, and we can only write down a vanishingly small subset of the natural numbers. Of course, this isn’t what mean when they talk about “writing down” a number, but I’ve long thought that assuming the existence of natural numbers that you can’t write down is poetically apt. In some sense, the set of natural numbers is “too big” to be about everyday finite numbers alone and it seems fitting to acknowledge that our usual axioms can’t exclude weirdo large finite numbers that are simply too big to ever reach.
- intuitionist 5y agoMaddy’s work is great and worth reading (even as an antirealist!), but it’s worth keeping in mind that debates about foundations are basically irrelevant to the working lives of the large majority of mathematicians. If you’re studying, say, extremal graph theory or the Langlands program or low-dimensional topology, the cardinality of the continuum is simply not relevant.
- pavpanchekha 5y agoYes, I actually have a kind-of related blog post: https://pavpanchekha.com/blog/proof-system-os.html https://pavpanchekha.com/blog/proof-system-os.html I tried to restrict my post to just set theory because this philosophical point is often hard for people to grasp.
- scrubs 5y ago@pavpanchekha: thank you indeed for this great post and great references. I took ML and ran into CH, Ultrafilters but never really got my head around it. Reading with interest!
- 01GOD 5y agoHmmm…somebody named “chow” faking something…why is that not surprising?
- pdonis 5y agoThanks for these references! The Chow paper is the first one I've read that makes me feel like I understand forcing and Cohen's proof.
- ProfHewitt 5y agoNote that forcing and the independence results are only for 1st-order logic. They do not work for theories that characterize mathematical abstractions such as the Ordinals and Natural Numbers up to a unique isomorphism. See the following video: https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI