Induction rules, reflection principles, and provably recursive functions

Annals of Pure and Applied Logic 85 (3):193-242 (1997)
  Copy   BIBTEX


A well-known result states that, over basic Kalmar elementary arithmetic EA, the induction schema for ∑n formulas is equivalent to the uniform reflection principle for ∑n + 1 formulas . We show that fragments of arithmetic axiomatized by various forms of induction rules admit a precise axiomatization in terms of reflection principles as well. Thus, the closure of EA under the induction rule for ∑n formulas is equivalent to ω times iterated ∑n reflection principle. Moreover, for k < ω, k times iterated ∑n reflection principle over EA precisely corresponds to the extension of EA by k nested applications of ∑n induction rule.The above relationship holds in greater generality than just stated. In fact, we give general formulas characterizing in terms of iterated reflection principles the extension of any given theory by k nested applications of ∑n or Πn induction rules. In particular, the closure of a theory T under just one application of ∑1 induction rule is equivalent to T together with ∑1 reflection principle for each finite Π2 axiomatized subtheory of T.These results have closely parallel ones in the theory of subrecursive function classes. The rules under study correspond, in a canonical way, to natural closure operators on the classes of provably recursive functions. Thus, ∑1 induction rule precisely corresponds to the primitive recursive closure operator, and ∑1 collection rule, introduced below, corresponds to the elementary closure operator.



    Upload a copy of this work     Papers currently archived: 91,998

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Accessible recursive functions.Stanley S. Wainer - 1999 - Bulletin of Symbolic Logic 5 (3):367-388.
Variations on a theme by Weiermann.Toshiyasu Arai - 1998 - Journal of Symbolic Logic 63 (3):897-925.
Elementary realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.
Syntactic translations and provably recursive functions.Daniel Leivant - 1985 - Journal of Symbolic Logic 50 (3):682-688.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
The Problem of Induction.Gilbert Harman & Sanjeev R. Kulkarni - 2006 - Philosophy and Phenomenological Research 72 (3):559-575.
Some restrictions on simple fixed points of the integers.G. L. McColm - 1989 - Journal of Symbolic Logic 54 (4):1324-1345.


Added to PP

52 (#306,694)

6 months
30 (#106,270)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Arithmetical Reflection and the Provability of Soundness.Walter Dean - 2015 - Philosophia Mathematica 23 (1):31-64.
Provability algebras and proof-theoretic ordinals, I.Lev D. Beklemishev - 2004 - Annals of Pure and Applied Logic 128 (1-3):103-123.
Axiomatization of provable n-provability.Evgeny Kolmakov & Lev Beklemishev - 2019 - Journal of Symbolic Logic 84 (2):849-869.

View all 29 citations / Add more citations

References found in this work

The incompleteness theorems.Craig Smorynski - 1977 - In Jon Barwise (ed.), Handbook of mathematical logic. New York: North-Holland. pp. 821 -- 865.
On the scheme of induction for bounded arithmetic formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (C):261-302.
Reflection Principles and Their Use for Establishing the Complexity of Axiomatic Systems.Georg Kreisel & Azriel Lévy - 1968 - Zeitschrift für Mathematische Logic Und Grundlagen der Mathematik 14 (1):97--142.
Fragments of arithmetic.Wilfried Sieg - 1985 - Annals of Pure and Applied Logic 28 (1):33-71.

View all 16 references / Add more references