Things that can and things that cannot be done in PRA (Q1971796)

This article examines the strength of parameter free schematic forms of statements from analysis over two second order extensions of primitive recursive arithmetic (PRA). The strength of the statements is expressed via conservation results and characterizations of the provably recursive functions of the theories. The second order extensions used include PRA\(^2\) and the weaker PRA\(^2_-\) which omits an iteration functional. PRA\(^2\) is a fragment of \( \widehat {\text{PA}} ^\omega \restriction\) from \textit{S.~Feferman}'s article ``Theories of finite type related to mathematical practice'' [in: Jon Barwise, Handbook of mathematical logic (Studies in Logic and the Foundations of Mathematics, Vol. 90. Amsterdam - New York - Oxford: North-Holland Publishing Company), 913-971 (1977; Zbl 0443.03001)], and can be extended to PRA\(^2\)+AC\(^{0,0}\)-qf, a function variable version of the system \(\text{RCA}_0\) from reverse mathematics. The analytic principles covered include schematic versions of a principle on convergence of bounded monotone sequences (PCM\(^-\)), the Bolzano-Weierstraß principle (BW\(^-\)), the Ascoli-Arzela principle (A-A\(^-\)), and a principle asserting the existence of limit superiors (Limsup\(^-\)). Relative to PRA\(^2\)+AC\(^{0,0}\)-qf, none of these principles are conservative over PRA. Indeed, the Ackermann function is provably recursive in PRA\(^2\)+PCM\(^-\). By contrast, PCM\(^-\), BW\(^-\), and A-A\(^-\) are conservative over PRA relative to PRA\(^2_-\), while \(\text{Limsup}^-\) is not. The provably recursive functions of PRA\(^2_-\)+AC\(^{0,0}\)-qf+WKL+PCM\(^-\)+BW\(^-\)+A-A\(^-\) are exactly the primitive recursive ones. This work extends previous work of the author [for example, \textit{U.~Kohlenbach}, Arch. Math. Logic 36, 31-71 (1996; Zbl 0882.03050)].