On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories (Q2566065)

This highly technical paper, written by the two top superstars of the field, consists of two independent parts. In the first part (Sections~1--4) the axiom schema (Lim) asserting that any eventually descending elementary function has a limit and its corresponding rule (LimR) are studied. The schema appears in Solovay's completeness theorem (for Solovay functions). In Section~2 it is shown, among other results, that Lim axiomatizes I\(\Sigma_1^-\), the parameter-free \(\Sigma_1\)-induction over Elementary Arithmetic EA. In Section~3 it is shown that the closure of EA under LimR is contained in I\(\Pi_1^-\), the parameter-free \(\Pi_1\)-induction, and also any instance of I\(\Pi_1^-\) is provable by one application of LimR over EA; and the rest of the section is devoted to the proof of the interesting fact that EA+LimR axiomatizes the \(\Sigma_2\)-consequences of I\(\Sigma_1\). In Section~4 the theorem of Berarducci-Shavrukov-Hájek-Montagna, that ILM is the \(\Pi_1\)-conservativity logic of theories extending I\(\Sigma_1\), is improved to theories extending I\(\Pi_1^-\); the proof assumes familiarity with the notation of [\textit{G. Japaridze} and \textit{D. de Jongh}, ``The logic of provability'', in: S. R. Buss (ed.), Handbook of proof theory. Amsterdam: Elsevier. Stud. Logic Found. Math. 137, 475--546 (1998; Zbl 0915.03019)], especially its Theorem 14.2. Next, the authors, by adapting a theorem of D. Zambella and G. Mints, show that the bound I\(\Pi_1\) cannot be much improved: the logic of \(\Pi_1\)-conservativity of PRA extends ILM properly. In the second part (Section~5) an ordinal classification of \(\Sigma_n\)-consequences of standard fragments of PA, based on iterated reflection principles of a special kind, is given. The proofs are largely based on the ideas of [\textit{L. D. Beklemishev}, ``Proof-theoretic analysis by iterated reflection'', Arch. Math. Logic 42, No. 6, 515--552 (2003; Zbl 1026.03041)].