Unfolding finitist arithmetic

Abstract

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