Skip to main content
2 of 3
Spelling

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.