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?


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.

  • $\begingroup$ 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". $\endgroup$ – Keshav Srinivasan Dec 1 '13 at 22:55
  • $\begingroup$ Also, you're talking about finitism, which is what people like Kreisel and Tait talk about. But Edward Nelson and Parsons are talking about a more extreme version which Nelson calls "strict finitism" and which critics call "ultrafinitism" (although the term ultrafinitism more properly refers to someone like Essenin-Volpin who believes that there are only finitely many natural numbers). Unlike finitists, strict finitists don't accept mathematical induction, because they view it as impredicative. Are the papers you're discussing about finitism or strict finitism? $\endgroup$ – Keshav Srinivasan Dec 1 '13 at 23:16
  • 1
    $\begingroup$ 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). $\endgroup$ – Ulrik Buchholtz Dec 2 '13 at 3:56
  • 1
    $\begingroup$ 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. $\endgroup$ – Ulrik Buchholtz Dec 2 '13 at 4:02
  • $\begingroup$ What do you mean by "basic finitism"? And yes, there are different kind's of finitism. Tait's notion of finitism amounts to PRA, Kreisel's amounts to PRA plus quantifier-free transfinite induction up to $\epsilon_0$. But the "strict finitism" of Nelson and Parsons is much more extreme than either of those. Yes, including even a single existential quantifier would be prohibited in strict finitism, because it assumes that there's an existing totality of natural numbers that we can quantify over, as opposed to a mere potential infinity. That's why there's a skepticism of induction. $\endgroup$ – Keshav Srinivasan Dec 2 '13 at 17:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.