Some independence results related to finite trees

Philos Trans A Math Phys Eng Sci. 2023 May 29;381(2248):20220017. doi: 10.1098/rsta.2022.0017. Epub 2023 Apr 10.

Abstract

We investigate some concrete independence results for systems of reverse mathematics which emerge from monotonicity properties of number-theoretic functions. Natural properties of the less than or equal to relation with respect to sums of natural numbers lead to independence results for first-order Peano arithmetic. Natural properties of the less than or equal to relation with respect to sums and products of natural numbers lead to independence results for arithmetical transfinite recursion. By considering number-theoretic functions of arbitrary arities, we obtain independence results for systems beyond arithmetical transfinite recursion. We discuss how these embeddability relations are related to tree embeddability relations and we consider variants where the tree embeddability relation is not assumed to preserve infima. The findings of this paper are complementary to results on Kruskal-like theorems proved earlier by the first author. This article is part of the theme issue 'Modern perspectives in Proof Theory'.

Keywords: Kruskal’s theorem; independence results; maximal order types; miniaturizations; well-partial orderings; well-quasi orderings.