TY - JOUR

T1 - Some conservation results on weak König's lemma

AU - Simpson, Stephen G.

AU - Tanaka, Kazuyuki

AU - Yamazaki, Takeshi

N1 - Funding Information:
Keywords: RCA0; WKL0; Weak Ko$nig’s lemma; Conservation theorems; Hard core theorem; Productive functions; Forcing; Universal trees; Genericity; Pointed perfect trees ∗Corresponding author. E-mail addresses: simpson@math.psu.edu (S.G. Simpson), tanaka@math.tohoku.ac.jp (K. Tanaka), yamazaki@mi.cias.osakafu-u.ac.jp (T. Yamazaki). URL: http://www.math.psu.edu/simpson 1Simpson was partially supported by NSF grant DMS-0070718. 2Tanaka was partially supported by Grants-in-Aid for Scienti7c Research of the Ministry of Education No. 09440072. 3Yamazaki was partially supported by JSPS Research Fellowships for Young Scientists No. 0005744.

PY - 2002/12/1

Y1 - 2002/12/1

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

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

KW - Conservation theorems

KW - Forcing

KW - Genericity

KW - Hard core theorem

KW - Pointed perfect trees

KW - Productive functions

KW - RCA

KW - Universal trees

KW - Weak König's lemma

KW - WKL

UR - http://www.scopus.com/inward/record.url?scp=0036885389&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0036885389&partnerID=8YFLogxK

U2 - 10.1016/S0168-0072(01)00121-X

DO - 10.1016/S0168-0072(01)00121-X

M3 - Article

AN - SCOPUS:0036885389

SN - 0168-0072

VL - 118

SP - 87

EP - 114

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 1-2

ER -