scientific article; zbMATH DE number 2186968

MaRDI QIDQ3025192zbMATH OpenFDO

Authors Klaus Aehlig

Publication date 12 July 2005

zbMATH Keywords

inductive definitionsproof-theoretic strengthprovably recursive functions

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Inductive definability (03D70) Second- and higher-order arithmetic and fragments (03F35) Constructive and recursive analysis (03F60)

Review text

This book is the author's dissertation. It consists of a thorough analysis of theories formalizing finitely iterated inductive definitions. In the first chapter the theories are defined in several variations and their proof-theoretic strength is determined. These results (together with some completions of chapter 2.2) are published separately [\textit{K. Aehlig}, J. Symb. Log. 70, No. 4, 1087--1107 (2005)]. In chapter 2 induction on the natural numbers is added. It is shown that ``[o]n the one hand, adding full induction results in an increase of the proof-theoretical strength by an additional inductive definition. On the other hand induction on arithmetical formulae only affects the arithmetical consequences of the system. [p.~31] The third chapter contains a discussion of fragments of system F which characterize the provably recursive function of the theories under considerations. In the final section the limit of the theories, \(\text{ID}^c_{<\omega}\), is considered which can be characterized as the one-variable fragment of intuitionistic analysis.

Recommendations

• Weak determinacy and iterations of inductive definitions
• Induction and inductive definitions in fragments of second order arithmetic
• Proof-theoretic strengths of weak theories for positive inductive definitions
• Recursion theory on weak fragments of Peano arithmetic: A study of definable cuts
• A finite axiomatisation of inductive-inductive definitions
• An interpretation of intuitionistic analysis with restricted transfinite inductive definitions
• A Proof-Theoretic Analysis of Theories for Stratified Inductive Definitions
• Finiteness axioms on fragments of intuitionistic set theory
• Forcing and reductibilities. II. Forcing in fragments of analysis
• scientific article; zbMATH DE number 515737

Cited in

(6)

• The metamathematics of ergodic theory
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
• A note on the theory of positive induction, \({{\text{ID}}^*_1}\)
• Fragment of Nonstandard Analysis with a Finitary Consistency Proof
• Iterated inductive definitions revisited
• Schwichtenberg's style analysis of parameter-free fragments of Girard's system F

This page was built for publication:

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