Fraïssé’s conjecture, partial impredicativity and well-ordering principles, part I

Freund, Anton

doi:10.1090/proc/17149

Fraïssé’s conjecture, partial impredicativity and well-ordering principles, part I
HTML articles powered by AMS MathViewer

by Anton Freund;

Proc. Amer. Math. Soc. 153 (2025), 937-946

DOI: https://doi.org/10.1090/proc/17149

Published electronically: February 3, 2025

HTML | PDF | Request permission

Abstract:

Fraïssé’s conjecture (proved by Laver) is implied by the $\Pi ^1_1$-comprehension axiom of reverse mathematics, as shown by Montalbán. The implication must be strict for reasons of quantifier complexity, but it seems that no better bound has been known. We locate such a bound in a hierarchy of Suzuki and Yokoyama, which extends Towsner’s framework of partial impredicativity. Specifically, we show that Fraïssé’s conjecture is implied by a principle of pseudo $\Pi ^1_1$-comprehension. As part of the proof, we introduce a cofinite version of the $\Delta ^0_2$-Ramsey theorem, which may be of independent interest. We also relate pseudo $\Pi ^1_1$-comprehension to principles of pseudo $\beta$-model reflection (due to Suzuki and Yokoyama) and reflection for $\omega$-models of transfinite induction (studied by Rathjen and Valencia-Vizcaíno). In a forthcoming companion paper, we characterize pseudo $\Pi ^1_1$-comprehension by a well-ordering principle, to get a transparent combinatorial bound for the strength of Fraïssé’s conjecture.

References

D. Fernández-Duque, P. Shafer, H. Towsner, and K. Yokoyama, Metric fixed point theory and partial impredicativity, Philos. Trans. Roy. Soc. A 381 (2023), no. 2248, Paper No. 20220012, 20. MR 4590512, DOI 10.1098/rsta.2022.0012
Anton Freund, $\Pi _1^1$-comprehension as a well-ordering principle, Adv. Math. 355 (2019), 106767, 65. MR 3994445, DOI 10.1016/j.aim.2019.106767
Anton Freund, Computable aspects of the Bachmann-Howard principle, J. Math. Log. 20 (2020), no. 2, 2050006, 26. MR 4128719, DOI 10.1142/S0219061320500063
Anton Freund, On the logical strength of the better quasi order with three elements, Trans. Amer. Math. Soc. 376 (2023), no. 9, 6709–6727. MR 4630789, DOI 10.1090/tran/8966
Anton Freund and Davide Manca, Weak well orders and Fraïssé’s conjecture, J. Symb. Log. (to appear), DOI 10.1017/jsl.2023.70.
Anton Freund, Alberto Marcone, Fedor Pakhomov, and Giovanni Soldà, Provable better quasi orders, Notre Dame Journal of Formal Logic (to appear), Preprint, arXiv:2305.01066.
Anton Freund and Michael Rathjen, Well ordering principles for iterated $\Pi ^1_1$-comprehension, Selecta Math. (N.S.) 29 (2023), no. 5, Paper No. 76, 83. MR 4654163, DOI 10.1007/s00029-023-00879-2
Harvey Friedman, Some systems of second order arithmetic and their use, Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974) Canad. Math. Congr., Montreal, QC, 1975, pp. 235–242. MR 429508
Jean-Yves Girard, Proof theory and logical complexity, Studies in Proof Theory. Monographs, vol. 1, Bibliopolis, Naples, 1987. MR 903244
Jeffry L. Hirst, Reverse mathematics and ordinal exponentiation, Ann. Pure Appl. Logic 66 (1994), no. 1, 1–18. MR 1263322, DOI 10.1016/0168-0072(94)90076-0
W. A. Howard, A system of abstract constructive ordinals, J. Symbolic Logic 37 (1972), 355–374. MR 329869, DOI 10.2307/2272979
U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008. MR 2445721
Alberto Marcone, On the logical strength of Nash-Williams’ theorem on transfinite sequences, Logic: from foundations to applications (Staffordshire, 1993) Oxford Sci. Publ., Oxford Univ. Press, New York, 1996, pp. 327–351. MR 1428011
Alberto Marcone, Wqo and bqo theory in subsystems of second order arithmetic, Reverse mathematics 2001, Lect. Notes Log., vol. 21, Assoc. Symbol. Logic, La Jolla, CA, 2005, pp. 303–330. MR 2185443
Alberto Marcone and Antonio Montalbán, The Veblen functions for computability theorists, J. Symbolic Logic 76 (2011), no. 2, 575–602. MR 2830417, DOI 10.2178/jsl/1305810765
Antonio Montalbán, Fraïssé’s conjecture in $\Pi _1^1$-comprehension, J. Math. Log. 17 (2017), no. 2, 1750006, 12. MR 3730562, DOI 10.1142/S0219061317500064
C. St. J. A. Nash-Williams, On well-quasi-ordering infinite trees, Proc. Cambridge Philos. Soc. 61 (1965), 697–720. MR 175814, DOI 10.1017/s0305004100039062
C. St. J. A. Nash-Williams, On better-quasi-ordering transfinite sequences, Proc. Cambridge Philos. Soc. 64 (1968), 273–290. MR 221949, DOI 10.1017/s030500410004281x
Wolfram Pohlers, Subsystems of set theory and second order number theory, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, North-Holland, Amsterdam, 1998, pp. 209–335. MR 1640328, DOI 10.1016/S0049-237X(98)80019-0
Wolfram Pohlers, Proof theory, Universitext, Springer-Verlag, Berlin, 2009. The first step into impredicativity. MR 2457679
Michael Rathjen, $\omega$-models and well-ordering principles, Foundational adventures, Tributes, vol. 22, Coll. Publ., London, 2014, pp. 179–212. MR 3241960
Michael Rathjen and Pedro Francisco Valencia Vizcaíno, Well-ordering principles and bar induction, Gentzen’s centenary, Springer, Cham, 2015, pp. 533–561. MR 3443529
Michael Rathjen and Andreas Weiermann, Reverse mathematics and well-ordering principles, Computability in context, Imp. Coll. Press, London, 2011, pp. 351–370. MR 2857084, DOI 10.1142/9781848162778_{0}011
Richard A. Shore, On the strength of Fraïssé’s conjecture, Logical methods (Ithaca, NY, 1992) Progr. Comput. Sci. Appl. Logic, vol. 12, Birkhäuser Boston, Boston, MA, 1993, pp. 782–813. MR 1281172
Stephen Simpson, Bqo theory and Fraïssé’s conjecture, chapter in the book Recursive Aspects of Descriptive Set Theory by R. Mansfield and G. Weitkamp, Oxford University Press, 1985, pp. 124–138.
Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009. MR 2517689, DOI 10.1017/CBO9780511581007
Yudai Suzuki and Keita Yokoyama, On the ${\Pi }^1_2$-consequences of ${\Pi }^1_1$-$\mathsf {CA}_0$, arXiv:2402.07136, 2024.
Gaisi Takeuti, Consistency proofs of subsystems of classical analysis, Ann. of Math. (2) 86 (1967), 299–348. MR 219410, DOI 10.2307/1970691
Ian Alexander Thomson, Well-ordering principles and ${\Pi }^1_1$-comprehension $+$ bar induction, PhD thesis, University of Leeds, 2017.
Michael Rathjen and Ian Alexander Thomson, Well-ordering principles, $\omega$-models and $\Pi ^1_1$-comprehension, The legacy of Kurt Schütte, Springer, Cham, [2020] ©2020, pp. 171–215. MR 4294892, DOI 10.1007/978-3-030-49424-7_{1}2
Henry Towsner, Partial impredicativity in reverse mathematics, J. Symbolic Logic 78 (2013), no. 2, 459–488. MR 3145191, DOI 10.2178/jsl.7802070