Induction rules, reflection principles, and provably recursive functions
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.
- Fragments of arithmetic
- Herbrand analyses
- Hierarchies of Primitive Recursive Functions
- scientific article; zbMATH DE number 3857078 (Why is no real title available?)
- scientific article; zbMATH DE number 3668596 (Why is no real title available?)
- scientific article; zbMATH DE number 3784875 (Why is no real title available?)
- scientific article; zbMATH DE number 1555192 (Why is no real title available?)
- scientific article; zbMATH DE number 227056 (Why is no real title available?)
- scientific article; zbMATH DE number 3247155 (Why is no real title available?)
- scientific article; zbMATH DE number 3320380 (Why is no real title available?)
- scientific article; zbMATH DE number 3353255 (Why is no real title available?)
- Induction rules, reflection principles, and provably recursive functions
- On n-quantifier induction
- On the scheme of induction for bounded arithmetic formulas
- Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
- Reflection Principles in Fragments of Peano Arithmetic
- Rekursionszahlen und die Grzegorczyk-Hierarchie
- The optimality of induction as an axiomatization of arithmetic
- Interpretability in PRA
- Some results on cut-elimination, provable well-orderings, induction and reflection
- Elementary descent recursion and proof theory
- Induction rules, reflection principles, and provably recursive functions
- Provability algebras and proof-theoretic ordinals. I
- A note on the \(\Pi_ 2^ 0\)-induction rule
- Parameter free induction and provably total computable functions
- Unprovability results for clause set cycles
- Hyperarithmetical worm battles
- Induction rules in bounded arithmetic
- On axiom schemes for \(T\)-provably \(\Delta_1\) formulas
- Local induction and provably total computable functions
- The closed fragment of the interpretability logic of PRA with a constant for I\(\Sigma^1\)
- Local induction and provably total computable functions: a case study
- scientific article; zbMATH DE number 3948262 (Why is no real title available?)
- Parameter free induction and reflection
- scientific article; zbMATH DE number 1966617 (Why is no real title available?)
- On the induction schema for decidable predicates
- Proof theoretic analysis by iterated reflection
- Fragments of Arithmetic and true sentences
- Arithmetical interpretations and Kripke frames of predicate modal logic of provability
- Provably recursive functions of reflection
- A note on fragments of uniform reflection in second order arithmetic
- Honest elementary degrees and degrees of relative provability without the cupping property
- AXIOMATIZATION OF PROVABLE n-PROVABILITY
- Computer Science Logic
- PREDICATIVITY THROUGH TRANSFINITE REFLECTION
- Functions provably total in $I^{-}Σ_{n}$
- MODEL THEORY AND PROOF THEORY OF THE GLOBAL REFLECTION PRINCIPLE
- AN INCOMPLETENESS THEOREM VIA ORDINAL ANALYSIS
- ON SHAVRUKOV’S NON-ISOMORPHISM THEOREM FOR DIAGONALIZABLE ALGEBRAS
- Semi-honest subrecursive degrees and the collection rule in arithmetic
- On nested simple recursion
- Adventures in Gödel Incompleteness
- Fragments of arithmetic and cyclic proofs
- Reflexivity of -consistency in a general setting
- Numeral completeness of weak theories of arithmetic
- General notions of consistency
- Consistency statements and iterations of computable functions in \(\mathrm{I}\Sigma_1\) and PRA
This page was built for publication: Induction rules, reflection principles, and provably recursive functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1361250)
