Skip to main content
15 events
when toggle format what by license comment
Sep 28, 2018 at 5:36 vote accept lyrically wicked
Sep 28, 2018 at 0:19 comment added Noah Schweber @AndrésE.Caicedo Fixed, thanks!
Sep 28, 2018 at 0:19 history edited Noah Schweber CC BY-SA 4.0
added 5 characters in body
Sep 27, 2018 at 19:46 comment added Andrés E. Caicedo Thank you, Noah. Excellent as usual. (And sorry for all the bother.)
Sep 27, 2018 at 19:38 history edited Noah Schweber CC BY-SA 4.0
deleted 5 characters in body
Sep 27, 2018 at 19:09 comment added Noah Schweber @AndrésE.Caicedo I've edited to say a bit about this. Let me know what you think; I can of course edit it further to more adequately address the points you've raised.
Sep 27, 2018 at 19:08 history edited Noah Schweber CC BY-SA 4.0
added 2831 characters in body
Sep 27, 2018 at 16:51 comment added Noah Schweber @AndrésE.Caicedo But I do think that the proof-theoretic ordinal measures the strength of the theory, even in the absence of that ambient framework - it just doesn't do so very well. But you're right, my answer should say something about that; I'll edit it once I have time (I'm in a meeting right now).
Sep 27, 2018 at 16:34 comment added Andrés E. Caicedo Noah, I am just quoting from the question. I agree it is intrinsically interesting to search for such an ordinal. But the question explicitly mentions that it measures the strength of the theory, and seems to imply that this is because of general facts about proof-theoretic ordinals. I am saying that it is unwarranted (or problematic) to use this language, and I am saying that ideally an answer to the question should not ignore this issue.
Sep 27, 2018 at 16:26 comment added Noah Schweber (Which is why I don't think this is a fruitful thing to do).
Sep 27, 2018 at 16:25 comment added Noah Schweber @AndrésE.Caicedo I don't agree with that. I think "the least ordinal $\alpha$ such that there is no $e$ such that $T$ proves $\Phi_e$ is well-ordered and $\Phi_e$ has order type $\alpha$" is inherently interesting, regardless of what ambient theory we can develop around it; so asking about it doesn't presuppose such a theory (or even that $\alpha$ measures the strength of $T$ in any useful way). As to whether the natural number produced as per above measures the strength of the theory in question, I'd say that it does so exactly insofar as the proof-theoretic ordinal itself does.
Sep 27, 2018 at 16:22 comment added Andrés E. Caicedo I guess the thing is that we can assign many numbers to a reasonable theory (the least number of states of a Turing machine that is total but the theory does not prove it, say), but it is far from clear that we can say that they correspond to the "strength" of the theory in any meaningful sense unless we actually know that there is a reasonable notion of "proof-theoretic ordinal" for the theory. So, yes, there is a question we can straightforwardly address (as you point out), but that seems to ignore a serious, significant, unwarranted claim in the phrasing of the question.
Sep 27, 2018 at 16:07 comment added Noah Schweber @AndrésE.Caicedo Sure, there are things we want the proof-theoretic ordinal (which I define as you've stated) to do which for e.g. ZF we don't know how yet. But (i) it definitely makes sense to use that definition, regardless of whether it currently has the nice properties we want it to, and (ii) that's not relevant to the issue of the OP as far as I can tell since there's nothing better about attaching a specific number to it. I think that you've really addressed instead the question, "What does a 'calculation of the proof-theoretic ordinal of ZFC' need to do in order to be satisfying?"
Sep 27, 2018 at 15:59 comment added Andrés E. Caicedo Yes, but I guess the underlying issue is whether it makes sense to talk of the proof-theoretic ordinal of ZF. One can of course define it as the least $\alpha$ such that ZF cannot prove that a recursive ordering of $\omega$ of type $\alpha$ is a well-ordering. But really I think that to use the expression requires more (for instance, we would like a reasonable system of ordinal notations with supremum $\alpha$, a way to relate proofs in ZF to ordinals below $\alpha$, a way to define a fast growing hierarchy so that a provably total recursive function is majorized by one in the hierarchy, etc)
Sep 27, 2018 at 15:51 history answered Noah Schweber CC BY-SA 4.0