TY - JOUR

T1 - On the limit existence principles in elementary arithmetic and ∑n0-consequences of theories

AU - Beklemishev, Lev D.

AU - Visser, Albert

N1 - Funding Information:
We would like to thank J. Joosten for useful comments and proof reading and G. Mints for a kind permission to include one of his results. Special thanks go to an anonymous referee whose remarks eventually led us to a proof of Theorem 7.Infact, the referee proved that a version of the limit rule with arbitrary Σ2 side formulas provides an axiomatization of Σ2-consequences of I Σ1, and we were later able to improve this result to the original rule without side formulas by dealing with the notion of special Σ2-formula. The first author was supported in part by the Russian Foundation for Basic Research.

PY - 2005/10

Y1 - 2005/10

N2 - We study the arithmetical schema asserting that every eventually decreasing elementary recursive function has a limit. Some other related principles are also formulated. We establish their relationship with restricted parameter-free induction schemata. We also prove that the same principle, formulated as an inference rule, provides an axiomatization of the ∑2-consequences of I ∑1. Using these results we show that ILM is the logic of Π1 -conservativity of any reasonable extension of parameter-free Π1-induction schema. This result, however, cannot be much improved: by adapting a theorem of D. Zambella and G. Mints we show that the logic of Π1-conservativity of primitive recursive arithmetic properly extends ILM. In the third part of the paper we give an ordinal classification of ∑n0-consequences of the standard fragments of Peano arithmetic in terms of reflection principles. This is interesting in view of the general program of ordinal analysis of theories, which in the most standard cases classifies Π-classes of sentences (usually Π11 or Π20).

AB - We study the arithmetical schema asserting that every eventually decreasing elementary recursive function has a limit. Some other related principles are also formulated. We establish their relationship with restricted parameter-free induction schemata. We also prove that the same principle, formulated as an inference rule, provides an axiomatization of the ∑2-consequences of I ∑1. Using these results we show that ILM is the logic of Π1 -conservativity of any reasonable extension of parameter-free Π1-induction schema. This result, however, cannot be much improved: by adapting a theorem of D. Zambella and G. Mints we show that the logic of Π1-conservativity of primitive recursive arithmetic properly extends ILM. In the third part of the paper we give an ordinal classification of ∑n0-consequences of the standard fragments of Peano arithmetic in terms of reflection principles. This is interesting in view of the general program of ordinal analysis of theories, which in the most standard cases classifies Π-classes of sentences (usually Π11 or Π20).

KW - Conservativity

KW - Elementary arithmetic

KW - Inference rule

KW - Interpretability logic

KW - Ordinal analysis

KW - Parameter-free induction

KW - Reflection principles

UR - http://www.scopus.com/inward/record.url?scp=23944459322&partnerID=8YFLogxK

U2 - 10.1016/j.apal.2005.05.005

DO - 10.1016/j.apal.2005.05.005

M3 - Article

AN - SCOPUS:23944459322

SN - 0168-0072

VL - 136

SP - 56

EP - 74

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 1-2

ER -