Well-ordering principles in Proof theory and Reverse Mathematics

There are several familiar theories of reverse mathematics that can be characterized by well-ordering principles 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). Some of these equivalences have been obtained by recursion-theoretic and combinatorial methods. They (and many more) can also be shown by proof-theoretic methods, employing search trees and cut elimination theorems in infinitary logic with ordinal bounds. One could perhaps generalize and say that every cut elimination theorem in ordinal-theoretic proof theory encapsulates a theorem of this type.

One aim of the talk is to present a general methodology underlying these results that enables one to construct omega-models of particular theories from (*).

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 more than 10 years ago, but its proof has only been worked out by Anton Freund in recent years