Abstract:
In this paper the numerical strength of fragments of
arithmetical comprehension, choice and general uniform boundedness is studied
systematically. These principles are investigated relative to base systems
in all finite types which are suited to formalize
substantial parts of analysis but nevertheless have provably recursive
function(al)s of low growth. We reduce the use of instances of these
principles in -proofs of a large class of formulas to
the use of instances of certain arithmetical principles thereby determining
faithfully the arithmetical content of the former. This is achieved using the
method of elimination of Skolem functions for monotone formulas which was
introduced by the author in a previous paper.
As corollaries we obtain new conservation results for fragments of analysis over fragments of arithmetic which strengthen known purely first-order conservation results
Available as PostScript, PDF, DVI.