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

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.

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?

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.

• Are you aware that Feferman, Schutte, and Weyl are concerned with a different notion of predicativity than the one that Nelson and Parsons are dealing with? Feferman et al. are talking about "predicative given the natural numbers", i.e. we treat the set of natural numbers as a completed totality, but then we proceed predicatively after that. Nelson and Parsons are treating the natural numbers as a potential infinity, so they're just concerned with "predicativity", not "predicativity given the natural numbers". – Keshav Srinivasan Dec 1 '13 at 22:55
• First, yes I'm aware that the Feferman-Schütte analysis of predicative concerns predicativity given the natural numbers. The unfolding of NFA is one way to approach that, and Feferman proposed that it should also be able to capture other notions of predicative closure, for instance of basic finitism (and in my dissertation, I study the unfolding of ID$_1$ which can model the predicative closure of one positive arithmetical inductive definition). – Ulrik Buchholtz Dec 2 '13 at 3:56
• I'm also aware that there are various approaches to finitism; e.g., under Kreisel's analysis it comes out to be equivalent with PA! But the system FA of Feferman-Strahm is fairly conservative: the logic is restricted to positive existential quantification over N. Maybe you would prefer a quantifier free presentation. In any case, with your proposal you run into the well-known problem with analyses of (any kind of) finitism that you want to go beyond the finite levels (!). Using unfolding avoids that quandary. – Ulrik Buchholtz Dec 2 '13 at 4:02
• @KeshavSrinivasan: It seems to me that skepticism in induction based on the view that the naturals are not a complete totality is actually ill-founded. That skepticism instead implies that we should not simply accept LEM for unbounded quantification. There are then two possible underlying logics that we may switch to, namely intuitionistic logic or 3-valued logic. In both cases, we can still justify having the rule ( ( A ⊢ B ; B ⊢ A ) ⊢ A∨¬A ) for any Σ1-sentence A and Π1-sentence B, and importantly we can justify the induction rule ( Q(0) ; ( k∈N ⊢ ( Q(k) ⊢ Q(k+1) ) ) ⊢ ∀k∈N ( Q(k) ) ). – user21820 May 20 '19 at 4:48
• In particular, there is no philosophical issue with induction, but rather related principles that depend on LEM for unbounded quantification, such as the well-ordering principle. @UlrikBuchholtz: I'm interested to hear your opinion on my view as well. – user21820 May 20 '19 at 4:50