Content area
This dissertation explores different approaches for determining the strength of mathematical statements, as expressed in the language of second order arithmetic. The statements that we consider mainly concern ordered structures that satisfy a variety of strong well-foundedness properties, such as being a well order, a well partial order, or a better quasi order, as well as appropriate classes of transformations which preserve those properties. We analyse those statements using methods from reverse mathematics and ordinal analysis: in most situations, we work in subsystems that are at least strong enough to prove arithmetical transfinite recursion.
One example is that of a theorem by Dushnik and Miller, which states that a countable linear order is a well order precisely when its initial segments cannot be collapsed via embeddings. Our analysis shows that the theorem, in its full generality, is equivalent to the principle of arithmetical transfinite recursion over recursive comprehension. This is consistent with the existing literature on the reverse mathematics of well orders, which shows that many fundamental properties of well orders are equivalent to arithmetical transfinite recursion. We also analyse some restrictions of the theorem to appropriate classes of linear orders, which can be proved even in weaker subsystems.
A particular focus is reserved for the reverse mathematics of better quasi orders. We consider the statement that a finite quasi order with at least three incomparable elements is a better quasi order: its exact strength is one of the most studied problems in the field. Recent work by Freund has shown that that statement implies the principle of arithmetical recursion along the natural numbers, i.e. the main axioms of the subsystem ACA+0. We improve that result by showing that the two cannot be equivalent. That is done by an argument from ordinal analysis. which amounts to proving that a notation system for the proof theoretic ordinal of ACA+0 is well founded.
We also deal extensively with the related notion of ∆02-better quasi order, which features prominently in Montalbán's analysis of Fraïssé's conjecture in Π11 comprehension. We show that many results from the reverse mathematics of better quasi orders, both classical and recent, admit close analogous versions for ∆02-better quasi orders in suitably strong theories. Moreover, we prove a new characterization of ∆02-better quasi orders in terms of a class of ill founded trees which are labelled in a sufficiently regular way: namely, we only allow for finitely many changes of label along each infinite path.
Finally, we study a notion of strong normality for well partial order dilators. Well partial order dilators are a class of particularly regular transformations, which generalizes the notion of dilator originally introduced by Girard for well orders. Freund, Rathjen and Weiermann have studied the strength of the statement that all normal well partial order dilators admit a well founded fixed point. That statement is stronger than the analogous one for normal dilators, as it is equivalent to Π11 comprehension rather than just II induction. We show that the restriction of that statement to strongly normal dilators on well partial orders is equivalent to Π11 induction as well. Moreover, we obtain another desirable property, not verified by well partial order dilators that are just normal: in fact, the strongly normal ones induce a normal function on the ordinals, just like normal dilators on well orders.