The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice (Q1400604)

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}.