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

From MaRDI portal
Set OpenAlex properties.
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Iterated local reflection versus iterated consistency / rank
 
Normal rank
Property / cites work
 
Property / cites work: Parameter free induction and provably total computable functions / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof-theoretic analysis by iterated reflection / rank
 
Normal rank
Property / cites work
 
Property / cites work: The interpretability logic of Peano arithmetic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4215636 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Transfinite recursive progressions of axiomatic theories / rank
 
Normal rank
Property / cites work
 
Property / cites work: The logic of \(\Pi_ 1\)-conservativity / rank
 
Normal rank
Property / cites work
 
Property / cites work: The logic of \(\Pi_ 1\)-conservativity continued / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5286672 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A simple proof of arithmetical completeness for \(\Pi_ 1\)-conservativity logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: On parameter free induction schemas / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3866106 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Systems of Logic Based on Ordinals<sup>†</sup> / rank
 
Normal rank

Latest revision as of 16:34, 10 June 2024

scientific article
Language Label Description Also known as
English
On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories
scientific article

    Statements

    On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories (English)
    0 references
    0 references
    0 references
    22 September 2005
    0 references
    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)].
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    elementary arithmetic
    0 references
    parameter-free induction
    0 references
    inference rule
    0 references
    interpretability logic
    0 references
    conservativity
    0 references
    reflection principles
    0 references
    ordinal analysis
    0 references
    0 references