Separating Principles Below WKL0

Original · EN

In this paper, we study Ramsey-type Konig's Lemma, written RWKL, using a technique introduced by Lerman, Solomon, and the second author. This technique uses iterated forcing to construct an omega-model satisfying one principle T₁ but not another T₂. The technique often allows one to translate a "one step" construction (building an instance of T₂ along with a collection of solutions to each computable instance of T₁) into an omega-model separation (building a computable instance of T₂ together with a Turing ideal where T₁ holds). We illustrate this translation by separating d-DNR from DNR (reproving a result of Ambos-Spies, Kjos-Hanssen, Lempp, and Slaman), and then apply this technique to separate RWKL from DNR (which has been shown separately by Bienvenu, Patey, and Schafer).