Controlling iterated jumps of solutions to combinatorial problems

Ludovic Patey (1, 2)

1 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
2 PI.R2 - Design, study and implementation of languages for proofs and programs

Among the Ramsey-type hierarchies, namely, Ramsey's theorem, the free set, the thin set and the rainbow Ramsey theorem, only Ramsey's theorem is known to collapse in reverse mathematics. A promising approach to show the strictness of the hierarchies would be to prove that every computable instance at level n has a lown solution. In particular, this requires to control effectively iterations of the Turing jump. In this paper, we design some variants of Mathias forcing to construct solutions to cohesive-ness, the Erd˝ os-Moser theorem and stable Ramsey's theorem for pairs, while controlling their iterated jumps. For this, we define forcing relations which, unlike Mathias forcing, have the same definitional complexity as the formulas they force. This analysis enables us to answer two questions of Wei Wang, namely, whether cohesiveness and the Erd˝ os-Moser theorem admit preservation of the arithmetic hierarchy, and can be seen as a step towards the resolution of the strictness of the Ramsey-type hierarchies.

Domaines: Logique [math.LO]

Ludovic Patey. Controlling iterated jumps of solutions to combinatorial problems. Computability, 2017, 6 (1), pp.47 - 78. ⟨10.3233/COM-160056⟩. ⟨hal-01888648⟩