UNFOLDING FINITIST ARITHMETIC
Solomon Feferman, Thomas Strahm · The Review of Symbolic Logic · 2010
The concept of the (full) unfolding $\user1{{\cal U}}(S)$ of a schematic system $S$ is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted $S$ ? The program to determine $\user1{{\cal U}}(S)$ for various systems $S$ of foundational significance was previously carried out for a system of nonfinitist arithmetic, $NFA$ ; it was shown that $\user1{{\cal U}}(NFA)$ is proof-theoretically equivalent to predicative analysis. In the present paper we work out the unfolding notions for a basic schematic system of finitist arithmetic, $FA$ , and for an extension of that by a form $BR$ of the so-called Bar Rule. It is shown that $\user1{{\cal U}}(FA)$ and $\user1{{\cal U}}(FA + BR)$ are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic, $PRA$ , and to Peano Arithmetic, $PA$ .