The proof-theoretic analysis of _1¹ transfinite dependent choice

DOI10.1016/S0168-0072(03)00006-XMaRDI QIDQ1400604zbMATH OpenFDO

Authors Christian Rüede

Publication date 13 August 2003

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

Full work available at URL https://doi.org/10.1016/S0168-0072(03)00006-X

zbMATH Keywords

\(\Sigma_1^1\) transfinite dependent choiceMetapredicativityOrdinal analysisSubsystems of analysis

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Recursive ordinals and ordinal notations (03F15) Second- and higher-order arithmetic and fragments (03F35)

Review text

The theory \((\Sigma^1_1\text{-TDC})_0\) of \(\Sigma^1_1\) transfinite dependent choice is a strengthening of \(\Sigma^1_1\) dependent choice \((\Sigma^1_1\text{-DC})_0\) [cf. \textit{A. Cantini}, J. Symb. Log. 51, 360-373 (1986; Zbl 0632.03046)], which states the existence of implicitly \(\Sigma^1_1\) definable sequences along an arbitrary well-ordering. The author gives a proof-theoretic analysis of this subsystem of analysis. For the lower bound a well-ordering proof is given (following \textit{T. Strahm}'s work [in: S. B. Cooper et al. (eds.), Sets and proofs. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 258, 383-402 (1999; Zbl 0961.03057); J. Symb. Log. 67, 260-278 (2002; Zbl 1032.03050), reviewed above]). The proof of the upper bound shows the standard methods of infinitary proof theory at work. As proof-theoretic strength of the theory one gets \(\varphi\), \(\omega\), \(0\), \(0\) (in terms of the ternary Veblen function \(\varphi\) [cf., e.g., \textit{G. Jäger}, \textit{R. Kahle, A. Setzer} and \textit{T. Strahm}, J. Symb. Log. 64, 53-67 (1999; Zbl 0937.03065)]). Therefore, \((\Sigma^1_1\text{-TDC})_0\) is an example of a subsystem of analysis belonging to the new area of {metapredicative proof theory}.

Recommendations

• Transfinite dependent choice and ω-model reflection
• scientific article; zbMATH DE number 193575
• The proof-theoretic analysis of transfinitely iterated fixed point theories
• Fixed point theories and dependent choice
• Proof theory and ordinal analysis

Cites work

• Fixed point theories and dependent choice
• scientific article; zbMATH DE number 4033739 (Why is no real title available?)
• scientific article; zbMATH DE number 4039890 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1390282 (Why is no real title available?)
• scientific article; zbMATH DE number 1420857 (Why is no real title available?)
• Kennzeichnung von Ordnungszahlen durch rekursiv erklärte Funktionen
• On the relation between choice and comprehension principles in second order arithmetic
• On the relationship between ATR₀ and
• Reflecting on incompleteness
• Systems of explicit mathematics with non-constructive -operator and join
• The proof-theoretic analysis of transfinitely iterated fixed point theories
• The strength of Martin-Löf type theory with a superuniverse. I
• Transfinite dependent choice and ω-model reflection
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• Wellordering proofs for metapredicative Mahlo

Cited in

(4)

• On the relationship between fixed points and iteration in admissible set theory without foundation
• Reflections on reflections in explicit mathematics
• Transfinite dependent choice and ω-model reflection
• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic

This page was built for publication: The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice

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