Return to Question

EDIT 2: As I discuss in this question, the Feferman-Schutte approach to extending the ramified hierarchy to transfinite levels seems to rely on some form of the omega rule, either the infinitary omega rule or the formalized omega rule. I don't know what the philosophical justification for invoking the omega rule is, but whatever it is, does it depend on the fact that Feferman and Schutte are analyzing "predicativity given the natural numbers", which takes the set of natural numbers as a completed totality, thereby justifying the omega rule somehow. If that's the case, then presumably we wouldn't be justified in using the oeega rule here, since the stricter notion of predicativity (as opposed to predicativity given thr natural numbers) that Parsons and Nelson espouse treats the natural numbers as only a potential infinity, leading to a skepticism of induction itself, let alone the omega rule.

EDIT 2: As I discuss in this question, the Feferman-Schutte approach to extending the ramified hierarchy to transfinite levels seems to rely on some form of the omega rule, either the infinitary omega rule or the formalized omega rule. I don't know what the philosophical justification for invoking the omega rule is, but whatever it is, does it depend on the fact that Feferman and Schutte are analyzing "predicativity given the natural numbers", which takes the set of natural numbers as a completed totality, thereby justifying the omega rule somehow. If that's the case, then presumably we wouldn't be justified in using the oeega rule here, since the stricter notion of predicativity (as opposed to predicativity given thr natural numbers) that Parsons and Nelson espouse treats the natural numbers as only a potential infinity, leading to a skepticism of induction itself, let alone the omega rule.

EDIT 2: As I discuss in this question, the Feferman-Schutte approach to extending the ramified hierarchy to transfinite levels seems to rely on some form of the omega rule, either the infinitary omega rule or the formalized omega rule. I don't know what the philosophical justification for invoking the omega rule is, but whatever it is, does it depend on the fact that Feferman and Schutte are analyzing "predicativity given the natural numbers", which takes the set of natural numbers as a completed totality, thereby justifying the omega rule somehow. If that's the case, then presumably we wouldn't be justified in using the oeega rule here, since the stricter notion of predicativity (as opposed to predicativity given thr natural numbers) that Parsons and Nelson espouse treats the natural numbers as only a potential infinity, leading to a skepticism of induction itself, let alone the omega rule.

So can anyone confirm that the omega rule is essential to how Feferman and Schutte extend the ramified hierarchy, and if so whether there's any other way to extend it in the context of h Burgess-Hazen analysis?

EDIT: @UlrikBuccholtz's answer points to a paper by Leivant which states that "predicative stratification in the polymorphic lambda calculus using levels $<\omega^\ell$ leads to definability of functions in Grzegorczyk's $\mathscr E_{\ell+4}$". I'm not that familiar with the lambda calculus, so can someone confirm that this implies that $EFA$ with predicative second-order logic with comprehension schemes for levels up to $<\omega^3$ proves that all the functions in Grzegorczyk's $\mathscr E_{7}$ are total? If that were true then the proof-theoretic ordinal of this system would be $\omega^7$, and then by similar methods, I think we can go to $\omega^{11}$, $\omega^{15}$, etc, all the way up to $\omega^\omega$, the proof-theoretic ordinal of $PRA$.