Elementary descent recursion and proof theory

DOI10.1016/0168-0072(94)00003-LMaRDI QIDQ1344279zbMATH OpenOpenAlexFDO

Authors Michael Sheard, Harvey M. Friedman

Publication date 9 February 1995

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

Full work available at URL https://doi.org/10.1016/0168-0072(94)00003-l

zbMATH Keywords

functionalsGrzegorczyk hierarchyHardy hierarchyordinal estimates for provably recursive functionstransfinite inductiontransfinite recursionwell- orderings

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20) Proof theory in general (including proof-theoretic semantics) (03F03) Recursive ordinals and ordinal notations (03F15) First-order arithmetic and fragments (03F30)

Review text

As the authors say in the introduction, much of the results of this paper will look familiar to proof theorists. They include basic properties of functions and functionals defined by transfinite recursion, connection of Grzegorczyk and Hardy hierarchies and ordinal estimates for provably recursive functions and well-orderings of the systems with some forms of mathematical and transfinite induction. The emphasis is on detailed and careful proofs, and some refinements, like construction of a primitive recursive cut-elimination operator, are sacrificed.

Recommendations

• Recursion and proofs
• A proof-theoretic account of primitive recursion and primitive iteration
• scientific article; zbMATH DE number 941039
• Recursion theory in a lower semilattice
• Recursion, induction and well-founded orders
• Towards an algebraic theory of recursion
• Recursion theory. Computational aspects of definability
• scientific article; zbMATH DE number 2222029
• scientific article; zbMATH DE number 3857082
• Induction rules, reflection principles, and provably recursive functions

Cites work

• Finite investigations of transfinite derivations
• scientific article; zbMATH DE number 3857078 (Why is no real title available?)
• scientific article; zbMATH DE number 3550662 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 3327279 (Why is no real title available?)
• On n-quantifier induction
• Proof theory

Cited in

(24)

• Phase transitions for Gödel incompleteness
• Reverse mathematics and well-ordering principles: a pilot study
• Rudimentary relations and primitive recursion: A toolbox
• Some results on cut-elimination, provable well-orderings, induction and reflection
• Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones
• Recursive proof composition from accumulation schemes
• An ordinal analysis for theories of self-referential truth
• Update procedures and the 1-consistency of arithmetic
• Sub-computabilities
• Classifying the Provably Total Functions of PA
• Goodstein sequences for prominent ordinals up to the Bachmann-Howard ordinal
• Variations on a theme by Weiermann
• How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
• An application of graphical enumeration to PA *
• scientific article; zbMATH DE number 941039 (Why is no real title available?)
• How to characterize provably total functions by local predicativity
• A note on fragments of uniform reflection in second order arithmetic
• A mathematical commitment without computational strength
• Long finite sequences
• Mining the surface: witnessing the low complexity theorems of arithmetic
• Fundamental sequences and fast-growing hierarchies for the Bachmann-Howard ordinal
• Witnessing flows in arithmetic
• Subsystems of true arithmetic and hierarchies of functions
• Peano arithmetic, games and descent recursion

This page was built for publication: Elementary descent recursion and proof theory

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