Well-ordering principles in Proof theory and Reverse Mathematics
March 4, 2020 4:30 pm - 5:30 pm
Logic Center, 2 Arrow St, Rm 420
Michael Rathjen - University of Leeds
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