Timeline for Explaining the consistency of PRA and ZF from predicative foundations
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 19, 2019 at 22:48 | comment | added | Nik Weaver | @IngoBlechschmidt: I replied to your comment within my post. | |
| Feb 19, 2019 at 22:48 | history | edited | Nik Weaver | CC BY-SA 4.0 |
added 728 characters in body
|
| Feb 19, 2019 at 21:17 | comment | added | Timothy Chow | @IngoBlechschmidt : While it's true that formal proofs may not give you any joy if you're seeking explanations of the consistency of (say) large cardinal axioms, one frequently used technique for justifying large cardinal axioms is reflection. One can of course debate whether a reflection argument counts as a convincing "explanation," but it does at least illustrate the possibility of an informal justification of a consistency (or even a soundness) claim. But of course appealing to reflection is anathema to a predicativist. | |
| Feb 19, 2019 at 20:43 | comment | added | Ingo Blechschmidt | Thank you for the insightful answer and the pointers to your papers, Nik. I wasn't aware of them. It seems then that the (apparent) consistency of impredicative systems is an unexplainable mystery from a predicative point of view. Upon further reflection I recognize that maybe this fact shouldn't be too unsettling: After all, formal systems have the tendency to not decide the consistency of formal systems, including that (of course) a system such as ZFC doesn't prove the consistency of ZFC. | |
| Feb 19, 2019 at 20:21 | vote | accept | Ingo Blechschmidt | ||
| Feb 18, 2019 at 13:28 | comment | added | Asaf Karagila♦ | Yes, to clarify my previous comment, it was intended to be read with a tongue heavily buried in one's cheek. | |
| Feb 18, 2019 at 13:27 | comment | added | Nik Weaver | @AsafKaragila: I assume you're joking, but in any case if ZF is consistent then in principle there exists a predicative proof of this fact. One just checks, case by case, that no $n$ is the Godel number of a proof of $0=1$. The proof has length $\omega$, but predicativists (of the type we're discussing) would be fine with that. | |
| Feb 18, 2019 at 12:23 | comment | added | David Roberts♦ | @Asaf that's some impressive classical logic you got there... | |
| Feb 18, 2019 at 8:10 | comment | added | Asaf Karagila♦ | It would be epic if we can prove that any inconsistency proof of ZF must be impredicative. Then predicativists will have to deny it, so they would in fact claim that ZF is consistent. | |
| Feb 18, 2019 at 4:09 | history | answered | Nik Weaver | CC BY-SA 4.0 |