Reverse mathematics and well-ordering principles: a pilot study (Q1032626)

This paper is part of the larger project of studying the proof-theoretic and computability-theoretic complexity of sentences of the form ``if \(X\) is well-ordered then \(f(X)\) is well-ordered'', where \(f\) is a function from linear ordering to linear orderings that maps ordinals to ordinals. It has turned out that, when \(f\) is a standard proof-theoretic function, a statement of this form is often equivalent to the existence of countable coded \(\omega \)-models for a particular theory \(T_f\) whose consistency can be proved by means of a cut-elimination theorem in infinitary logic which crucially involves the function \(f\). To illustrate this theme, the authors prove in this paper that the statement ``if \(X\) is well-ordered then \(\varepsilon_X\) is well-ordered'' is equivalent to \(\text{ACA}_0^+\). This result was first proved by \textit{A. Marcone} and \textit{A. Montalbán} [``The Veblen functions for computability theorists'' (to appear)] using computability-theoretic and combinatorial methods to code the \(\omega\)-Turing jump. The proof given here is principally proof-theoretic, the main techniques being Schütte's method of proof search (deduction chains) [\textit{K. Schütte}, Proof theory. Berlin-Heidelberg-New York: Springer-Verlag (1977; Zbl 0367.02012)] and cut elimination for a (small) fragment of \(\mathcal L_{\omega_1,\omega}\). It is remarkable how the same result has two such different proofs.