UNFOLDING FINITIST ARITHMETIC

The concept of the (full) unfolding 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 U(S) for various systems S of foundational significance was previously carried out for a system of nonfinitist arithmetic, NFA; it was shown that 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 U(FA) and U(FA + BR) are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic, PRA, and to Peano Arithmetic, PA.