Some conservation results on weak Königʹs lemma Original Research Article

By View the MathML source, we denote the system of second-order arithmetic based on recursive comprehension axioms and Σ10 induction. View the MathML source is defined to be View the MathML source plus weak Königʹs lemma: every infinite tree of sequences of 0ʹs and 1ʹs has an infinite path. In this paper, we first show that for any countable model M of View the MathML source, there exists a countable model M′ of View the MathML source whose first-order part is the same as that of M, and whose second-order part consists of the M-recursive sets and sets not in the second-order part of M. By combining this fact with a certain forcing argument over universal trees, we obtain the following result (which has been called Tanakaʹs conjecture): if View the MathML source proves ∀X∃!Yϕ(X,Y) with ϕ arithmetical, so does View the MathML source. We also discuss several improvements of this results.