The uniform Kruskal theorem: a bridge between finite combinatorics and abstract set existence

Anton Freund

An important theorem of J. Kruskal states that any infinite sequence t₀,t₁,… of finite trees admits i<j such that t_i embeds into t_j. As shown by H. Friedman, this theorem – and even a ‘finitized’ corollary – is unprovable in predicative axiom systems, such as the theory ATR₀ from reverse mathematics. This is one of the most convincing mathematical examples for the incompleteness phenomenon from Gödel’s theorems.

The ‘minimal bad sequence lemma’ due to C. Nash-Williams provides a particularly elegant proof of Kruskal’s theorem. By a result of A. Marcone, this lemma is equivalent to the impredicative principle of Π₁¹-comprehension, over a weak base theory from reverse mathematics. Kruskal’s theorem itself cannot be equivalent to this principle, as its quantifier complexity is too low. This suggests the following question:

In which sense can we view Kruskal’s theorem as the concrete ‘shadow’ of an abstract set existence principle?

To suggest an answer, I will present joint work with M. Rathjen and A. Weiermann [4], which shows that Π₁¹-comprehension is equivalent to a uniform version of Kruskal’s theorem (with general recursive data types at the place of trees). Together with the aforementioned result of Marcone, this confirms the intuition that minimal bad sequences provide ‘the’ canonical proof.

An analogous equivalence [2] has been established between Π₁¹-transfinite recursion, a minimal bad sequence result of I. Kříž, and a uniform version of Friedman’s extended Kruskal theorem with ordinal labels and gap condition. The results rely on previous work [1, 3] that connects the ‘concrete’ viewpoint of ordinal analysis with the more ‘abstract’ setting of reverse mathematics.

The results and proofs will be presented on an intuitive level. Beyond the specific case of Kruskal’s theorem, the hope is to shed some light on a remarkable phenomenon in modern mathematics: that concrete statements about finite objects are sometimes proved via abstract and infinite ones.

References

[1]

Anton Freund, Π₁¹-comprehension as a well-ordering principle, Advances in Mathematics, vol. 355 (2019), article no. 106767, 65 pp.

[2]

Anton Freund, Reverse mathematics of a uniform Kruskal-Friedman theorem, arXiv:2112.08727 (preprint), 25 pp.

[3]

Anton Freund and Michael Rathjen, Well ordering principles for iterated Π₁¹-comprehension, arXiv:2112.08005 (preprint), 67 pp.

[4]

Anton Freund, Michael Rathjen and Andreas Weiermann, Minimal bad sequences are necessary for a uniform Kruskal theorem, Advances in Mathematics, vol. 400 (2022), article no. 108265 , 44 pp.

This document was translated from L^AT_EX by H^EV^EA.

 Overview  Program