Some conservation results on weak König's lemma

Stephen G. Simpson, Kazuyuki Tanaka, Takeshi Yamazaki

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


By 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.

Original languageEnglish
Pages (from-to)87-114
Number of pages28
JournalAnnals of Pure and Applied Logic
Issue number1-2
Publication statusPublished - 2002 Dec 1


  • Conservation theorems
  • Forcing
  • Genericity
  • Hard core theorem
  • Pointed perfect trees
  • Productive functions
  • RCA
  • Universal trees
  • Weak König's lemma
  • WKL


Dive into the research topics of 'Some conservation results on weak König's lemma'. Together they form a unique fingerprint.

Cite this