Skip to main content
added 5 characters in body
Source Link
Noah Schweber
  • 249k
  • 21
  • 355
  • 626

(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 $pt(T)=\omega_1^{CK}$$pto(T)=\omega_1^{CK}$.)

(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 $\Pi^1_1$-sound then $pt(T)=\omega_1^{CK}$.)

(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}$.)

deleted 5 characters in body
Source Link
Noah Schweber
  • 249k
  • 21
  • 355
  • 626

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] into $\alpha$.

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] into $\alpha$.

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$.

added 2831 characters in body
Source Link
Noah Schweber
  • 249k
  • 21
  • 355
  • 626
  • 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 focusonfocus 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 $\Pi^1_1$-sound then $pt(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.

  • 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 focuson 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.

  • 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 $\Pi^1_1$-sound then $pt(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.

Source Link
Noah Schweber
  • 249k
  • 21
  • 355
  • 626
Loading