Ordinal Analysis of Well-Ordering Principles, Well Quasi-Orders Closure Properties, and Σ n -Collection Schema

Source abstract

The study of well quasi-orders, wqo , is a relevant part of combinatorics and within wqo theory Kruskal’s theorem plays a crucial role. Extending previous proof-theoretic results, we calculate the [Formula: see text] ordinals of two different versions of labelled Kruskal’s theorem: [Formula: see text] K[Formula: see text] and K[Formula: see text] [Formula: see text]denoting, respectively, all the cases of labelled Kruskal’s theorem for trees with an upper bound on the branching degree, and the standard Kruskal’s theorem for labelled trees. In order to reach these computations, a key step is to move from Kruskal’s theorem, which regards preservation of wqo ’s, to an equivalent Well-Ordering Principle (WOP), regarding instead preservation of well-orders. Given an ordinal function [Formula: see text], WOP[Formula: see text] amounts to the following principle [Formula: see text], where WO[Formula: see text] states that “[Formula: see text] is a well-order”. In our case, the two ordinal functions involved are [Formula: see text] and [Formula: see text]. In addition to the ordinal analysis of Kruskal’s theorem and its related WOP, a series of Well Quasi-orders Principles (WQP) is considered. Given a set operation [Formula: see text] that preserves the property of being a wqo , its Well Quasi-orders Principle, WQP[Formula: see text], is given by the statement [Formula: see text]. Conducting this study, unexpected connections with different principles arising from Ramsey and Computational theory, such as RT[Formula: see text], CAC, ADS, RT[Formula: see text], turn up. Lastly, extending and combining previous results, we also obtain the ordinal analysis of the collection schema [Formula: see text] within a weak base theory.