\(\Pi_1^1\)-comprehension as a well-ordering principle (Q2274030): Difference between revisions

Using \(\mathsf{ATR}^{\mathsf{set}}_0\) as a base system, the author proves that \(\Pi^1_1\)-comprehension is equivalent to the principle that every dilator has a Bachmann-Howard fixed point. This is a well-ordering principle of type 2, so the result proves conjectures of \textit{M. Rathjen} [Tributes 22, 179--212 (2014; Zbl 1358.03022)] and \textit{A. Montalbán} [Bull. Symb. Log. 17, No. 3, 431--454 (2011; Zbl 1233.03023)]. The equivalence result can be sharpened to hold over \(\mathsf{RCA}_0\), as shown in [the author, ``Computable aspects of the Bachmann-Howard Principle'', J. Math. Logic (to appear)]. The paper is based on parts of the author's PhD thesis [Type-two well-ordering principles, admissible sets, and \(\Pi^1_1\)-comprehension. Leeds: University of Leeds (PhD Thesis) (2018)].