What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

Question

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.

Thank You in Advance.

Answer 1

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.

Answer 2

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.