Searcharxiv⌕ Search

arXiv subjects

Quentin Le Houérou

Publications and source records attributed to Quentin Le Houérou.

10 recordsLinked to original sources

Partition theorems for Ketonen-Solovay largeness: Hardy-like version

We develop the framework of $α$-largeness introduced by Ketonen and Solovay, by proving a partition theorem for $α$-large sets with $α< ε_0$ which generalizes theorems from Ketonen and Solovay and from Bigorajska and Kotlarski. We also prove that for every $ω^{nk+3}$-large set $X$ with $\min X \geq 18$, every coloring $f : [X]^2 \to k$ admits an $ω^n$-large $f$-homogeneous subset. This bound is tight, up to an additive constant.

math.LO↗

The reverse mathematics of the pigeonhole hierarchy

The infinite pigeonhole principle for $k$ colors ($\mathsf{RT}^1_k$) states, for every $k$-partition $A_0 \sqcup \dots \sqcup A_{k-1} = \mathbb{N}$, the existence of an infinite subset $H \subseteq A_i$ for some~$i < k$. This seemingly trivial combinatorial principle constitutes the basis of Ramsey's theory, and plays a very important role in computability and proof theory. In this article, we study the infinite pigeonhole principle at various levels of the arithmetical hierarchy from both a computability-theoretic and reverse mathematical viewpoint. We prove that the hierarchy of pigeonhole principles induced by restricting instances to levels of the arithmetic hierarchy is strict over $\mathsf{RCA}_0$ using an elaborate iterated jump control construction, and study its first-order consequences. This is part of a large meta-mathematical program studying the computational content of combinatorial theorems.

math.LO↗

$Π^0_4$ conservation of a Carlson-Simpson lemma for 1-variable words

Carlson and Simpson proved that for every finite coloring of the 1-variable words over a finite alphabet~$A$, there is an infinite $ω$-variable word on which all the 1-variable words are monochromatic. This statement for $\ell$-colorings, written $\mathsf{CSL}^1_\ell$, is known to be strictly weaker than $\mathsf{ACA}_0$. We prove that $\mathsf{RCA}_0 + \mathsf{CSL}^1_2$ is a $\forall Π^0_4$-conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Sigma_2$. Among its consequences, it implies that neither the indivisibility of the universal triangle-free Henson graph for 2-colorings, nor the tree theorem for pairs and two colors, imply $Σ^0_2$-induction. This answers a question of Chong, Li, Wang and Yang.

math.LO↗

Ramsey-like theorems for separable permutations

We conduct a computability-theoretic study of Ramsey-like theorems of the form "Every coloring of the edges of an infinite clique admits an infinite sub-clique avoiding some pattern", with a particular focus on transitive patterns. As it turns out, the patterns corresponding to separable permutations play an important role in the computational features of the statement. We prove that the avoidance of any separable permutation is equivalent to the existence of an infinite homogeneous set in standard models, while this property fails for any other pattern. For this, we develop a novel argument for relativized diagonal non-computation.

math.LO↗

The reverse mathematics of bounded Ramsey's theorem for pairs

In this article, we study a degenerate version of Ramsey's theorem for pairs and two colors ($\mathsf{RT}^2_2$), in which the homogeneous sets for color 1 are of bounded size. By $\mathsf{RT}^2_2$, it follows that every such coloring admits an infinite homogeneous set for color 0. This statement, called $\mathsf{BRT}^2_2$, is known to be computably true, that is, every computable instance admits a computable solution, but the known proofs use $Σ^0_2$-induction ($\mathsf{I}Σ_2^0$). We prove that $\mathsf{BRT}^2_2$ follows from the Erdős-Moser theorem but not from the Ascending Descending sequence principle, and that its computably true version is equivalent to $\mathsf{I}Σ_2^0$ over $\mathsf{RCA}_0$.

math.LO↗

Conservation of Ramsey's theorem for pairs and well-foundedness

In this article, we prove that Ramsey's theorem for pairs and two colors is $Π^1_1$-conservative over~$\mathsf{RCA}_0 + \mathsf{B}Σ^0_2 + \mathsf{WF}(ε_0)$ and over~$\mathsf{RCA}_0 + \mathsf{B}Σ^0_2 + \bigcup_n \mathsf{WF}(ω^ω_n)$. These results improve theorems from Chong, Slaman and Yang and Kołodziejczyk and Yokoyama and belong to a long line of research towards the characterization of the first-order part of Ramsey's theorem for pairs.

math.LO↗

$Π^0_4$ conservation of Ramsey's theorem for pairs

In this article, we prove that Ramsey's theorem for pairs and two colors is a $\forall Π^0_4$ conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$, where a $\forall Π^0_4$ formula consists of a universal quantifier over sets followed by a $Π^0_4$ formula. The proof is an improvement of a result by Patey and Yokoyama and a step towards the resolution of the longstanding question of the first-order part of Ramsey's theorem for pairs.

math.LO↗

Ramsey-like theorems for the Schreier barrier

The family of finite subsets $s$ of the natural numbers such that $|s|=1+\min s$ is known as the Schreier barrier in combinatorics and Banach Space theory, and as the family of exactly $ω$-large sets in Logic. We formulate and prove the generalizations of Friedman's Free Set and Thin Set theorems and of Rainbow Ramsey's theorem to colorings of the Schreier barrier. We analyze the strength of these theorems from the point of view of Computability Theory and Reverse Mathematics. Surprisingly, the exactly $ω$-large counterparts of the Thin Set and Free Set theorems can code $\emptyset^{(ω)}$, while the exactly $ω$-large Rainbow Ramsey theorem does not code the halting set.

math.LO↗

Largeness notions and polytime translation for $\forall Σ^0_3$-consequences of $\mathsf{RT}^2_2$

Le Houérou, Patey and Yokoyama defined a parameterized version of $α$-largeness to prove that $\mathsf{WKL}_0 + \mathsf{RT}^2_2$ is a $\forall Σ^0_3$-conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$, where $\forall Σ^0_3$ is the universal set-closure of the class of $Σ^0_3$-formulas. We introduce a variant of this notion of largeness and obtain polynomial bounds, using a tree partition theorem based on Milliken's tree theorem. Thanks to the framework of forcing interpretation, this yields that any proof of a $\forall Σ^0_3$-sentence in the theory $\mathsf{WKL}_0 + \mathsf{RT}^2_2$ can be translated into a proof in $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$ at the cost of a polynomial increase in size.

math.LO↗

$Π^0_4$ conservation of the Ordered Variable Word theorem

A left-variable word over an alphabet~$A$ is a word over~$A \cup \{\star\}$ whose first letter is the distinguished symbol~$\star$ standing for a placeholder. The Ordered Variable Word theorem ($\mathsf{OVW}$), also known as Carlson-Simpson's theorem, is a tree partition theorem, stating that for every finite alphabet~$A$ and every finite coloring of the words over~$A$, there exists a word $c_0$ and an infinite sequence of left-variable words $w_1, w_2, \dots$ such that $\{ c_0 \cdot w_1[a_1] \cdot \dots \cdot w_k[a_k] : k \in \mathbb{N}, a_1, \dots, a_k \in A \}$ is monochromatic. In this article, we prove that $\mathsf{OVW}$ is $Π^0_4$-conservative over~$\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$. This implies in particular that $\mathsf{OVW}$ does not imply $\mathsf{ACA}_0$ over~$\mathsf{RCA}_0$. This is the first principle for which the only known separation from~$\mathsf{ACA}_0$ involves non-standard models.

math.LO↗