Are finitist systems the ones with a proof-theoretic ordinal of at most $\omega^\omega$?

81 Views Asked by At

The proof-theoretic ordinal of $\mathsf{EFA}$ and $\mathsf{RCA}_0^*$ are $\omega^3$ and the one of $\mathsf{PRA}$, $\mathsf{I\Sigma1}$, $\mathsf{RCA}_0$, etc. is $\omega^\omega$.

See https://ncatlab.org/nlab/show/ordinal+analysis.

In general, is there a connection between the fact that a system is considered finitist and its proof-theoretic ordinal? If so, is the bound $\leq\omega^\omega$ or $<\epsilon_0$? Would the bound for ultrafinitism be $<\omega$?