Two unfoldings of finitist arithmetic

Thomas Strahm


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 non-finitist arithmetic, NFA; it was shown that U(NFA) is proof-theoretically equivalent to predicative analysis. After a general introduction and explanation of previous results, the main emphasis of this talk is to discuss 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.

(joint work with S. Feferman, Stanford University)

An extended abstract with references can be found here:

Tuesday 13th April 2010, 14:00
Board Room
Department of Computer Science