Timeline for How dangerous are set-size assumptions?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 21, 2019 at 20:04 | comment | added | Timothy Chow | @user36212 : Let M be the Turing machine that, on empty input, searches for a contradiction in ZFC. It could be the case that M does not halt, yet ZFC proves $\neg$Con(ZFC) and hence that M halts. This would not by itself show that ZFC is inconsistent. | |
| Jun 21, 2019 at 7:40 | comment | added | Asaf Karagila♦ | @Pace: I'm not here to trash Nik or his knowledge of set theory, and I think he's well versed in what he's saying. But I think that people are the product of their views. I find it almost disparaging to call ZFC "hodgepodge", and double-down by saying that the iterative concept is "utterly unconvincing". I found it very convincing. I don't find statements like "true" and "false" convincing, though, I mean, who made you the king of everything that you can know what is true and what is false. So what? | |
| Jun 21, 2019 at 7:26 | comment | added | user21820 | @MonroeEskew: You're just wrong, because PA+Con(ZFC) certainly proves Con(ZFC). In any case, that is irrelevant since I never said anything about proving Con(ZFC). The proof of my claim is quite trivial: (Work within ATR.) If ZFC proves ( ZFC is inconsistent ), then either ZFC is inconsistent and thus unsound, or ZFC is consistent and thus unsound because it proves a false Σ1-sentence. Even just ACA can easily prove ( If ZFC proves ( ZFC is inconsistent ), then ZFC is Σ1-unsound ) where "Σ1-unsound" is encoded. So it is wrong for Nik to say weaker theories could not prove unsoundness of ZFC. | |
| Jun 21, 2019 at 7:01 | comment | added | Peter LeFanu Lumsdaine | @Asaf: absolutely, I didn’t mean to direct that admonition just at ZFC-ists — I think most of us who care about foundations are guilty of it to a grease or lesser extent :-) | |
| Jun 21, 2019 at 3:24 | comment | added | Asaf Karagila♦ | @Peter: And who's to say thar Nik doesn't have Stockholm Syndrome towards predicative mathematics? | |
| Jun 20, 2019 at 16:30 | comment | added | Peter LeFanu Lumsdaine | @AsafKaragila: Your point is fair, but in the converse direction, it’s easy to get Stockholm syndrome: Once you’re deeply familiar with the consequences of some definition, they shape your intuition, and so the definition feels natural because it matches this intuition so well. So even when some definition is terribly ad hoc, its adherents will find it natural. Most arguments about foundations come down in large part to these two effects: people overlook kludges in the systems they’re most familiar with, and are disproportionately conscious of them in other systems. | |
| Jun 20, 2019 at 15:35 | comment | added | Pace Nielsen | @AsafKaragila I don't think your criticism is apropo. Nik has done lots of serious work with set theory, including writing a treatise on forcing for the regular mathematician, using diamond principle to solve problems in algebra, etc... | |
| Jun 20, 2019 at 15:15 | comment | added | Asaf Karagila♦ | It is easy to sit on a high chair and make claims that this or that theory is unmotivated. We all do that from time to time. That's just how being a human being works. But I can tell you that once you start working with ZFC and do set theory, rather than using set theory to construct the real numbers "and more or less that's it", the motivation become much clearer. The same can be said about chasing large cardinal axioms, weak choice principles, or reverse mathematics, or any other theory. If you're far away, the technical details will seem fuzzy, and confusing. | |
| Jun 20, 2019 at 14:08 | comment | added | Nik Weaver | @user36212: fair point, of course I meant "any weaker system which is known to be sound". | |
| Jun 20, 2019 at 13:46 | comment | added | user36212 | On the Turing Machines front, if a TM halts (on a given input) then Peano proves it, the proof being simply to write out the computation up to halting; the same goes for does not halt before time t. So I guess the only possibility left is that you are worried ZFC+Universes might prove that a given 'really' non-halting TM halts but the proof does not give any bound on the halting time? But this still implies ZFC+Universes is inconsistent, though this time the argument is not intuitionistic (unsurprisingly)..! | |
| Jun 20, 2019 at 13:24 | comment | added | user21820 | Your claim "as long as ZFC is consistent, no weaker system could prove that it is unsound" seems to be blatantly false. If someone does manage to construct a proof within ZFC of ( ZFC is inconsistent ), then we definitely can conclude that ZFC is unsound, even from the perspective of a very weak meta-system, because we can verify that ( ZFC proves ¬Con(ZFC) ) purely mechanically. In fact, we do not even need that much. It suffices if anyone constructs a ZFC proof of ( ZFC is Σ[n]-unsound ) for any fixed n. | |
| Jun 20, 2019 at 11:58 | history | edited | Nik Weaver | CC BY-SA 4.0 |
added 1 character in body
|
| Jun 20, 2019 at 11:40 | history | edited | Nik Weaver | CC BY-SA 4.0 |
added 365 characters in body
|
| Jun 20, 2019 at 10:48 | comment | added | Nik Weaver | @AndrejBauer: I do, but in that setting there are circularity issues that haven't been appreciated; see Sections 10 and 11 of this paper of mine. | |
| Jun 20, 2019 at 6:58 | comment | added | Andrej Bauer | Do the inductive constructions in type theory strike you as less of a hodgepodge? | |
| Jun 20, 2019 at 6:19 | comment | added | Monroe Eskew | As you stated, we’d never be able to come across a reason that it’s unsound. So the only way we’d get “no reason” to believe in soundness is if we are radical and dismiss the intuition of the vast majority of mathematicians as having no import. I know that’s your whole schtick but I want to point out that it’s radical. | |
| Jun 20, 2019 at 6:11 | comment | added | Monroe Eskew | “Hodgepodge”?? The instances we take are every class intersected with every set! This isn’t NF! | |
| Jun 20, 2019 at 1:20 | comment | added | Nik Weaver | You're very welcome. Thank you for the interest! | |
| Jun 20, 2019 at 0:30 | comment | added | Pace Nielsen | +1 Thanks for the background! | |
| Jun 19, 2019 at 22:44 | history | answered | Nik Weaver | CC BY-SA 4.0 |