Some conservation results on weak König's lemma

AbstractBy RCA0, we denote the system of second-order arithmetic based on recursive comprehension axioms and Σ10 induction. WKL0 is defined to be RCA0 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 RCA0, there exists a countable model M′ of WKL0 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 WKL0 proves ∀X∃!Yϕ(X,Y) with ϕ arithmetical, so does RCA0. We also discuss several improvements of this results