Inductive definitions over a predicative arithmetic

DOI10.1016/J.APAL.2005.05.011MaRDI QIDQ2566072zbMATH OpenOpenAlexFDO

Authors Stanley S. Wainer, Richard S. Williams

Publication date 22 September 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.011

zbMATH Keywords

inductive definitionsordinal analysispredicative arithmeticproof-theoretical investigationprovably recursive functions

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20) Recursive ordinals and ordinal notations (03F15) First-order arithmetic and fragments (03F30)

Review text

The paper begins with a brief survey of work by Ostrin and Wainer on the development of the theory EA(I;O), alternative to Leivant's, which codifies the basic principles of predicative arithmetic. The main part is devoted to a Buchholz-style proof-theoretical investigation of the theory ID\(_{1}\)(I;O) of (non-iterated) inductive definitions over predicative arithmetic. It is shown that no matter which inductive definitions are added (even Kleene's \({\mathcal O}\)), its strength, in terms of provably recursive functions, is never greater than PA. Thus PA is recaptured as the predicative theory of one inductive definition.

Recommendations

• Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
• The proof theory of classical and constructive inductive definitions. A forty year saga, 1968--2008
• New Computational Paradigms
• Induction and inductive definitions in fragments of second order arithmetic
• Proof-theoretic strengths of weak theories for positive inductive definitions

Cites work

• A new recursion-theoretic characterization of the polytime functions
• A slow growing analogue to Buchholz' proof
• An independence result for \((\Pi^ 1_ 1-CA)+BI\)
• Characterizing the elementary recursive functions by a fragment of Gödel's \(T\)
• Consistency proof via pointwise induction
• Elementary arithmetic
• scientific article; zbMATH DE number 3781167 (Why is no real title available?)
• scientific article; zbMATH DE number 1215495 (Why is no real title available?)
• scientific article; zbMATH DE number 3999883 (Why is no real title available?)
• scientific article; zbMATH DE number 2110622 (Why is no real title available?)
• Π12-logic, Part 1: Dilators

Cited in

(6)

• Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
• The proof theory of classical and constructive inductive definitions. A forty year saga, 1968--2008
• A theory of formal truth arithmetically equivalent to ID₁
• scientific article; zbMATH DE number 1342277 (Why is no real title available?)
• ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
• New Computational Paradigms

This page was built for publication: Inductive definitions over a predicative arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566072)