Well-Ordering Principles across Reverse Mathematics

In this thesis, we use the means of reverse mathematics in order to study the proof-theoretic strength of several principles involving well orders and well partial orders. The strengths of our considered statements cover each of the Big Five, the most prominent systems of reverse mathematics, as well as some outliers of the so-called "zoo". We begin by exploring effective transfinite recursion, a concept from recursion theory that can be used for the definition of computable functions along ordinals. In the context of second-order arithmetic, the logical framework of reverse mathematics, we can formulate a similar principle, that allows for the recursive definition of a family of sets using effective means along well orders. We compare a definition due to Dzhafarov, Flood, Solomon, and Westrick with a variation due to Freund and determine their proof-theoretic strengths, characterized by the systems WKL\(_0\) and ACA\(_0\), respectively. Also, we discuss a rule version of this recursion principle, which is already available in the weakest of the Big Five: RCA\(_0\). It is easy to define a partial order on finite sequences. This operation preserves well partial orders, a result known as Higman's lemma, and can be used to characterize arithmetical comprehension. Gordeev could show that a variant of Higman's lemma involving a so-called gap condition, which goes back to Friedman, captures ATR\(_0\). We reproduce his result by a simpler proof and extend it to well partial orders as well as other variants of the gap condition and certain trees. For the case of well orders, we determine the maximal order types of all considered structures. The termination of Goodstein sequences is a popular example of a true statement that cannot be proved using the means of Peano arithmetic or, in our case, arithmetical comprehension. In order to obtain a higher proof-theoretic strength using such a principle, Abrusci, Girard, and van de Wiele combined a similar construction with Girard's concept of dilators. The termination of the resulting inverse Goodstein sequence is true, but not provable in certain impredicative systems such as ID\(_1\). In fact, the termination happens at the well-known Bachmann-Howard ordinal. Inspired by a conjecture due to Andreas Weiermann, we capture the strength of general increasing dilator sequences using \(\Pi^1_1\)-comprehension, the characterizing axiom of \(\Pi^1_1\)-CA\(_0\). For this, we employ the new tool of 1-fixed points due to Freund and Rathjen, which is based on the earlier concept of Bachmann-Howard fixed points due to Freund. The close connection between points of termination of increasing dilator sequences and 1-fixed points allows explicit notation systems for the reached ordinals and is valid even outside the confines of second-order arithmetic. Our final topic considers the uniform Kruskal theorem due to Freund, Rathjen, and Weiermann. This principle, which is closely related to Bachmann-Howard- and 1-fixed points, generalizes the well-known Kruskal theorem and allows for the construction of recursive data types that are well partial orders. The main result of these authors is the equivalence between their theorem and the principle of \(\Pi^1_1\)-comprehension. However, this equivalence is not proved over only RCA\(_0\), but requires a further axiom ADS, a weak consequence of Ramsey's theorem. Following from an observation on a proof due to Hirst, we show that this additional axiom can be omitted. In joint work with Anton Freund, however, we reveal by certain conservativity results that assumptions like ADS are crucial for giving fragments of the uniform Kruskal theorem proof-theoretic strength.