The unfolding of non-finitist arithmetic Original Research Article

The unfolding of schematic formal systems is a novel concept which was initiated in Feferman (in: Hájek (Ed.), Gödel ’96, Lecture Notes in Logic, Springer, Berlin, 1996, pp. 3–22). This paper is mainly concerned with the proof-theoretic analysis of various unfolding systems for non-finitist arithmetic View the MathML source. In particular, we examine two restricted unfoldings View the MathML source and View the MathML source, as well as a full unfolding, View the MathML source. The principal results then state: (i) View the MathML source is equivalent to View the MathML source; (ii) View the MathML source is equivalent to View the MathML source; (iii) View the MathML source is equivalent to View the MathML source. Thus View the MathML source is proof-theoretically equivalent to predicative analysis.