Unfolding Finitist Arithmetic

Solomon Feferman & Thomas Strahm

The notion of unfolding a schematic formal system was introduced in Feferman [1] in order to answer the following question:

Given a schematic system S, which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted S?

A paradigmatic example of a schematic system S is the basic system NFA of non-finitist arithmetic. In Feferman and Strahm [2], three unfolding systems for NFA of increasing strength have been analyzed and characterized in more familiar proof-theoretic terms; in particular, it was shown that the full unfolding of NFA, U(NFA), is proof-theoretically equivalent to predicative analysis.

The aim of the present contribution is to elucidate the concept of unfolding in the context of the schematic system for finitist arithmetic FA in order to answer the crucial question of what principles are implicit in the actual finitist conception of the set of natural numbers. The main results state that the operational unfolding U_{0}(FA) and even the full (predicate) unfolding U(FA) of finitist arithmetic FA conservatively extend Skolem’s system of primitive recursive arithmetic PRA. These results support Tait’s informal analysis of finitism in [3] according to which finitist mathematics does not go beyond PRA.

[1] Feferman, S. Gödel’s program for new axioms: Why, where, how and what? In Gödel ’96, P. Hájek, Ed., vol. 6 of Lecture Notes in Logic. Springer, Berlin, 1996, pp. 3–22.

[2] Feferman, S., and Strahm, T. The unfolding of non-finitist arithmetic. Annals of Pure and Applied Logic. To appear.

[3] Tait, W. Finitism. Journal of Philosphy 78 (1981), 524–546.

Addresses Solomon Feferman: Department of Mathematics, Stanford University, Stanford, CA 94305 USA

E-mail: sf@csli.stanford.edu

Thomas Strahm: Institut für Informatik und angewandte Mathematik, University of Bern, Neubrückstr. 10, CH-3012 Bern, Switzerland

E-mail: strahm@iam.unibe.ch