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

Fraïssé’s conjecture (proved by Laver) is implied by the <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Pi 1 Superscript 1"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Π</mml:mi> <mml:mn>1</mml:mn> <mml:mn>1</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Pi ^1_1</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-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 <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Pi 1 Superscript 1"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Π</mml:mi> <mml:mn>1</mml:mn> <mml:mn>1</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Pi ^1_1</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-comprehension. As part of the proof, we introduce a cofinite version of the <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Delta 2 Superscript 0"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Δ</mml:mi> <mml:mn>2</mml:mn> <mml:mn>0</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Delta ^0_2</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-Ramsey theorem, which may be of independent interest. We also relate pseudo <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Pi 1 Superscript 1"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Π</mml:mi> <mml:mn>1</mml:mn> <mml:mn>1</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Pi ^1_1</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-comprehension to principles of pseudo <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="beta"> <mml:semantics> <mml:mi>β</mml:mi> <mml:annotation encoding="application/x-tex">\beta</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-model reflection (due to Suzuki and Yokoyama) and reflection for <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="omega"> <mml:semantics> <mml:mi>ω</mml:mi> <mml:annotation encoding="application/x-tex">\omega</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-models of transfinite induction (studied by Rathjen and Valencia-Vizcaíno). In a forthcoming companion paper, we characterize pseudo <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Pi 1 Superscript 1"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Π</mml:mi> <mml:mn>1</mml:mn> <mml:mn>1</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Pi ^1_1</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-comprehension by a well-ordering principle, to get a transparent combinatorial bound for the strength of Fraïssé’s conjecture.