Induction rules, reflection principles, and provably recursive functions
type: Item
instance of: scholarly article
title: Induction rules, reflection principles, and provably recursive functions
zbMATH Open document ID: 0882.03055
DOI: 10.1016/S0168-0072(96)00045-0
author: Lev D. Beklemishev
published in: Annals of Pure and Applied Logic
publication date: 1998-03-12T00:00:00Z
review text: The author characterizes \(\Pi_n\)- and \(\Sigma_n\)-induction rules, \(\Pi_n\)-IR and \(\Sigma_n\)-IR, respectively. With a rule, in contrast to an axiom, one can take into account how many times it is applied nestedly. Thus, for instance, \([T,\Sigma_n\text{-IR}]_k\) is the theory obtained from the given \(T\) by using \(\Sigma_n\)-IR at most \(k\) times. \(\Pi\)- and \(\Sigma\)-IR are related. He shows, for example, that \([T,\Pi_{n+2}\text{-IR}]_k\) is included in \([T,\Sigma_{n+1}\text{-IR}]_{k+1}\), where \(T\) is any \(\Pi_{n+2}\)-theory extending Kalmar elementary arithmetic, EA. The main result is the relation with the reflection principle, \(\text{RFN}_\Gamma(T)\), for formulas in \(\Gamma\). For \(T\) extending EA, \([T,\Sigma_{n+1}\text{-IR}]_1\) is equivalent to \(T+\{\text{RFN}_{\Sigma_{n+1}}(T_0)/T_0\) is finite \(\Pi_{n+2}\)-axiomatized subtheory of \(T\}\). Similar characterization of \(\Pi_n\)-IR is given with respect to \(\Pi_n\)-RFN. Results of different nature pertain to characterizations of various classes of functions. For example, for a theory \(T\) axiomatized by one \(\Pi_2\) sentence, a function is shown to be total in \([T,\Sigma_1\text{-IR}]_1\) exactly when it is obtained from the standard witness function of \(T\) by composition and one application of primitive recursion. Since the results are of a positive nature, namely a formula proved in a theory is also obtained in another way, etc., what the author does is a careful analysis of the situation at hand, using familiar tools like Herbrand theorem. This paper is self-contained, as the author provides abundant information and explanations. Indeed, he ``did not try to be overly laconic''.
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03D20
zbMATH DE Number: 1038665
zbMATH Keywords: nested applications
zbMATH Keywords: provably recursive function
zbMATH Keywords: induction rules
zbMATH Keywords: reflection principle
MaRDI profile type: MaRDI publication profile
cites work: Q3962995
cites work: Q5286672
cites work: Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
cites work: The optimality of induction as an axiomatization of arithmetic
cites work: Q5628105
cites work: Reflection Principles in Fragments of Peano Arithmetic
cites work: Hierarchies of Primitive Recursive Functions
cites work: Q5600870
cites work: On n-quantifier induction
cites work: Q5533181
cites work: Q3325707
cites work: Q3866106
cites work: Rekursionszahlen und die Grzegorczyk-Hierarchie
cites work: Fragments of arithmetic
cites work: Herbrand analyses
cites work: Q4525292
cites work: On the scheme of induction for bounded arithmetic formulas
full work available at URL: s0168-0072(96)00045-0
OpenAlex ID: W2076792546
Recommended article: Q4981456
Recommended article: Q4364507
Recommended article: Parameter free induction and provably total computable functions
Recommended article: Computer Science Logic
description: scientific article; zbMATH DE number 1038665