Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies to $n + 1$ whenever it applies to $n$, and you define an inductive number to be any number that has all the hereditary properties of $0$, then the definition of "inductive" involves quantification over all hereditary properties, including the property "inductive". If you're sufficiently Platonistic concerning sets of natural numbers, that won't concern you, because you can say for instance that $0$ obviously has ALL the properties of $0$, so in particular it has all the hereditary properties of $0$, so it's inductive. But predicativists like Weyl and Poincare would say that in order to verify that $0$ is inductive, we need to know what hereditary properties it has, and in order to know what hereditary properties it has, we need to verify that it has the hereditary property known as inductiveness!

In the context of second-order logic, impredicative comprehension refers to any instance of the second-order comprehension schema that involves bound set variables. If we take second-order arithmetic and allow only predicative comprehension, i.e. we only apply the comprehension schema to formulas with no bound set variables, then we get a subsystem of second-order $PA$ known as $ACA_0$, which is conservative over first-order $PA$. But disallowing bound set variables is not the only way to ensure predicativity. We can instead adopt the ramified theory of types, which breaks the comprehension schema into levels. The comprehension schema for level $0$ sets allows no bound set variables. The schema for level $1$ sets allows quantification over level $0$ sets. In general, the schema for level $n + 1$ sets allow for quantification over sets of level $n$ and below. This way, you can still quantify over sets, but you won't risk quantifying over the set you happen to be defining.

And there's no particular reason to stop at finite levels. We can define a comprehension schema for level $\omega$ sets, for instance, allowing quantifies to range over sets of finite level. And so on, going to bigger and bigger transfinite ordinals. Godel apparently showed that if you carried this process all the way up to $\omega_1$, the first uncountable ordinal, you wouldn't need to go any further. But this is somewhat problematic, since there are presumably countable ordinals whose existence aren't even provable by predicative means. In other words, for sufficiently great ordinals $\alpha$, it may not be predicatively provable that there exists a well-ordering of the natural numbers with order-type $\alpha$. Feferman and Schutte remedied this by only allowing a comprehension-schema for level $\alpha$ sets if the ordinal $\alpha$ is in fact predicatively acceptable (using the comprehension-schemata for lower-level sets). See pg 15-16 of this paper for a brief explanation. In any case, they reached the following conclusion: if $RA_\alpha$ denotes second-order arithmetic with a comprehension schemata for sets of level $\alpha$ and below, then $RA_\alpha$ is only predicatively acceptable if $\alpha$ is less than a certain ordinal known as $\Gamma_0$, the Feferman-Schutte ordinal.

My question is, assuming the Feferman-Schutte analysis of predicativity is accurate, can we give a precise criterion for what is and isn't provable in predicative second-order arithmetic. That is, given a sentence $S$ in the language of second-order arithmetic, under what conditions does there exist an $\alpha < \Gamma_0$ such that $S$ is provable in $RA_\alpha$? Of course, such a characterization of what truths are predicatively acceptable would not itself be predicatively acceptable. It's similar to how the truths provable in Edward Nelson's system of predicative first-order provable are precisely the bounded consequences of $Q$ + bounded induction + "exponentiation is total", even though Nelson himself would reject that characterization because he doesn't think exponentiation IS total.

It seems to me that just like $Q$ + bounded induction + "exponentiation is total" is an "upper bound" for Nelson's predicative first-order arithmetic, the system $ATR_0$, Arithmetical Transfinite Recursion, is an "upper bound" for the Feferman-Schutte conception of predicative-second order arithmetic. After all, the proof-theoretic ordinal of $ATR_0$ is $\Gamma_0$, the least impredicative ordinal, and it proves the consistency of $ACA_0$, a predicative subsystem of arithmetic. So can we characterize the set of predicatively acceptable theorems as some appropriate subset of the set of theorems of $ATR_0$, distinguished by some syntactic property, just like we could take the bounded consequences of $Q$ + bounded induction + "exponentiation is total"?

Any help would be greatly appreciated.

EDIT: As @AndreasBlass pointed out, on page 18 this paper, Feferman says that $ATR_0$ is "locally predicatively justifiable", meaning that a predicativist would reject the system as a whole as impredicative, but would accept each individual theorem of the system as predicatively acceptable, i.e. each theorem of $ATR_0$ is provable in $RA_\alpha$ for some $\alpha < \Gamma_0$ (where $\alpha$ can vary). So now the question becomes, is $ATR_0$ "maximally locally predicatively justifiable"? In other words, are there predicatively acceptable statements of second-order arithmetic not provable in $ATR_0$? And if so, is there some larger system that IS maximal? I assume any such system would still have proof-theoretic ordinal $\Gamma_0$. (Am I right about that?)

-

The Feferman-Schutte analysis is completely wrong. The problem is that "well-ordered" is not a single predicative concept because predicativists lack strong comprehension axioms. If you can't form the set $\{x \in X: \neg\phi(x)\}$ then you can't go from "every subset of $X$ has a smallest element" to "if $(\forall x < a)\phi(x) \to \phi(a)$ for any $a \in X$,then $(\forall x \in X)\phi(x)$".

This wrecks their whole argument because at each stage they use proof trees of height $\gamma_n$ to prove that $\gamma_{n+1}$ is well-ordered in the weak sense and then claim that this justifies acceptance of proof trees of height $\gamma_{n+1}$, which would require induction up to $\gamma_{n+1}$ for all sentences of second order arithmetic.

The argument is absurd in the other direction as well --- if the predicativist can grasp the jump from $\gamma_n$ to $\gamma_{n+1}$ for each $n$, why can't he grasp the general principle that for all $n$, induction up to $\gamma_n$ implies induction up to $\gamma_{n+1}$, and infer induction up to $\Gamma_0$? No cogent answer to this question was ever given. Believe me, I dug through the literature pretty hard.

I discuss this in more detail than you could possibly want in my paper Predicativity beyond $\Gamma_0$.

-
I have heard of your paper, and read various discussions of it on the FOM mailing list, for instance. Did you ever respond to Harvey Friedman's challenge? www.cs.nyu.edu/pipermail/fom/2006-April/010411.html. But in any case, my question is about how you would characterize predicativity assuming the Feferman-Schutte analysis is correct, not whether the analysis is correct. And besides, I'm not sure want "correct" really means, since predicativity is a vague enough thing that it's not clear how much of the disagreement is just attributable having different conceptions of predicativity. –  Keshav Srinivasan Sep 26 '13 at 12:48
First, Friedman's "challenge" is content-free and has nothing to do with my specific criticism of Feferman-Schutte. Second, the disagreement is not about having different conceptions of predicativity. You can't just arbitrarily decide that your predicativist has the ability to apply sigma-1 comprehension at one point in your analysis, but nowhere else, after it is pointed out to you that you've implicitly assumed this. (If you allow sigma-1 comprehension in general then you get far beyond $\Gamma_0$.) –  Nik Weaver Sep 26 '13 at 17:22

I quote from Simpson "Subsystems of second order arithmetic" 2nd edition:

Remark I.11.9 (first order part of ATR0 ). It is known that the first order part of ATR0 is the same as that of Feferman's system IR of predicative analysis; indeed, these two systems prove the same $\Pi^1_1$ sentences. Thus our development of mathematics within ATR0 (theorem I.11.5, remark I.11.6, chapter V) may be viewed as contributions to a program of "predicative reductionism," analogous to Hilbert's program of finitistic reductionism (remark I.10.6, section IX.3). [..]

-
How does that quote answer my question? I want to know how to characterize the second-order statements that are predicatively provable. By the way, how can he say that $ATR_0$ proves the same first-order truths as a predicative system? Doesn't it prove $Con(ACA_0)$ and thus $Con(PA)$? And isn't it not possible to predicatively prove any statement of first-order arithmetic not already provable in $PA$? –  Keshav Srinivasan Sep 26 '13 at 12:55
@KeshavSrinivasan It seems to me that a predicativist, who (as you assumed in the question) accepts all the ordinals below $\Gamma_0$ and thus in particular accepts $\varepsilon_0$, would also accept Gentzen's consistency proof for PA. In fact, I would expect predicativists to also accept the truth predicate for first-order sentences of arithmetic and thus to accept the "obvious" proof that PA is consistent because all its axioms are true. –  Andreas Blass Sep 26 '13 at 14:20
@AndreasBlass Then why does Feferman say "if a known mathematical result can be established predicatively, it can already be done in a system conservative over Peano Arithmetic (PA)" on page 19 of this paper: math.stanford.edu/~feferman/papers/predicativity.pdf –  Keshav Srinivasan Sep 26 '13 at 14:39
@KeshavSrinivasan The passage you quoted isn't the whole sentence; Feferman precedes it with "It turns out in practice that". I suspect he is making a distinction here between mathematical facts (the subject of this sentence) and metamathematical facts like Con(PA) (or the well-foundedness of $\varepsilon_0$ or the existence of a truth predicate for first-order arithmetic). The next sentence reformulates the claim in terms of "everyday mathematics", and the sentence after that says that there is no theorem that can establish this. –  Andreas Blass Sep 26 '13 at 14:49
At the bottom of page 18, Feferman says that $ATR_0$ is locally predicatively justifiable, which, according to the definition on page 16, would imply that each individual theorem is predicatively justifiable, but not necessarily that a predicativist would see the whole system as justified. –  Andreas Blass Sep 26 '13 at 15:00

All of the traditional "locally predicatively justifiable" theories are supposed to have equivalent $\Pi^1_1$ theorems; but they differ for statements of higher complexity. So they would not, even under the traditional reading, characterize all of second-order predicative arithmetic. Presumably, one would need a predicative version of the Axiom of Projective Determinacy to characterize the provable higher-complexity statements (and of course the analysis would depend on the classical version of this axiom).

But, in fact, something seems to have gone wrong somewhere, because $\mathcal{ATR}_0$ is finitely axiomizable (Feferman points this out on page 21); so it cannot be locally predicatively justifiable. For an explicit example, "For any $\alpha<\Gamma_0$, the Axiom of Reducibility is relatively consistent over $RA_\alpha$" is a $\Pi_2^0$ sentence provable in $\mathcal{ATR}_0$ but not in $RA_\alpha$ for any $\alpha < \Gamma_0$.

-