On the limit existence principles in elementary arithmetic and _n^0-consequences of theories

DOI10.1016/J.APAL.2005.05.005MaRDI QIDQ2566065zbMATH OpenOpenAlexFDO

Authors Albert Visser, Lev D. Beklemishev

Publication date 22 September 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.005

zbMATH Keywords

conservativityelementary arithmeticinference ruleinterpretability logicordinal analysisparameter-free inductionreflection principles

Mathematics Subject Classification ID

Recursive ordinals and ordinal notations (03F15) First-order arithmetic and fragments (03F30) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Review text

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)].

Recommendations

• Reflection principles and provability algebras in formal arithmetic
• On the quantifier complexity of \(\Delta_{n+1}(T)\)-induction
• On the optimality of conservation results for local reflection in arithmetic
• Reflection Principles in Fragments of Peano Arithmetic
• On some formalized conservation results in arithmetic

Cites work

• A simple proof of arithmetical completeness for \(\Pi_ 1\)-conservativity logic
• scientific article; zbMATH DE number 3668596 (Why is no real title available?)
• scientific article; zbMATH DE number 1215499 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• Iterated local reflection versus iterated consistency
• On parameter free induction schemas
• Parameter free induction and provably total computable functions
• Proof-theoretic analysis by iterated reflection
• Systems of Logic Based on Ordinals^†
• The interpretability logic of Peano arithmetic
• The logic of \(\Pi_ 1\)-conservativity
• The logic of \(\Pi_ 1\)-conservativity continued
• Transfinite recursive progressions of axiomatic theories

Cited in

(14)

• Lewis meets Brouwer: constructive strict implication
• Axiomatizing provable \(n\)-provability
• The arithmetics of a theory
• Pell Equations and Weak Regularity Principles
• Provability and interpretability logics with restricted realizations
• Weak forms of the Regularity Principle in the presence of \documentclass{article}\usepackage{amssymb}\begin{document}\pagestyle{empty}$\bf {\mathsf {I}{\mathrm{E}}_1}$\end{document}
• Provably \(\Delta ^0_2\) and weakly descending chains
• A mathematical commitment without computational strength
• The small-is-very-small principle
• AXIOMATIZATION OF PROVABLE n-PROVABILITY
• On the optimality of conservation results for local reflection in arithmetic
• On a Problem of J. Paris
• Marginalia on a theorem of Woodin
• Transductions in arithmetic

This page was built for publication: On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566065)