Can the Burgess-Hazen analysis of Predicative Arithmetic be extended to Transfinite Types?

Question

Around page 300 of his book "Mathematical Thought and its Objects", Charles Parsons discusses the work of Edward Nelson, who believes that mathematical induction is impredicative, because it can be applied to formulas with quantifiers ranging over natural numbers, even though we conceive of natural numbers as objects belonging to all inductive formulas, including the formula we happen to be applying induction to. Nelson argues that if we reconstruct arithmetic along predicative lines, then we can only accept weak forms of induction that are interpretable in Robinson's Q, like induction on formulas with bounded quantifiers, and on this basis he accepts the totality of addition and multiplication, but not exponentiation.

Parsons agrees with Nelson that there's something impredicative about induction, but he believes that the totality of exponentiation is still predicative. This is based on a paper by Burgess and Hazen, "Predicative Logic and Formal Arithmetic": projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdf_1&handle=euclid.ndjfl/1039293018

This paper is concerned with predicative second-order logic, which is like regular second-order logic, except we have a ramified theory of types, which breaks the comprehension schema into levels. The comprehension schema for level 0 sets only allows formulas that have no quantification over sets. The schema for level 1 sets allows quantification only over level 0 sets. For any natural number n, the schema for level n+1 allows quantification over sets of level n and below. Burgess and Hansen prove that predicative second-order logic plus the axiom of infinity implies Robinson's Q + induction on formulas with bounded quantifiers + the totality of exponentiation. This is the basis on which Parsons concludes that exponentiation is total from a predicative point of view.

But as Parson points out, there's no particular reason to stop at finite levels. We can define a comprehension schema for level ω sets, for instance, allowing quantifies to range over sets of finite level. And so on, going to bigger and bigger transfinite ordinals. This is analogous to the Feferman-Schutte analysis of predicative second-order arithmetic (except that Feferman and Schutte rely on a different notion of predicativity, known as "predicativity given the natural numbers", which accepts the natural numbers as a completed totality, in contrast to Nelson and Paraons who think of it only as a potential infinity). We allow a comprehension schema for level $\alpha$ sets as long as $\alpha$ is a transfinite ordinal that is "predicatively acceptable" in a well-defined sense using lower-level comprehension schemes. For starters, we can have comprehension for levels up to $\omega^3$, since as discussed above we can establish the totality of exponentiation using finite levels, and exponentiatial function arithmetic has proof-theoretic ordinal $\omega^3$. This process would presumably converge on some ordinal, akin to the Feferman-Schutte ordinal. And it would presumably allow us to establish a larger subsystem of first-order arithmetic than if we just stuck to finite levels as Burgess and Hazen did.

Parsons, who wrote his book in 2008, said that it was still an open problem as to what exactly that larger subsystem was, although he guesses that it won't be bigger than PRA. Has any progress been made on this since 2008, or was Paraons even mistaken about it being unsolved? Has it at least been shown that, say, the totality of superexponentiation is provable in this larger subsystem?

Any help would be greatly appreciated.

Thank You in Advance.

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$.

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?

Answer 1

I'm not aware of anyone doing the setup exactly as you describe, although it is very likely that it has been done, because it is very similar to Kreisel's proposed method of analyzing finitism in Ordinal logics and the characterization of informal concepts of proof (of course, by many accounts he overestimated the reach of finitism and predicativity given the natural numbers).

However, I would suggest you take a look at Feferman and Strahm (2010), Unfolding of finitist arithmetic, where it is shown that the unfolding (in the sense of Feferman's unfolding program) of finitism is proof-theoretically equivalent to PRA (Primitive Recursive Arithmetic) and hence has proof-theoretic ordinal $\omega^\omega$.

The unfolding is relevant here because it gives a kind of predicative closure given certain base principles. For instance, Feferman and Strahm (2000), The unfolding of non-finitist arithmetic, show that the unfolding of a basic system NFA (of Non-Finitist Arithmetic) is proof-theoretically equivalent to predicative analysis and has proof-theoretic ordinal $\Gamma_0$.

Update: You may also be interested in the work of Leivant, in particular his paper with Danner, Stratified polymorphism and primitive recursion, where it is shown that predicative stratification in the polymorphic lambda calculus using levels $<\omega^\ell$ leads to definability of functions in Grzegorczyk's $\mathscr E_{\ell+4}$. But they don't study an autonomous system.