Published online by Cambridge University Press: 11 August 2010
The concept of the (full) unfolding of a schematic system
is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted
? The program to determine
for various systems
of foundational significance was previously carried out for a system of nonfinitist arithmetic,
; it was shown that
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,
, and for an extension of that by a form
of the so-called Bar Rule. It is shown that
and
are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic,
, and to Peano Arithmetic,
.