×

The proof-theoretic analysis of transfinitely iterated quasi least fixed points. (English) Zbl 1115.03084

The author gives a proof-theoretic analysis of the iterated fixed-point theories \(\mathsf{ID}_{\alpha}^*\), \(\alpha\) less than a certain ordinal \(\Phi_0\). The theories \(\mathsf{ID}_{\alpha}^*\) are defined as the well-known theories \(\mathsf{ID}_{\alpha},\) but induction on the fixed points is restricted to formulas that contain fixed-point constants only positively. It is shown that the proof-theoretic ordinals \(| \mathsf{ID}_{\alpha}^*| \) of \(\mathsf{ID}_{\alpha}^*\) coincide with the ones of \(\widehat{\mathsf{ID}}_{\alpha}\), the theories \(\mathsf{ID}_{\alpha}\) but without any induction on fixed points.

MSC:

03F35 Second- and higher-order arithmetic and fragments
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Bollettino Unione Mathematica Italiana 4 pp 413– (1985)
[2] On the relationship between choice and comprehension principles in second order arithmetic 51 pp 360– (1986)
[3] On the relationship between ATR0 61 pp 768– (1996)
[4] The strength of Martin-Löf’s type theory with one universe (1977)
[5] Subsystems of Second Order Arithmetic (1998)
[6] Handbook of Mathematical Logic pp 867– (1977)
[7] Proof Theory (1977)
[8] Annals of Pure and Applied Logic 121 pp 195– (2003)
[9] Archive for Mathematical Logic pp 561– (2005)
[10] Proof Theory: An Introduction 1407 (1989)
[11] Lectures on modern mathematics III pp 95– (1965)
[12] The proof-theoretic analysis of transfinitely iterated fixed point theories 64 pp 53– (1999) · Zbl 0937.03065
[13] DOI: 10.1002/malq.200310097 · Zbl 1049.03039
[14] Reflecting on incompleteness 56 pp 1– (1991)
[15] The Patras Symposion pp 171– (1982)
[16] Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies 897 (1981) · Zbl 0489.03022
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.