Ordinal Analysis of Well-Ordering Principles, Well Quasi-Orders Closure Properties, and $\Sigma_n$-Collection Schema

TL;DR

This paper conducts an ordinal analysis of well-ordering principles, closure properties of well quasi-orders, and the $ ext{B} ext{-} ext{Sigma}_n$ collection schema, extending proof-theoretic results for Kruskal's theorem and related principles.

Contribution

It computes the $ ext{Pi}^1_1$ ordinals of labelled Kruskal's theorems and analyzes their connection to well quasi-order principles and other logical systems.

Findings

Calculated the $ ext{Pi}^1_1$ ordinals for labelled Kruskal's theorems.

Established connections between well quasi-order principles and Ramsey and computational theories.

Extended ordinal analysis to the $ ext{B} ext{-} ext{Sigma}_n$ collection schema.

Abstract

The study of well quasi-orders, wqo, is a cornerstone of combinatorics and within wqo theory Kruskal's theorem plays a crucial role. Extending previous proof-theoretic results, we calculate the $\Pi^1_1$ ordinals of two different versions of labelled Kruskal's theorem: $\forall n \,$ $\mbox{KT}_\ell(n)$ and $\mbox{KT}_{\omega}(n)$; 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 $g$, WOP$(g)$ amounts to the following principle $\forall X\, [\mbox{WO}(X) \rightarrow \mbox{WO}(g(X))]$, where $WO(X)$ states that ``$X$ is a well-order''. In our case, the two ordinal functions involved are ${g}_{\forall}(X)=\sup_{n}\vartheta(\Omega^n \cdot X)$ and ${g}_{\omega}(X)=\vartheta(\Omega^{\omega}\! \cdot X)$. 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 $G$ that preserves the property of being a wqo, its Well Quasi-orders closure Property, WQP$(G)$, is given by the principle $\forall Q\, [Q\, \mbox{wqo} \rightarrow G(Q)\, \mbox{wqo}]$. Conducting this study, unexpected connections with different principles arising from Ramsey and Computational theory, such as RT$^2_{<\infty}$, CAC, ADS, RT$^1_{<\infty}$, turn up. Lastly, extending and combining previous results, we achieve also the ordinal analysis of the collection schema $\mbox{B}\Sigma_n$.