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 -