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.
Thank You in Advance.
EDIT: I emailed Albert Visser, and he referred me to his paper "The Predicative Frege Hierarchy", where he apparently shows that if you try to naively extend the ramified hierarchy to the transfinite using ordinal notations, and you don't add the formalized omega rule or any other principle, then the resulting system can't prove any more statements than a system with finite levels, because any given proof only involves finitely many ordinal levels, and thus we can just interpret them as finite levels.
So it looks like the formalized omega rule, or something to take its place, is essential to building the ramified hierarchy to transfinite levels in a non-trivial way. So what is the predicative justification of the formalized omega rule in the Feferman-Schutte context? Does that justification depend on a Platonic view of the set of natural numbers, and if so can we replace the formalized omega rule with something else that IS predicative justifiable if you don't accept the natural numbers as a completed totality? Perhaps an iteration of consistency statements or other reflection principle?
