Timeline for Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 5, 2023 at 10:12 | comment | added | C7X | "an ordinal such that the well-foundedness of any representation implies Con(ZFC)" - according to answer #333522, there is no such ordinal. For any notation system $\alpha$, it is possible to construct a notation system $\alpha^*$ such that $\alpha$ and $\alpha^*$ are notations for the same ordinal, and $\mathsf{RCA}_0+\mathsf{WF}(\alpha^*)$ fails to prove even $\mathsf{Con(RCA}_0)$, not only $\mathsf{Con(ZFC)}$. | |
| May 28, 2022 at 17:25 | comment | added | Binary198 | Recently Arai gave an ordinal analysis of Kripke-Platek set theory, a subtheory of ZF, with $\Pi_1$-collection. It is estimated to be a little stronger than the aforementioned $\Pi^1_2$-comprehension. | |
| Apr 23, 2014 at 23:19 | comment | added | Henry Towsner | @ScottAaronson: That looks exactly right. Giving a constructive proof of that is basically exactly what those proof-theorists are trying to do. | |
| Apr 23, 2014 at 23:01 | comment | added | Henry Towsner | @JoelDavidHamkins: The background theory is $\Pi^1_1$-soundness of ZFC. I believe that may be necessary (at least, there's a slight variant of the ordinal which is computable iff the theory is $\Pi^1_1$-sound). | |
| Apr 23, 2014 at 22:44 | comment | added | Scott Aaronson | Henry: Just to check my understanding, the proof that there exists a computable ordinal $\alpha$ that ZF doesn't prove to be well-founded is completely nonconstructive? I.e., starting from the ZF axioms, we can't write down a Turing machine (even a weird, incomprehensible one) that computes the order relation of that $\alpha$? Also, is it correct that we currently have no proof, not even a nonconstructive one, that there exists a computable ordinal $\alpha$ such that the well-foundedness of $\alpha$ (under any encoding scheme, not just a contrived one) implies Con(ZF)? | |
| Apr 23, 2014 at 21:48 | comment | added | Joel David Hamkins | (For example, in a model of ZFC+Con(ZFC)+ notCon(Con(ZFC)), there are programs that ZFC proves to halt, that don't really halt in that model, and one can use them to build denotations of ordinals in that model that ZFC proves are well-ordered, even though they aren't well-ordered in that model.) So what is the right background theory for the $\Sigma^1_1$-boundedness argument? | |
| Apr 23, 2014 at 21:48 | comment | added | Joel David Hamkins | @HenryTowsner The claim that the ZFC provably well-founded computable notations for ordinals form a $\Sigma^1_1$ set seems to assume that ZFC proves only true instances of well-foundedness, doesn't it? This claim implies Con(ZFC), but it seems to be strictly stronger. | |
| Apr 23, 2014 at 21:46 | comment | added | Timothy Chow | In particular, the claim that (for example) all arithmetical (or even $\Pi_1$) consequences of ZF can be deduced from some axiom in the first-order language of arithmetic with the same general form as Gentzen's axiom, just with $\epsilon_0$ replaced by "the proof-theoretic ordinal of ZF," is at present still, as Ron Maimon admits, an "article of faith." | |
| Apr 23, 2014 at 21:27 | comment | added | Scott Aaronson | Thanks so much; that's exactly the context I was looking for! | |
| Apr 23, 2014 at 21:26 | vote | accept | Scott Aaronson | ||
| Apr 23, 2014 at 21:21 | history | answered | Henry Towsner | CC BY-SA 3.0 |