# What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

As I discuss in my answer here, it seems to me that Solomon Feferman shows, on pages 10-11 of his seminal 1964 paper "Systems of Predicative Analysis", that if you consider predicative second-order arithmetic with the ramified hierarchy going to arbitrarily high transfinite ordinals, then the sets you'll ultimately get are the hyperarithmetic sets. In contrast, in the standard Feferman-Schutte version of predicative second-order arithmetic, we only allow the ramified hierarchy to go up to an ordinal $\alpha$ if we are able to prove that $\alpha$ is well-founded using the comprehension schemata for lower levels of the ramified hierarchy. And proceeding in this way, Feferman and Schutte showed you could build the ramified hierarchy up to $\Gamma_0$, the Feferman-Schutte ordinal. And Gamma_0 is also the proof-theoretic ordinal of the resultant system of predicative second-order arithmetic.

Now obviously going up all the way up the ramified hierarchy would yield more sets than simply going up to $\Gamma_0$, so I expect second-order arithmetic with hyperarithmetical comprehension to be stronger than then the Feferman-Schutte version of predicative second-order arithmetic, and thus I expect that the former would have a higher proof-theoretic ordinal than $\Gamma_0$. So what is this ordinal?

One thing that gives me pause is that page 3 of this PDF (which I haven't read) says that "hyperarithmetic analysis", which I assume means second-order arithmetic with hyperarithmetical comprehension, is "mostly here in between" $ACA_0$ and $ATR_0$, which have proof-theoretic ordinals $\epsilon_0$ and $\Gamma_0$ respectively. How is this possible? Shouldn't hyperarithmetical comprehension have a higher proof-theoretic ordinal than $\Gamma_0$?

Any help would be greatly appreciated.

-
There's a nice survey in Feferman's chapter on predicativity for the Oxford Handbook of Logic and Philosophy of Mathematics. You can find it online here: math.stanford.edu/~feferman/papers/predicativity.pdf –  Benedict Eastaugh Dec 18 '13 at 2:13
A quick look makes me think the thing that's wrong is your contention that "if you consider predicative second-order arithmetic with the ramified hierarchy going to arbitrarily high transfinite ordinals, then the sets you'll ultimately get are the hyperarithmetic sets". Kleene proved that if you iterate the ramified hierarchy up to $\omega_1^{CK}$ you get the hyperarithmetic sets. But that doesn't exhaust the sets of natural numbers which one can get from the ramified hierarchy by iterating through more ordinals. –  Benedict Eastaugh Dec 18 '13 at 2:16
@BenedictEastaugh Thanks, I skimmed that paper at some point, but it may merit closer examination. Do you have any idea what sets you would ultimately get if you iterated through arbitrarily high ordinals? If so, can you respond to my question here? mathoverflow.net/questions/151172/… Also, can you tell me what's wrong with my answer to that question? Feferman proves that a variation of the ramified hierarchy collapses at $\omega_1^{CK}$, so why not the ramified hierarchy itself? –  Keshav Srinivasan Dec 18 '13 at 2:28

The difficulty is in what it means to go up the ramified hierarchy. When talking about theories, you can't write down a computable or c.e. theory which perfectly captures the whole ramified hierarchy.

The paper of Feferman's you mention constructs a sequence of systems $\mathcal{M}_\alpha$, with $\alpha$ ranging over the ordinals, so that as $\alpha$ ranges over all countable ordinals, you see the hyperarithmetic sets. But this is a sequence of systems indexed by ordinals, not a single system. (Further, the proof-theoretic ordinals go at least to $\omega_1^{CK}$ as you consider different $\mathcal{M}_\alpha$.)

If you want to try to capture hyperarithmetic comprehension in a single system, you need to write down an axiom. This can be phrased various ways, but one is to say something like "if $\alpha$ is an ordinal, the ramified hierarchy up to $\alpha$ exists". The problem is that now we're quantifying over $\alpha$ inside the system, which means there will be models which get wrong which $\alpha$ are actually ordinals.

Depending on how you make precise which $\alpha$ are ordinals, you could get systems which "undershoot"---systems which only capture the ramified hierarchy up to a certain level---or systems which "overshoot"---where standard models contain all the hyperarithmetic sets, but also some additional ones ($ATR_0$ is an example of the latter).

So while it's true that going all the way up the ramified hierarchy yields more sets than going to $\Gamma_0$, there isn't a canonical way to express the same idea proof-theoretically; different approaches give different answers, but none of them are exactly the same as climbing the ramified hierarchy.

Perhaps the remaining question is why even call these theories of hyperarithmetic analysis. A good reason is that if you take any informal argument using hyperarithmetic sets, you expect it to be formalized in such a system. After all, any well-orderings you used were presumably proved to be well-orderings. And any time you quantified over well-orderings, your argument should also work over non-well-orderings whose infinite descending sequences are too complicated to be constructed in your argument.

This is what we should expect of proof theory: an axiom of hyperarithmetic comprehension should capture the method of proof embodied in the use of the hyperarithmetic comprehension (which it does), and can't hope to capture the model/set theoretic notion of looking at the actual hyperarithmetic sets.

-
"When talking about theories, you can't write down a computable or c.e. theory which perfectly captures the whole ramified hierarchy." Yes, but I'm willing to discuss things in a nonrecursive fashion. We can have a nonrecursive system in which for each ordinal $\alpha$, there is a comprehension schema for level $\alpha$. –  Keshav Srinivasan Dec 18 '13 at 20:58
Capturing hyperarithmetic comprehension in a single recursive system seems trivial to me. You don't even need to use the ramified hierarchy. You just have to say that there exists a set corresponding to each hyperarithmetic formula. –  Keshav Srinivasan Dec 18 '13 at 21:01
Anyway, if you're right there's no approach that's the same as going all the way up the ramified hierarchy, how do you interpret Godel's result that going all the way up the ramified hierarchy corresponds to going up to $\omega_1$? Do you have any thoughts on my question here? mathoverflow.net/questions/151172/… Also see my answer to my question. –  Keshav Srinivasan Dec 18 '13 at 21:04
@KeshavSrinivasan: If you're talking about nonrecursive theories or systems which explicitly state the existence of each hyperarithmetic set, you're outside the realm of proof theory and proof theoretic ordinals. (I made the comment about proof-theoretic ordinals going to at least $\omega_1^{CK}$ because some of those theories are nonrecursive; one could simply say that they have no proof-theoretic ordinal, or try to define an analog, which would presumably by $\geq\omega_1^{CK}$.) –  Henry Towsner Dec 19 '13 at 16:44
Regarding your other comments: 1) What is a hyperarithmetic formula that can be quantified over in a recursive way? 2) Godel is talking about the ramified hierarchy being constructed in non-recursive settings where you iterate over all ordinals; the result has no proof-theoretic ordinal –  Henry Towsner Dec 19 '13 at 16:48

This is a second answer (think of it as part two of the other, already long, answer), in response to the clarification of the question by Keshav Srinivasan in the comments on that question.

First, note that there's no such thing as a $\Delta^1_1$ formula; there are pairs of formulas $\phi(X,x)$ and $\psi(Y,x)$ where $\forall X\phi(X,x)$ is $\Pi^1_1$, $\exists Y\psi(Y,x)$ is $\Sigma^1_1$, and $\forall X\phi(X,x)$ is provably equivalent to $\exists Y\psi(Y,x)$. This is important to understanding why you don't get the behavior you might expect: we have a computable list of things that might define $\Delta^1_1$ sets, but we don't have a computable way to tell which ones actually do.

The theory which states that every $\Delta^1_1$-definable set exists---that is, the axiom $$(\forall x[\forall X\phi(x,X)\leftrightarrow\exists Y\psi(x,Y))\rightarrow(\exists Z\forall x(\forall X\phi(x,X)\leftrightarrow x\in Z)$$ is called $\Delta_1^1-CA_0$ and has proof-theoretic ordinal $\Gamma_0$; it is actually slightly weaker than $ATR_0$. The reason you don't get more is because there are nonstandard models which get the $\Delta^1_1$ sets wrong---models in which $\forall X\phi$ fails to be equivalent to $\exists Y\psi$ even though in the standard model they would be equivalent, and therefore a set that "ought" to exist fails to.

-
OK thanks, I didn't realize that the question of whether two formulas define the same set varies from model to model in this way. Do you have a reference where I can read more about this? Also, when you say that this theory is weaker than $ATR_0$, do you mean that $ATR_0$ can prove the existence of all the sets that $\Delta_1^1 - CA$ can? That would be surprising to me, because it seems to me that some of those sets would never appear in the Feferman-Schutte autonomous progression. –  Keshav Srinivasan Dec 19 '13 at 20:26
The usual reference on theories of second order arithmetic is Simpson's book, "Subsystems of Second-Order Arithmetic". For the ordinal analysis side, some of Pohlers' writings---his book, "Proof Theory: The first step into impredicativity" and his article in the Handbook of Proof Theory. As for the relationship between $ATR_0$ and $\Delta^1_1-CA_0$, yes, $ATR_0$ proves the existence of all the sets $\Delta^1_1-CA_0$ can; you can find this as Theorem VIII.4.1 of Simpson's book. –  Henry Towsner Dec 19 '13 at 23:33