  Several theorems about the equivalence of familiar theories of reverse
mathematics with certain well-ordering principles have been proved by
recursion-theoretic and combinatorial methods (Friedman, Marcone, Montalban et
al.) and with far-reaching results by proof-theoretic technology (Afshari,
Freund, Girard, Rathjen, Thomson, Valencia Vizcano, Weiermann et al.),
employing deduction search trees and cut elimination theorems in infinitary
logics with ordinal bounds in the latter case. At type level one, the
well-ordering principles are 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 (such f's are always dilators). One aim of the paper is to present a
general methodology underlying these results that enables one to construct
omega-models of particular theories from (*) and even beta-models from the type
2 version of (*).
  As (*) is of complexity Pi-1-2 such a principle cannot characterize stronger
comprehensions at the level of Pi-1-1-comprehension. This requires a higher
order version of (*) that employs ideas from ordinal representation systems
with collapsing functions used in impredicative proof theory. The simplest one
is the Bachmann construction. Relativizing the latter construction to any
dilator f and asserting that this always yields a well-ordering turns out to be
equivalent to Pi-1-1-comprehension. This result has been conjectured and a
proof strategy adumbrated roughly 10 years ago, but the proof has only been
worked out in recent years.
