I have found the following quote ( source ):

The proof-theoretic ordinal of any theory is less than $\omega_1^{CK}$.

But if all these proof-theoretic ordinals are recursive and below $\omega_1^{CK}$, then can we assume that for any set theory $T$ (including KP, ZFC, MK), there exists some particular finite natural number that corresponds to the “strength” of $T$? Basically, this number is equal to the minimal natural number $n$ such that there exists an $n$-state Turing machine that computes any ordinal $\alpha$ such that the proof-theoretical ordinal of $T$ is embedded into $\alpha$.

If this assumption is correct, then I would want to see mathematical (formal) explanation of how such numeric measure should be defined and what requirements such "PTO-computing" Turing machines should satisfy.


Yes, this is easy to do, and you've done it already.

Incidentally, I really think you should look at the first section of Sacks' book, which goes into detail about computable ordinals and which I think will clear up a lot of these issues.

Your guess is already one perfectly formal definition:

The minimal natural number $n$ such that there exists an $n$-state Turing machine that computes any ordinal $\alpha$ such that the proof-theoretical ordinal of $T$ is [smaller than] $\alpha$.

(Once we fix a precise meaning of "proof-theoretic ordinal," of course.) So I don't know what additional formality you want.

I've replaced "is embedded into" with "smaller than" since the former suggests that the embedding itself should be computable, which I'm not sure you want; I think the language I've used is less suggestive.

The key point is that the phrase "computes an ordinal" is perfectly precise: we mean that the Turing machine $\Phi$ in question computes the characteristic function of a binary relation $R$ on $\mathbb{N}$ such that $(\mathbb{N}; R)$ is a well-ordering. There are no additional assumptions on the Turing machine which need to be made in order for this to make sense (although of course not every Turing machine does compute an ordinal, and the set of indices of Turing machines computing ordinals is highly complicated$^1$).

That said, there are many variations you could consider:

  • You could replace "smaller than" with "actually equal to." That this is different in general shouldn't be surprising: think about how (in the context of $\mathbb{N}$) the Kolmogorove complexity of $a$ can be bigger than that of $b$, even if $a<b$.

  • You could focus on indices as opposed to states: that is, "... such that the $n$th computable well-ordering is ..."

  • You could ask for an embedding of the proof-theoretic ordinal into $\alpha$ to be "effective" in some sense. E.g. you could fix a computable copy $S$ of the proof-theoretic ordinal $\theta$ of $T$ (that is, $S$ is a computable binary relation on $\mathbb{N}$ such that $(\mathbb{N}; S)$ is isomorphic to the proof-theoretic ordinal of $T$), and then look for a pair of Turing machines, one of which computes a copy of some ordinal $\ge\theta$ and the other of which computes an embedding of $S$ into that copy.

  • And so forth.

However, all of these approaches merely "rename" the proof-theoretic ordinal; although natural numbers are simpler than ordinals, they're not any simpler (in this context) than computable ordinals, so it's not clear that this shift gains anything.

EDIT: This part is in response to Andres' comments below.

It's worth noting that the claim "the proof-theoretic ordinal of $T$ measures the strength of $T$" has problematic aspects.

(For simplicity, let's define the proof-theoretic ordinal of $T$, $pto(T)$, as the least ordinal having no "$T$-provable" computable copy; that is, the least ordinal $\alpha$ such that there is no $e$ such that $(i)$ the $e$th Turing machine computes a copy of $\alpha$ and $(ii)$ $T$ proves that the $e$th Turing machine computes a well-ordering. As long as $T$ is $\Pi^1_1$-sound, overspill implies that $pto(T)<\omega_1^{CK}$; conversely, it's not hard to show that if $T$ is not $\Pi^1_1$-sound then $pto(T)=\omega_1^{CK}$.)

The issue is:

What information does $pto(T)$ actually give us?

Remember that the proof-theoretic ordinal lives in a broader proof-theoretic context; "measuring the strength of $T$" is generally taken to mean much more than just having some "concrete" description of $pto(T)$ (whatever that means; note that we can trivially cook up a computable copy of $pto(T)$ - namely, $$\sum_{\mbox{$T\vdash$ "$\Phi_e$ is a well-ordering"}}\Phi_e$$ - so "concrete" here is a very loaded word!). For example, we want:

  • A good understanding of the computable functions which $T$ proves are total (e.g. for RCA$_0$ these are exactly the primitive recursive functions).

  • A natural system of notations leading up to $pto(T)$ (this is arguably folded into the word "concrete" above), together with a connection between these notations and proofs from $T$ (this is the new bit).

  • Some fixed notation for $pto(T)$ together with a proof from a very weak theory that the well-foundedness of the ordering corresponding to this notation implies the consistency of $T$ (this is closely related to the previous bulletpoint, and really should fall out of it directly).

  • And probably a bunch of other things proof theorists know about but I don't.

All of this goes beyond just finding a "concrete description" for $pto(T)$. (For example, how would we figure out anything about what computable functions PA proves are total just by being told out of thin air that $pto(PA)=\epsilon_0$?) So we have to be careful: especially when talking about strong theories (like ZF), we don't want to assume out of hand that $pto(T)$ is necessarily measuring as much as we want it to.

That said, I would say that $pto(T)$ measures the strength of $T$ (at least to some extent), and in this I might disagree with Andres below. But it is important (as he pointed out) to make this issue clear; $pto(T)$ isn't some magic box which tells us everything about the strength of $T$, and divorcing it from these ambient assumptions may make it (and by extension, questions like this) less mysterious.

$^1$I've linked to Kleene's $\mathcal{O}$ here; this isn't literally the set of indices of Turing machines computing ordinals, but it is in fact "equivalent" to that set (precisely: the two sets are Turing equivalent, indeed $1$-equivalent). The general theory of Kleene's $\mathcal{O}$, and of computable ordinals in general, is developed in the first part of Sacks' book.

| cite | improve this answer | |
  • $\begingroup$ 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) $\endgroup$ – Andrés E. Caicedo Sep 27 '18 at 15:59
  • $\begingroup$ @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?" $\endgroup$ – Noah Schweber Sep 27 '18 at 16:07
  • $\begingroup$ 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. $\endgroup$ – Andrés E. Caicedo Sep 27 '18 at 16:22
  • $\begingroup$ @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. $\endgroup$ – Noah Schweber Sep 27 '18 at 16:25
  • 1
    $\begingroup$ @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). $\endgroup$ – Noah Schweber Sep 27 '18 at 16:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.