Fixed point theories and dependent choice
ATR is Friedman's famous system of second-order arithmetic for arithmetical transfinite recursion; \(\text{ATR}_0\) is ATR with induction on the natural numbers restricted to sets of natural numbers; \((\Sigma^1_1\text{-DC})\) is the usual schema of dependent choice for \(\Sigma^1_1\) formulas. With \(\widehat{\text{ID}}_\alpha\) we denote the first-order system for \(\alpha\) times iterated fixed points generated by positive arithmetic operator forms; \(\widehat{\text{ID}}_{<\beta}\) denotes the union of the theories \(\widehat{\text{ID}}_\alpha\) for \(\alpha<\beta\). In this paper we establish the proof-theoretic equivalence of (i) ATR and \(\widehat{\text{ID}}_\omega\), (ii) \(\text{ATR}_0 + (\Sigma^1_1\text{-DC})\) and \(\widehat{\text{ID}}_{<\omega^\omega}\), and (iii) \(\text{ATR} +(\Sigma^1_1\text{-DC})\) and \(\widehat{\text{ID}}_{<\varepsilon_0}\).
- On the relationship between ATR0 and
- The proof-theoretic analysis of transfinitely iterated fixed point theories
- About the proof-theoretic ordinals of weak fixed point theories
- Ranked structures and arithmetic transfinite recursion
- The proof-theoretic analysis of transfinitely iterated quasi least fixed points
- Some results on cut-elimination, provable well-orderings, induction and reflection
- The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice
- Full and hat inductive definitions are equivalent in NBG
- Forcing for hat inductive definitions in arithmetic
- About the proof-theoretic ordinals of weak fixed point theories
- Wellordering proofs for metapredicative Mahlo
- Transfinite dependent choice and ω-model reflection
- scientific article; zbMATH DE number 1420857 (Why is no real title available?)
This page was built for publication: Fixed point theories and dependent choice
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1590660)
