Timeline for Explaining the consistency of PRA and ZF from predicative foundations
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 20 at 5:13 | answer | added | Ingo Blechschmidt | timeline score: 3 | |
| Feb 19, 2019 at 20:36 | comment | added | Ingo Blechschmidt | @Timothy: I thought so too, but hoped for an answer in the other direction demonstrating that my intuition is off. Maybe I should stress that my question only referred to consistency, not soundness. A priori, the position that PRA is in itself consistent while still proving lots of falsehoods might be a coherent position. | |
| Feb 19, 2019 at 20:21 | vote | accept | Ingo Blechschmidt | ||
| Feb 18, 2019 at 19:13 | comment | added | Timothy Chow | Regarding the consistency of PRA, I very much doubt that anyone who does not already find its consistency obvious will find any argument (formal or informal) for its consistency convincing. | |
| Feb 18, 2019 at 4:09 | answer | added | Nik Weaver | timeline score: 10 | |
| Feb 18, 2019 at 1:10 | comment | added | David Roberts♦ | @Ingo ok, thanks. Also, I just noticed the typo in my first comment. It should read "...a primitive recursive decreasing sequence of ordinals stabilises" | |
| Feb 18, 2019 at 1:07 | comment | added | user44143 | A devotee of predicative math may look down on some supposed evidence for the consistency of impredicativity — once you know how to take ordinary applied math and make it predicative, the fact that people have applied it without contradiction on an impredicative basis may be less impressive. | |
| Feb 18, 2019 at 0:31 | comment | added | Ingo Blechschmidt | @Not_Here: Ah, okay. I agree, and would appreciate any insight even if it only pertains to the consistency of PRA from the point of view of predicative arithmetic or to the consistency of (I)ZF from the point of view of predicative set theory. | |
| Feb 18, 2019 at 0:26 | comment | added | Not_Here | @IngoBlechschmidt Right, my apologizes I don't think my comment was clear. My point was that I think that there should be a clear distinction between people like Nelson on the one hand and people like Feferman on the other. Asking why we should believe PRA is consistent and asking why we should believe ZF is consistent are two completely different questions, even if the motivation for both beliefs can be called 'predicativism'. | |
| Feb 18, 2019 at 0:21 | comment | added | Ingo Blechschmidt | @Not_Here: I agree that the Feferman cogently explains why one could worry about impredicative set theory, in particular, why one might worry about the powerset axiom and why one hence might doubt the consistency of ZF, seeing that it includes a worrisome axiom. But I'm looking for predicative arguments which shed light on (which explain to some degree) the apparent consistency of ZF instead of giving reasons to doubt it. | |
| Feb 18, 2019 at 0:14 | comment | added | Not_Here | Pretty much all of Feferman's work will apply to this. For example, he was very critical of "an arbitrary subset of the natural numbers" having any coherent meaning, because that is an extraordinarily impredicative definition. That probably qualifies under your "informal, philosophical" arguments. People like Nelson are coming at the problem from a much different angle than Feferman and Weyl, for example, so their arguments will be very different. So to that extent, I think there needs to be a clear distinction between people who are skeptical of PRA and those critical of ZF. | |
| Feb 18, 2019 at 0:11 | comment | added | Ingo Blechschmidt | @David: (cont'd) (However, Gentzen's result doesn't seem to be directly relevant to my question. Predicative arithmetic doubts that primitive recursions terminate, hence doubts Gentzen's result, and predicative set theory has no problems verifying the consistency of PA, since in CZF and IZF we do have the completed set of naturals.) Regarding your second comment: Yes. The existence of such a simulation would satisfactorily explain the consistency of impredicative set theory from a predicative point of view. However, in the absence of such a simulation, there might still be other explanations. | |
| Feb 18, 2019 at 0:07 | comment | added | Ingo Blechschmidt | @David: Yes, Timothy's paper is an excellent survey of the question of the consistency of PA! And Gentzen's proof provides a rich understanding of the consistency of PA for someone who adopts $\text{PRA}+\text{QF-TI}(\varepsilon_0)$ as their metatheory: Firstly, it provides a proof of consistency; secondly, while they still might doubt the truth of theorems of PA, Gentzen's proof still provides them with some meaning to theorems of PA, namely winning strategies in Gentzen's game of reductions. | |
| Feb 18, 2019 at 0:05 | comment | added | David Roberts♦ | To pick apart your question, I guess if one works in a predicative framework where one can take the power class of a set, and this isn't a set, then you are worried there's no way to 'simulate' the impredicative behaviour of the power set? | |
| Feb 17, 2019 at 23:58 | comment | added | David Roberts♦ | You may know of this already, but for others: Timothy Chow, in The Consistency of Arithmetic, gives a variant on Gentzen's proof of the consistency of PA (Theorem 2). One doesn't have to rely on "PA ... [is] consistent because [its] axioms are true, when interpreted to refer to the actual numbers ..." Instead, one has to believe a primitive recursive sequence decreasing sequence of ordinals stabilises. | |
| Feb 17, 2019 at 23:37 | history | asked | Ingo Blechschmidt | CC BY-SA 4.0 |