Reverse mathematics and well-ordering principles

The paper is concerned with generally Pi^1_2 sentences of the form '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 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, we shall focus on the well-known psi-function which figures prominently in so-called predicative proof theory. However, the approach taken here lends itself to generalization in that the techniques we employ can be applied to many other proof-theoretic functions associated with cut elimination theorems. In this paper we show that the statement 'if X is well ordered then 'X0 is well ordered' is equivalent to ATR0. This was first proved by Friedman, Montalban and Weiermann [7] using recursion-theoretic and combinatorial methods. The proof given here is proof-theoretic, the main techniques being Schuette's method of proof search (deduction chains) [13], generalized to omega logic, and cut elimination for infinitary ramified analysis