# What is the role of the (formalized) omega rule in Ramified Analysis?

In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a method of disallowing a formula $\phi$ from being substituted into the comprehension schema if it has quantification over all sets, including the set being defined by $\phi$ itself. This is done by dividing the comprehension schema into levels, as follows. The comprehension schema for level $0$ sets does not allow any formulas with second-order quantifiers. The comprehension schema for level $1$ sets allows formulas with quantification over level $0$ sets. For any natural number $n$, the schema for level $n+1$ sets allows quantification over sets of level $n$ and below.

And there's no particular reason to stop at finite levels. The schema for level omega sets, for instance, allows quantification over sets of any finite level. And so on, for higher and higher transfinite ordinals. There's a question of which ordinals to use, and Feferman and Schutte answered it as follows: we only allow an ordinal $\alpha$ if it is predicatively acceptable, i.e. we can prove its existence using the comprehension schemata for lower levels. Proceeding in this way, they argued that if you started from $ACA_0$, which is second-order artihmetic with only comprehension for level 0 sets, you would get all the levels up to $\Gamma_0$, the Feferman-Schutte ordinal.

There's one part of the Feferman-Schutte analysis, however, that I don't understand the point of: the use of the omega rule in the systems of ramified second-order logic. I haven't studied Feferman's 1964 paper "Systems of Predicative Analysis" in detail, so some of this may be wrong, but here's what I've gleamed: he presents two systems of ramified second-order arithmetic. One system is an infinitary system, in which the ordinals that index the levels of the ramified hierarchy are defined set-theoretically, and there is an infinitary omega rule: from $\phi(0)$, $\phi(1)$, $\phi(2)$, ..., conclude $\forall x \phi(x)$. The other system is a finitary system, where we use Kleene's $O$ to encode the ordinals using natural numbers. This time, there is a "formalized omega rule", which is defined as follows: let $\sharp \phi$ denote the Godel number of $\phi$, and let $PROV(x)$ denote the probability predicate that encodes the proposition that the statement with Godel number $x$ is provable (in the system we're considering). Then the formalized omega rule states that $\forall x PROV(\sharp\phi(x))$ implies $\forall x \phi(x)$. In other words, if $\phi(n)$ is provable for all $n$, then conclude $\forall x \phi(x)$.

My question is, why is either version of the omega rule needed for systems of ramified analysis? What would happen if you proceeded without it? Would we not be able to prove any new truths of arithmetic? And what is the philosophical justification for using it? Is it because in the context of the Feferman-Schutte analysis, we're talking about "predicativity given the natural numbers", so we're willing to accept natural numbers on a Platonic basis, rendering the omega rule being acceptable somehow?

If that's the explanation, what would we do if we were doing ramified second-order arithmetic in other contexts, for instance starting with a weaker base theory as I discuss in this question? In that context, we're talking about "predicativity", full stop, not "predicativity given the natural numbers", so we're even questioning the validity of induction, let alone the omega rule. Would we not be able to extend the ramified hierarchy to transfinite hierarchy in that case, or is the omega rule inessential?

Any help would be greatly appreciated.

Model-theoretically, the $\omega$-rule is equivalent to restricting attention to models whose first-order part consists of the standard integers. In particular, the rule allows proving all true $\Pi^1_1$ statements. If the rest of the theory is recursively axiomatizable, the presence of the rule makes it considerably stronger, even for statements at the lowest possible level of the arithmetical hierarchy ($\Pi^0_1$). I am not really familiar with the ramified theory of types, and I have no idea why Feferman and Schutte chose to do it this way. –  Emil Jeřábek Dec 21 '13 at 22:03