Reverse mathematics and well-ordering principles: A pilot study

The larger project broached here is to look at the generally Π 2 1 sentence “if X is well-ordered then f ( X ) is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω -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, we prove in this paper that the statement “if X is well-ordered then ε X is well-ordered” is equivalent to ACA 0 + . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search (deduction chains) [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a (small) fragment of L ω 1 , ω .