Some conservation results on weak König’s lemma

Stephen G. Simpson^{1}

Department of Mathematics, The Pennsylvania State University, University Park, PA 16802, USA

Kazuyuki Tanaka^{2}

Mathematical Institute, Tohoku University, Sendai, 980-8578, Japan

Takeshi Yamazaki^{3}

College of Integrated Arts and Sciences, Osaka Prefecture University, Sakai, 599-8531, Japan

Abstract

By RCA_{0}, we denote the system of second order arithmetic based on recursive comprehension axioms and Σ_{1}^{0} induction. WKL_{0} is defined to be RCA_{0} 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 RCA_{0}, there exists a countable model M′ of WKL_{0} 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 WKL_{0} proves ∀X∃!Y φ(X, Y) with φ arithmetical, so does RCA_{0}. We also discuss several improvements of this results.

Key words: RCA_{0}, WKL_{0}, weak König’s lemma, conservation theorems, hard core theorem, productive functions, forcing, universal trees, genericity, pointed perfect trees

1991 MSC: 03F35, 03B30, 03C25, 03D80

Preprint submitted to Elsevier Preprint 18 June 2001

1 Introduction

A celebrated metamathematical theorem due to L. Harrington asserts that WKL_{0} is conservative over RCA_{0} for the arithmetical (in fact, Π_{1}^{1}) sentences. In other words, if an arithmetical theorem can be obtained by some analytical methods involving the compactness argument over computable mathematics, it is already provable without it. This result can be viewed as a computable analogue of the Gödel-Kreisel theorem on set theory, which asserts that if an arithmetical sentence can be proved in ZF with the axiom of choice, it is already provable without it.

It is natural to think of extending Harrington’s conservation result to analytical sentences, since the Gödel-Kreisel theorem has been extended to the Σ_{2}^{1} (in fact, Π_{3}^{1}) sentences by J. Shoenfield. However, we can easily see that WKL_{0} is not conservative over RCA_{0} for all Σ_{1}^{1} sentences, since an instance of weak König’s lemma is Σ_{1}^{1}.

In this context, it has been conjectured by K. Tanaka [14] that if WKL_{0} proves ∀X∃!Y φ(X, Y) with φ arithmetical, so does RCA_{0}. By ∃!Xφ(X), we mean that there exists a unique X satisfying φ(X). The difficulty in solving the conjecture arises from the restricted induction of those systems. It was soon realized that Tanaka’s conjecture holds under the assumption of arithmetical induction.

Some important results concerned with this conjecture were obtained by several people. Most notably, A. M. Fernandes [3] already proved the conjecture for the sentences of the form ∀X∃!Y φ(X, Y) with φ ∈ Σ_{3}^{0}. He also showed that WKL_{0} + Σ_{2}^{0} induction is conservative over RCA_{0} + Σ_{2}^{0} induction with respect to the sentences of the same form. In a different context, U. Kohlenbach [8]

Email adresses: simpson@math.psu.edu (Stephen G. Simpson), tanaka@math.tohoku.ac.jp (Kazuyuki Tanaka), yamazaki@mi.cias.osakafu-u.ac.jp (Takeshi Yamazaki).

URL: www.math.psu.edu/simpson (Stephen G. Simpson). 1 Simpson was partially supported by NSF grant DMS-0070718. 2 Tanaka was partially supported by Grants-in-Aid for Scientific Research of the Ministry of Education No.09440072. 3 Yamazaki was partially supported by JSPS Research Fellowships for Young Scientists No.0005744.

independently obtained many results somewhat similar to ours. He works in finite type systems with weak Konig’s lemma, and investigates particular examples of unique existence theorems, e.g., the best Chebysheff approximation. It is not so easy to translate his results into our terms, but from them, we can obtain more or less a solution to the conjecture for sentences of the form ∀X∃!Y φ(X, Y) with φ ∈ Σ_{2}^{0}. Finally, Yamazaki [15] discusses variations of Tanaka’s conjecture, generalizing a result of Brown and Simpson [2].

The origin of the present paper was a defective attack on this problem by the last two authors. Subsequently, by adducing a result of Pour-El/Kripke [9], the first author completed the proof, which launched a joint study on more elaborate results and techniques reported in this paper.

Let us note an application of our main result. The fundamental theorem of algebra, which asserts that any complex polynomial of any positive degree has a unique factorization into linear terms, can be stated in the form ∀X∃!Y φ(X, Y) with φ arithmetical by using a canonical expression (i.e., the binary expansion) for the complex numbers. Most of popular proofs of the theorem use some analytical methods which can be easily formalized in WKL_{0} but not in RCA_{0}. However, by our conservation result, it can be concluded without elaborating a computable solution that the fundamental theorem of algebra (for polynomials of positive standard degrees) is already provable in RCA_{0}.

By contrast, consider the statement that any continuous real function on the closed unit interval [0, 1] has a maximum value. This sentence cannot be expressed in the form ∀X∃!Y φ(X, Y) with φ arithmetical. The point is that we can not determine arithmetically whether or not a set encodes a total continuous function in the terms of Simpson [12].

Now, we recall some basic definitions about the systems RCA_{0} and WKL_{0}. The language L_{2} of second-order arithmetic is a two-sorted language with number variables x, y, z, … and set variables X, Y, Z, … Numerical terms are built up from numerical variables and constant symbols 0, 1 by means of binary operations + and ·. Atomic formulas are s = t, s < t and s ∈ X, where s and t are numerical terms. Bounded (Σ_{0}^{0} or Π_{0}^{0}) formulas are constructed from atomic formulas by propositional connectives and bounded numerical quantifiers (∀x < t) and (∃x < t), where t does not contain x. A Σ_{n}^{0} formula is of the form ∃x_{1}∀x_{2} … x_{n}θ with θ bounded, and a Π_{n}^{0} formula is of the form ∀x_{1}∃x_{2} … x_{n}θ with θ bounded. All the Σ_{n}^{0} and Π_{n}^{0} formulas are the arithmetical (Σ_{0}^{1} or Π_{0}^{1}) formulas. A Σ_{n}^{1} formula is of the form ∃X_{1}∀X_{2} … X_{n}φ with φ arithmetical, and a Π_{n}^{1} formula is of the form ∀X_{1}∃X_{2} … X_{n}φ with φ arithmetical.

The system RCA_{0} consists of

1. the ordered semiring axioms for (ω, +, ·, 0, 1, <),

2. Δ_{1}^{0} comprehension scheme:

∀x(φ(x) ↔ ψ(x)) → ∃X∀x(x ∈ X ↔ φ(x)),

where φ(x) is Σ_{1}^{0}, ψ(x) is Π_{1}^{0}, and X does not occur freely in φ(x),

3. Σ_{1}^{0} induction scheme:

φ(0) ∧ ∀x(φ(x) → φ(x + 1)) → ∀xφ(x),

where φ(x) is a Σ_{1}^{0} formula.

Within RCA_{0}, we define 2^{<ℕ} to be the set of (codes for) finite sequences of 0’s and 1’s. A set T ⊆ 2^{<ℕ} is said to be a tree (or precisely 0-1 tree) if any initial segment of a sequence in T is also in T. We say that P ⊆ ℕ is a path through T if for each n, the sequence P [n] = ⟨χ_{P} (0), χ_{P} (1), …, χ_{P} (n − 1)⟩ belongs to T, where χ_{P} is the characteristic function of P. The axioms of WKL_{0} consists of those of RCA_{0} plus weak König’s lemma: every infinite 0-1 tree T has a path.

The interest of WKL_{0} has been well established through an ongoing program, called Reverse Mathematics. H. Friedman, S. G. Simpson and others have shown that numerous well-known theorems in different fields of mathematics are provably equivalent to WKL_{0} over RCA_{0} [12].

An L_{2}-structure M is an ordered 7-tuple (|M|, S_{M}, +_{M}, ·_{M}, 0_{M}, 1_{M}, <_{M}), where |M| serves as the range of the number variables and S_{M} is a set of subsets of |M|, that is, the range of the set variables. The first order part of M is obtained from M by removing S_{M}. If its first order part is the structure of standard natural numbers, M is called an ω-structure or an ω-model. In particular, ω-models of WKL_{0} are known as Scott systems and extensively studied by not a few people, e.g. Kaye [7].

In the next section, we use tree forcing to prove that for any countable model M of RCA_{0}, there exists a countable model M′ of WKL_{0} such that M and M′ have the same first order part and S_{M} ∩ S_{M′} is the set of M-recursive subsets of |M|. This can be regarded as a non-ω extension of Kreisel’s recursive hard core theorem, which asserts that the intersection of all ω-models of WKL_{0} is the set of recursive sets. In Section 3, we introduce universal tree forcing. In Section 4, by combining the techniques in the preceding sections, we prove our main theorem that if WKL_{0} proves ∀X∃!Y φ(X, Y) with φ arithmetical, so does RCA_{0}. In Section 5, we use a forcing argument with uniformly pointed perfect trees to prove that if WKL_{0} proves ∀X∃!Y φ(X, Y) with φ Π_{1}^{1}, then RCA_{0} proves ∀X∃Y φ(X, Y). In Section 6, we prove a stronger form of our main theorem, that is, if WKL_{0}^{+} proves ∀X∃!Y φ(X, Y) with φ arithmetical, so does RCA_{0}.

2 A non-ω hard core theorem

In this section, we first review the tree forcing argument which is originated by Jockusch/Soare [6] and used by L. Harrington for his conservation result on WKL_{0}. We then reinforce this argument with some other machinery to prove that for any countable model M of RCA_{0}, there exists a countable model M′ of WKL_{0} such that M′ has the same first order part as M and S_{M} ∩ S_{M′} is the set of M-recursive subsets of |M|. The following exposition of the tree forcing argument is based on [12, Section IX.2]. See also [12, Section VIII.2] for an account of hard core theorems.

Let M be an L_{2}-structure which satisfies the axioms of ordered semirings and Σ_{1}^{0} induction. We say that X ⊆ |M| is Δ_{1}^{0} definable over M, denoted X ∈ Δ_{1}^{0}- def(M), if there exist Σ_{1}^{0} formulas φ_{1} and φ_{2} with parameters from |M| ∪ S_{M} such that

X = {n ∈ |M| : M ⊧ φ_{1}(n)} = {n ∈ |M| : M ⊧ ¬φ_{2}(n)}.

If φ_{1} and φ_{2} have no set parameter (except A ∈ S_{M}), we say that X is Mrecursive (in A). By REC_{M} (or REC_{M}(A)), we denote the set of subsets of |M| which are M-recursive (M-recursive in A). If L_{2}-structures M and M′ have the same first order part, REC_{M} = REC_{M′}. It is also easy to see that if M is a model of RCA_{0}, Δ_{1}^{0}-def(M) = S_{M}.

Lemma 2.1 Let M be an L_{2}-structure which satisfies the axioms of ordered semirings and Σ_{1}^{0} induction. Let M′ be the L_{2}-structure with the same first order part as M and S_{M′} = Δ_{1}^{0}-def(M). Then M′ is a model of RCA_{0}.

Proof. See the proof of [12, Lemma IX.1.8]. □

We now define basic notions of the tree forcing. Let M be a countable model of RCA_{0}. Let T_{M} be the set of all T ∈ S_{M} such that M ⊧ T is an infinite 0-1 tree. For any T ∈ T_{M} and P ⊆ |M|, we say that P is a path through T if, for any n ∈ |M|, P [n] ∈ T. Here P [n] is a sequence σ ∈ (2^{n})_{M} such that for all m <_{M} n, m ∈ P if and only if M ⊧ σ(m) = 1. Let [T] be the set of paths through T. We put P_{M} = [(2^{<ℕ})_{M}]. We say that D ⊆ T_{M} is dense if, for each T ∈ T_{M}, there exists T′ ∈ D such that T′ ⊆ T. A path G is said to be T_{M}-generic if, for every M-definable dense set D ⊆ T_{M}, there exists T ∈ D such that G ∈ [T].

Lemma 2.2 Let M be a countable model of RCA_{0}. For any T ∈ T_{M}, there exists a T_{M}-generic G such that G ∈ [T].

Proof. Let ⟨D_{i} : i ∈ ω⟩ be an enumeration of all M-definable dense sets. We can easily construct a sequence of trees T_{i} (i ∈ ω) such that T_{0} = T, T_{i+1} ⊆ T_{i} and T_{i+1} ∈ D_{i} for each i ∈ ω. Then, a path G = ⋂ T_{i} is what we want. □

Lemma 2.3 Let M be a countable model of RCA_{0} and suppose that G ∈ P_{M} is T_{M}-generic. Let M′ be the L_{2}-structure such that M′ has the same first order part as M and S_{M′} = S_{M} ∪ {G}. Then, M′ ⊧ Σ_{1}^{0} induction.

Proof. It suffices to prove that for any m ∈ |M| and any Σ_{1}^{0} formula φ(x, G) with parameters from |M| ∪ S_{M′}, the set {n ∈ |M| : n <_{M} m ∧M′ ⊧ φ(n, G)} is M-finite, since Σ_{1}^{0} induction is provably equivalent to bounded Σ_{1}^{0} comprehension (cf. [12, Remark II.3.11]). Without loss of generality, we may assume that φ(x, G) is of the form ∃yθ(x, G[y]), where θ(x, τ) is Σ_{0}^{0} with parameters from |M| ∪ S_{M}. Let D_{m} be the set of all T ∈ T_{M} such that for any n <_{M} m, M satisfies either 1. ∀τ ∈ T ¬θ(n, τ), or

2. ∃w∀τ ∈ T (lh(τ) = w → ∃τ′ ⊆ τθ(n, τ′),

where lh(τ) denotes the length of sequence τ. Since we can prove that D_{m} is dense (see[12, Lemma IX.2.4], there exists T′ ∈ D_{m} such that G ∈ [T′]. Then, {n ∈ |M| : n <_{M} m ∧M′ ⊧ φ(n, G)} if and only if {n ∈ |M| : n <_{M} m ∧∃w∀τ ∈ T′(lh(τ) = w → ∃τ′ ⊆ τθ(n, τ′)}. Therefore, by Σ_{1}^{0} induction over M, {n ∈ |M| : n <_{M} m ∧M′ ⊧ φ(n, G)} is M-finite. □

Let B = ⟨B_{i} : i ∈ ω⟩ be a sequence from P_{M} = [(2^{<ℕ})_{M}]. Δ_{1}^{0}-def(M; B) is the set of all X ⊆ |M| such that there exist Σ_{0}^{0} formulas θ_{1} and θ_{2} with parameters from |M| ∪ S_{M} such that

X = {n ∈ |M| : ∀m ∈ |M|(M ⊧ θ_{1}(n, B_{1}[m], …, B_{l}[m]))}
= {n ∈ |M| : ∃m ∈ |M|(M ⊧ θ_{2}(n, B_{1}[m], …, B_{l}[m]))}

for some l ∈ ω. M[B] denotes the L_{2}-structure (|M|, Δ_{1}^{0}-def(M; B), +_{M}, ·_{M}, 0_{M}, 1_{M}, <_{M}). If B = ⟨P ⟩, then we write M[P] for M[B].

Lemma 2.4 Let M be a countable model of RCA_{0}. For any T_{M}-generic G, M[G] is a countable model of RCA_{0}.

Proof. It is obvious from Lemmas 2.1 and 2.3. □

Corollary 2.5 Let M be a countable model of RCA_{0}. For any T ∈ T_{M}, there exists a countable model M′ of RCA_{0} such that M′ has the same first part as M, S_{M} ⊆ S_{M′} and M′ ⊧ T has a path.

Proof. It is straightforward from Lemmas 2.2 and 2.4. □

Lemma 2.6 Let M be a countable model of RCA_{0}. Then there exists a countable model M′ of WKL_{0} such that M′ has the first part as M and S_{M} ⊆ S_{M′}.

Proof. Use Corollary 2.5 repeatedly. □

Theorem 2.7 (L. Harrington) For any Π_{1}^{1} sentence φ, if φ is a theorem of WKL_{0}, then φ is already a theorem of RCA_{0}. In particular, the arithmetical part of WKL_{0} is the same as that of RCA_{0}, or equivalently Σ_{1}^{0}-PA (first order Peano arithmetic with induction scheme restricted to the Σ_{1}^{0}-formulas).

Proof. It easily follows from Lemma 2.6 by the help of Gödel’s completeness theorem. □

We now recall another important characterization of models of WKL_{0}. Let M be a countable model of RCA_{0}. Let C be a countable subset of the set P (|M|) of all subsets of |M|. D ⊆ T_{M} is M ∪ C definable if there exists a formula φ with parameters from |M| ∪ S_{M} ∪ C such that for any T ∈ T_{M}, T ∈ D if and only if M′ ⊧ φ(T), where M′ = (|M|, S_{M} ∪ C, +_{M}, ·_{M}, 0_{M}, 1_{M}, <_{M}). A path G is said to be T_{M}-C-generic if, for every M ∪ C definable dense set D ⊆ T_{M}, there exists T ∈ D such that G ∈ [T]. If G is T_{M}-C-generic, then G is T_{M}-generic. The following lemma is a straightforward generalization of Lemma 2.2.

Lemma 2.8 Let M be a countable model of RCA_{0}. Let C be a countable subset of P (|M|). For any T ∈ T_{M}, there exists T_{M}-C-generic G such that G ∈ [T].

Lemma 2.9 Let M be a countable model of RCA_{0}. Suppose that C is a countable subset of P (|M|) with S_{M} ∩ C = ∅ and G is T_{M}-C-generic. Then S_{M[G]} ∩ C = ∅.

Proof. We want to prove that for any A ∈ C and any Σ_{1}^{0} formula φ_{1} and φ_{2} with parameters from |M| ∪ S_{M} ∪ {G},

A ≠ {n ∈ |M| : M[G] ⊧ φ_{1}(n, G)} or A ≠ {n ∈ |M| : M[G] ⊧ ¬φ_{2}(n, G)}.

So fix any A ∈ C. Suppose that φ_{i}(x, G) is of the form ∃yθ_{i}(x, G[y]) where θ_{i}(x, τ) is Σ_{0}^{0} with parameters from |M| ∪ S_{M}, for i = 0, 1. Then let D_{A} be the set of all T ∈ T_{M} such that one of the followings holds for some m ∈ |M|:

A1. m ∈ A ∧ M ⊧ ∀τ ∈ T ¬θ_{1}(m, τ),

A2. m ∉ A ∧ M ⊧ ∃w∀τ ∈ T (lh(τ) = w → ∃τ′ ⊆ τθ_{1}(m, τ′)),

A3. m ∈ A ∧ M ⊧ ∃w∀τ ∈ T (lh(τ) = w → ∃τ′ ⊆ τθ_{2}(m, τ′)),

A4. m ∉ A ∧ M ⊧ ∀τ ∈ T ¬θ_{2}(m, τ).

We show that D_{A} is dense. Then, there exists an M-tree in D_{A} such that G is a path through it. Hence, by the definition of D_{A}, the proof is completed.

To see that D_{A} is dense, let T ∈ T_{M} be given. We first claim that there exists P ∈ [T] such that A ≠ {n ∈ |M| : M[P] ⊧ φ_{1}(n, P)} or A ≠ {n ∈ |M| : M[P] ⊧ ¬φ_{2}(n, P)}. By way of contradiction, deny the claim. By Lemma 2.6, we can construct a countable model M′ of WKL_{0} such that M′ has the same first order part as M and S_{M} ⊆ S_{M′}. Then,

n ∈ A ⇔ M′ ⊧ ∀Z(Z is a path through T → φ_{1}(n, Z)).

Since “Z is a path through T ” is expressed as a Π_{1}^{0} formula, “Z is a path through T → φ_{1}(n, Z)” is Σ_{1}^{0}, and so the whole formula ∀Z(Z is a path through T → φ_{1}(n, Z)) is logically equivalent in M′ to a Σ_{1}^{0} formula φ′_{1}(n) with parameters from |M| ∪ S_{M} by virtue of compactness of the Cantor space (cf. [12, Lemma V.III.2.4]). Since for any n ∈ |M|, M′ ⊧ φ′(n) if and only if M ⊧ φ′(n), we finally have n ∈ A ⇔ M ⊧ φ′(n). Similarly, we have n ∈ A ⇔ M′ ⊧ ∃Z(Z is a path through T ∧ ¬φ_{2}(n, Z))}, and so by compactness, there exists a Π_{1}^{0} formula ψ′(x) with parameters from |M| ∪ S_{M} such that n ∈ A ⇔ M ⊧ ψ′(n) for all N ∈ |M|. Therefore, A is in S_{M} since M is a model of RCA_{0}. This contradicts with our assumption. Thus the claim is proved.

By the above claim, there exist P ∈ [T] and m ∈ |M| such that one of the following conditions holds:

B1. m ∈ A ∧ M[P] ⊧ ∀y¬θ_{1}(m, P [y]),

B2. m ∉ A ∧ M[P] ⊧ ∃yθ_{1}(m, P [y]),

B3. m ∈ A ∧ M[P] ⊧ ∃yθ_{2}(m, P [y]),

B4. m ∉ A ∧ M[P] ⊧ ∀y¬θ_{2}(m, Z[y]).

First suppose that condition B1 holds. Let T′ = {τ ∈ T : ∀τ′ ⊆ τ¬θ_{1}(m, τ′)}. Then, T′ ∈ T_{M}. It is also clear that A1 holds with T′ (instead of T). Thus T′ ∈ D_{A}. Next suppose that condition B2 holds. Take σ ∈ (2^{<ℕ})_{M} with σ = P [lh(σ)] and θ_{1}(m, σ). Set T′ = {τ ∈ T : τ is compatible with σ}. T′ clearly satisfies A2, hence T′ ∈ D_{A}. The other two cases can be treated similarly. Hence, in any case, there exists a subtree T′ of T such that T′ ∈ D_{A}, which means that D_{A} is dense. □

Corollary 2.10 Let M be a countable model of RCA_{0}. Let C a countable subset of P (|M|) such that S_{M} ∩ C = ∅. For any T ∈ T_{M}, there exists a countable model M′ of RCA_{0} such that the following four conditions hold:

(1) M′ has the same first part as M,

(2) S_{M} ⊆ S_{M′},

(3) S_{M′} ∩ C = ∅,

(4) M′ ⊧ T has a path.

Proof. It is straightforward from Lemmas 2.4, 2.8 and 2.9. □

Lemma 2.11 Let M be a countable model of RCA_{0}, and C a countable subset of P (|M|) such that S_{M} ∩ C = ∅. Then there exists a countable model M′ of WKL_{0} such that M′ has the same first order part as M, S_{M} ⊆ S_{M′} and S_{M′} ∩ C = ∅.

Proof. Use Corollary 2.10 repeatedly. □

The next theorem is a generalized version of Kreisel’s hard core theorem.

Theorem 2.12 Let M be a countable model of RCA_{0}. Then there exists a countable model M′ of WKL_{0} such that M′ has the same first order part as M and S_{M} ∩ S_{M′} = REC_{M}.

Proof. Let M be a countable model of RCA_{0}. Then (|M|, REC_{M}, +_{M}, ·_{M}, 0_{M} 1_{M}, <_{M}) is a countable model of RCA_{0}. Set C = S_{M} \REC_{M}. By Lemma 2.11, there exists a countable model M′ of WKL_{0} such that M′ has the same first order part as M, S′ ⊆ S_{M′} and S_{M′} ∩ C = ∅. That is, S_{M} ∩ S_{M′} = REC_{M}. □

Corollary 2.13 Let N be a countable model of Σ_{1}^{0}-PA. Then there exist uncountably many countable models M of WKL_{0} such that N is the first order part of M.

Proof. Suppose that A = {M : M is a countable model of WKL_{0} with the first order part N} is countable. Let C be the set (∪{S_{M} : M ∈ A}) \ REC_{M_{0}}, where M_{0} = (|N|, ∅, +_{N}, ·_{N}, 0_{N}, 1_{N}, <_{N}). By Lemma 2.11, we obtain another model M′ of WKL_{0} such that N is the first order part of M′ and S_{M′} ∩ C = ∅. This is a contradiction. □

3 Forcing with universal trees

In this section, we introduce the notion of M-universal trees and prove that all M-universal trees are homeomorphic to one another over M, where M is a countable model of RCA_{0}. Then, we show that all M-universal trees weakly force the same L_{2}(|M| ∪ S_{M})-sentences.

Definition 3.1 Let M be a countable model of RCA_{0}. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {G}). For any T ∈ T_{M}, φ is said to be weakly forced by T (denoted T ⊩ φ) if M[G] ⊧ φ for all T_{M}-generic G ∈ [T].

Lemma 3.2 Let M be a countable model of RCA_{0}. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {G}). Then we have

(1) T ⊩ φ is definable over M. Indeed, there exists an L_{2}-formula φ′ such that T ⊩ φ(n_{1}, …, n_{k}, A_{1}, … A_{l}) if and only if M ⊧ φ′(n_{1}, …, n_{k}, A_{1}, … A_{l}, T), where n_{1}, … n_{k} are from |M| and A_{1}, … A_{l} from S_{M}.

(2) For any T_{M}-generic G ∈ [T], if M[G] ⊧ φ then there exists T′ ∈ T_{M} such that T′ ⊆ T, G ∈ [T′] and T′ ⊩ φ.

Proof. We need to prove (1) and (2) of Lemma 3.2 simultaneously by induction on φ. However, we here only show (1) since (2) can be treated in an obvious way.

Case 1: Suppose that φ is atomic. When φ is t ∈ G, T ⊩ φ if and only if

M ⊧ ∃m(∀σ ∈ T (lh(σ) = m → σ(t) = 1)).

For other atomic φ, T ⊩ φ if and only if M ⊧ φ. Thus T ⊩ φ is definable over M.

Case 2: Suppose that φ ≡ ¬ψ. We clearly have ∀T′ ∈ T_{M}(T′ ⊆ T → T′ ⊮ ψ) if T ⊩ φ. Conversely, assume that T ⊮ φ. Then, there exists G ∈ [T] such that M[G] ⊧ ψ. By the induction hypothesis of (2), there exists T′ ∈ T_{M} such that T′ ⊆ T, G ∈ [T′] and T′ ⊩ ψ. Thus, T ⊩ φ if and only if ∀T′ ∈ T_{M}(T′ ⊆ T → T′ ⊮ ψ). Therefore, T ⊩ φ is definable.

Case 3: Suppose that φ ≡ (ψ_{1} ∧ψ_{2}). Then, T ⊩ φ if and only if T ⊩ ψ_{1} ∧ T ⊩ ψ_{2}. So T ⊩ φ is definable.

Case 4: Suppose that φ ≡ ∃xψ(x). We show that

T ⊩ φ ⇔ ∀T′ ∈ T_{M}(T′ ⊆ T → ∃T′′ ∈ T_{M}∃n ∈ |M|(T′′ ⊆ T′ ∧ T′′ ⊩ ψ(n))).

First assume that the right hand side. Let D = {T′ ∈ T_{M} : ∃n ∈ |M|(T′ ⊩ ψ(n)) or [T] ∩ [T′] = ∅}. Then it is easy to see that D is dense. Fix any T_{M}- generic path G through T. Since D is dense, there exists T′ such that G ∈ [T′] and T′ ⊩ ψ(n) for some n ∈ |M|. Therefore M[G] ⊩ φ, and hence T ⊩ φ.

Conversely, assume that T ⊩ φ. Fix any T′ ∈ T_{M} with T′ ⊆ T. Let G be a generic path through T′. Then M[G] ⊩ φ. Therefore, M[G] ⊩ ψ(n) for some n ∈ |M|. By the induction hypothesis of (2), there exists T′′ ∈ T_{M} such that T′′ ⊆ T′ and T′′ ⊩ ψ(n).

Case 5: Suppose that φ ≡ ∃Xψ(X). Let Y be a triple ⟨A, ψ_{1}, ψ_{2}⟩ where A ∈ S_{M} and, ψ_{1} and ψ_{2} are (codes for) Σ_{1}^{0} and Π_{1}^{0} formulas with parameters from |M| ∪ {A, G}. Let T r_{Σ_{1}^{0}} and T r_{Π_{1}^{0}} be appropriate universal lightface formulas. Name(Y) is defined to be ∀x(T r_{Σ_{1}^{0}}(ψ_{1}, x, A, G) ↔ T r_{Π_{1}^{0}}(ψ_{2}, x, A, G)). For any T′ ∈ T_{M} and any T_{M}-generic G ∈ [T′], if T′ ⊩ Name(Y), then {n ∈ |M| : M[G] ⊧ T r_{Σ_{1}^{0}}(ψ_{1}, n, A, G)} ∈ S_{M[G]}. Conversely, for any Z ∈ S_{M[G]}, there exists a triple W = ⟨B, ψ′_{1}, ψ′_{2}⟩ such that M[G] ⊧ Name(W) and Z = {n ∈ |M| : M[G] ⊧ T r_{Σ_{1}^{0}}(ψ′_{1}, n, B, G)} ∈ S_{M[G]}.

By ψ(Y), we denote the formula obtained from ψ(X) by replacing t ∈ X with T r_{Σ_{1}^{0}}(ψ_{1}, t, A, G). Then, by the same way as Case 4, we can prove that T ⊩ φ if and only if ∀T′ ∈ T_{M}(T′ ⊆ T → ∃T′′ ∈ T_{M}(T′′ ⊆ T′ ∧ ∃Y (T′′ ⊩ Name(Y) ∧ ψ(Y)))) □

Let B(X) be the set of Boolean expressions built from atoms in X by means of the usual set operations ∪, ∩ and ^{c}. For σ ∈ (2^{<ℕ})_{M}, let [σ] = {P ∈ P_{M} : P [lh(σ)] = σ}. Then for any expression b ∈ B((2^{<ℕ})_{M}), [b] is defined to be the subset of P_{M} which b denotes in the obvious way. For simplicity, we often write B for B((2^{<ℕ})_{M}).

For any two T, T′ ∈ T_{M}, a mapping F from [T] to [T′] is said to be Mcontinuous or simply continuous if S_{M} contains a function f : B → B (called a code for F) such that for any b ∈ B,

[f(b)] ∩ [T] = F^{−1}([b] ∩ [T′]).

Then, we can easily see that F (P) ∈ Δ_{1}^{0}-def(M; P).

Definition 3.3 Let M be a countable model of RCA_{0}. A tree T ∈ T_{M} is said to be (M-)universal if for any T′ ∈ T_{M}, there exists an M-continuous F from [T] to [T′].

Obviously, any subtree of a universal tree is also universal, whenever it belongs to T_{M}. In the rest of this section, we only treat a countable model M of RCA_{0} such that S_{M} = REC_{M}(A) for some A. Such a model M is said to be principal with a generator A.

Lemma 3.4 Let M be a principal model of RCA_{0}. Then the following hold:

(1) There exists an M-universal tree.

(2) If T is a universal tree, then for any T′ ∈ T_{M}, there exists an M-continuous function F from [T] onto [T′].

(3) If T and T′ are universal trees, then there exists an M-homeomorphism F from [T] to [T′].

Proof. Let M be a principal model of RCA_{0} with a generator A. For any n ∈ |M| and i = 0, 1, let b_{n}^{i} be a Boolean expression ⋃{τ : τ(n) = i ∧ lh(τ) = n+1}. Then, [T] ⊆ [b_{n}^{i}] if and only if every P ∈ [T] satisfies P (n) = i, i = 0, 1.

Since M is principal, there exists a universal Σ_{1}^{0} formula φ_{Σ}(e, x) with parameters from |M| ∪ S_{M}. Then, we say that g : |M| × |M| → |M| is a productive function for T if for any e and d ∈ |M|, supposing that (∀n ∈ M([T] ⊆ [b_{n}^{1}] → φ_{Σ}(e, n)), ∀n ∈ M([T] ⊆ [b_{n}^{0}] → φ_{Σ}(d, n)) and ¬∃x(φ_{Σ}(e, x) ∧ φ_{Σ}(d, x)), we have

¬(φ_{Σ}(e, g(e, d)) ∨ φ_{Σ}(d, g(e, d))).

Claim 1 There exists a tree T ∈ T_{M} which has a productive function in S_{M}.

Proof. For any consistent first-order theory Γ, let T_{Γ} be an infinite tree such that [T_{Γ}] = the set of the characteristic functions of consistent, complete extensions of Γ which is closed under logical consequence. It is known that for any T ∈ T_{M}, there exists a first-order theory Γ_{T} such that there exists an M-homeomorphism function from [T_{Γ_{T}}] to [T]. (See [12, Section IV.3.2] for details.)

For any X ∈ S_{M}, let Q_{X} be an L_{1}(R)-theory whose axioms consist of Robinson arithmetic Q plus {R(n) : n ∈ X} ∪ {¬R(n) : n ∉ X} with a new unary relation symbol R. Then Q_{X} is consistent since it has a weak model [12, Theorem II.8.4].

We show that T_{Q_{A}} has a productive function in S_{M} where A is a generator of M. Assume that ¬∃x(φ_{Σ}(e, x) ∧ φ_{Σ}(d, x)). We can effectively find an L_{1}(R)- formula Φ_{e,d} with only one free variable such that

φ_{Σ}(e, n) → Q_{A} ⊢ Φ_{e,d}(n̄), φ_{Σ}(d, n) → Q_{A} ⊢ ¬Φ_{e,d}(n̄),

where n̄ is the numeral for n (cf. Theorem III.1.23 [5]). By a diagonal argument [5, pp. 158], we can also effectively find an L_{1}(R)-sentence ψ such that Q_{A} ⊢ ψ_{e,d} ↔ ¬Φ_{e,d}(\underline{⌈ψ_{e,d}⌉}), where ⌈ψ_{e,d}⌉ is the Gödel number of ψ_{e,d}. Let g be a function such that g(e, d) = ⌈ψ_{e,d}⌉. Then g is a productive function for T_{Q_{A}} [10, pp. 94]. □

Let f be a function from |M| to B. Then we can extend f to f′ : B → B such that for each σ ∈ (2^{<ℕ})_{M},

f′(σ) = ⋂_{i<lh(σ),σ(i)=1} f(i) ∩ ⋂_{j<lh(σ),σ(j)=0} f(j)^{c},

and that f′ preserves Boolean operations. For simplicity, we also write f for f′.

Claim 2 Assume that T ∈ T_{M} has a productive function in S_{M}. Then, for any T′ ∈ T_{M}, there exists an M-continuous function F from [T] onto [T′].

Proof. Our proof is inspired with an argument due to Pour-El/Kripke [9, the proof of Lemma 1].

Assume that T ∈ T_{M} has a productive function g in S_{M}. Fix any T′ ∈ T_{M}. To construct an M-continuous function F from [T] onto [T′], it suffices to show that there exists an f : |M| → B in S_{M} such that for any b ∈ B,

[T] ∩ [f(b)] ≠ ∅ ⇔ [T′] ∩ [b] ≠ ∅. For, letting F (P) be a unique P′ ∈ [T′] such that P′ ∈ ⋂_{n∈M} f(P [n]), F is an M-continuous function from [T] onto [T′] with code f.

Let ψ_{1}(a, u, v, x, y) be a Σ_{1}^{0} formula saying that [T] ∩ [v] ⊆ [b_{x}^{0}] or [T′] ∩ [u] ⊆ [b_{a}^{1}] ∧ x = g((y)_{0}, (y)_{1}). Similarly, let ψ_{2}(a, u, v, x, y) mean that [T] ∩ [v] ⊆ [b_{x}^{1}] or [T′] ∩ [u] ⊆ [b_{a}^{0}]∧ x = g((y)_{0}, (y)_{1}). By the recursion theorem, there exist two functions t_{1} and t_{2} in S_{M} such that

∀x(φ_{Σ}(t_{1}(a, u, v), x) ↔ ψ_{1}(a, u, v, x, ⟨t_{1}(a, u, v), t_{2}(a, u, v)⟩)) and,
∀x(φ_{Σ}(t_{2}(a, u, v), x) ↔ ψ_{2}(a, u, v, x, ⟨t_{1}(a, u, v), t_{2}(a, u, v)⟩)).

Finally, put k(a, u, v) = g(t_{1}(a, u, v), t_{2}(a, u, v)).

Assuming that for any l <_{M} n, f(l) is defined, let f(n) = ⋃_{σ∈(2^{n})_{M}} (f(σ) ∩ b_{k(n,σ,f(σ))}^{1}). Then, it is obvious that f ∈ S_{M}. We now want to show that

(1) ∀b ∈ B([T] ∩ [f(b)] ≠ ∅ ⇔ [T′] ∩ [b] ≠ ∅).

Let φ(n) be a Σ_{0}^{0}(Σ_{1}^{0}) formula which means that ∀σ ∈ 2^{n}(([T] ∩ [f(σ)] ≠ ∅ ↔ [T′] ∩ [σ] ≠ ∅)). Then, it suffices to show that M ⊧ ∀nφ(n). Obviously, M ⊧ φ(0). Suppose that M ⊧ φ(n). Then, we will show that M ⊧ φ(n + 1) holds, that is, for any σ ∈ (2^{n})_{M},

[T] ∩ [f(σ)] ∩ [f(n)] ≠ ∅ ⇔ [T′] ∩ [σ] ∩ [b_{n}^{1}] ≠ ∅

and

[T] ∩ [f(σ)] ∩ [f(n)]^{c} ≠ ∅ ⇔ [T′] ∩ [σ] ∩ [b_{n}^{0}] ≠ ∅.

We may suppose that [T′] ∩ [σ] ≠ ∅. By the hypothesis, [T] ∩ [f(σ)] ≠ ∅. We first prove that [T′] ∩ [σ] ∩ [b_{n}^{1}] = ∅ ⇒ [T_{1}] ∩ [f(σ)] ∩ [f(n)] = ∅. Suppose that [T′] ∩ [σ] ∩ [b_{n}^{1}] = ∅. By the construction of k, M satisfies

(2) ∀x(φ_{Σ}(t_{2}(n, σ, f(σ)), x) ↔ (x = k(n, σ, f(σ)) ∨ [T] ∩ [f(σ)] ⊆ [b_{x}^{1}]))

and

(3) ∀x(φ_{Σ}(t_{1}(n, σ, f(σ)), x) ↔ [T] ∩ [f(σ)] ⊆ [b_{x}^{0}]).

By way of contradiction, we assume that [T] ∩ [f(σ)] ∩ [f(n)] ≠ ∅. Then,

[T] ∩ [f(σ)] ∩ [b_{k(n,σ,f(σ))}^{1}] ≠ ∅ since f(n) = [f(σ)] ∩ [b_{k(n,σ,f(σ))}^{1}]. Therefore,

¬∃x(φ_{Σ}(t_{1}(n, σ, f(σ)), x) ∧ φ_{Σ}(t_{2}(n, σ, f(σ)), x).

Since g is a productive function for T,

¬φ_{Σ}(t_{2}(n, σ, f(σ)), k(n, σ, f(σ))).

This contradicts with (2). Therefore, [T′]∩[σ]∩[b_{n}^{1}] = ∅ ⇒ [T]∩[f(σ)]∩[f(n)] = ∅. In a similar manner, we can prove that

[T′] ∩ [σ] ∩ [b_{n}^{0}] = ∅ ⇒ [T] ∩ [f(σ)] ∩ [f(n)]^{c} = ∅

and

[T′] ∩ [σ] ∩ [b_{n}^{1}] ≠ ∅ ∧ [T′] ∩ [σ] ∩ [b_{n}^{0}] ≠ ∅ ⇒
[T] ∩ [f(σ)] ∩ [f(n)] ≠ ∅ ∧ [T] ∩ [f(σ)] ∩ [f(n)]^{c} ≠ ∅.

Thus, M ⊧ φ(n + 1). By Σ_{0}^{0}(Σ_{1}^{0})-induction, then (1) holds. The proof is completed. □

Claim 3 Let M be a countable model of RCA_{0}. Suppose that both T and T′ have productive functions in S_{M}. Then there exists an M-homeomorphism H from [T] to [T′].

Proof. The proof is an obvious modification of the proof of Claim 2. (Cf. [9, the proof of Lemma 2].) Suppose that both T and T′ have productive functions in S. To construct a homeomorphism H from [T] to [T′], it suffices to show that there exist two functions h_{1} and h_{2} from M to B such that for any b, b′ ∈ B,

[T] ∩ [b′] ∩ [h_{1}(b)] ≠ ∅ if and only if [T′] ∩ [h_{2}(b′)] ∩ [b] ≠ ∅.

For, letting H(P) be a unique P′ ∈ [T′] such that P′ ∈ ⋂_{n∈M} h_{1}(P [n]), H is an M-homeomorphism from [T] to [T′] with code h_{1} and H^{−1} has a code h_{2}.

We construct h_{1} and h_{2} as follows. Assume that we have already defined h_{1}(l) and h_{2}(l) for any l <_{M} n. Then for any b, b′ ∈ B({σ : lh(σ) ≤ n}),

[T] ∩ [b′] ∩ [h_{1}(b)] ≠ ∅ if and only if [T′] ∩ [h_{2}(b′)] ∩ [b] ≠ ∅.

As the proof of Claim 2, we can define h_{1}(n) such that for any b ∈ B({σ : lh(σ) ≤ n + 1}) and b′ ∈ B, [T] ∩ [b′] ∩ [h_{1}(b)] ≠ ∅ if and only if [T′] ∩ [h_{2}(b′)] ∩ [b] ≠ ∅. In a similar way, we can find h_{2}(n) such that for any b, b′ ∈ B({σ : lh(σ) ≤ n + 1}), [T] ∩ [b′] ∩ [h_{1}(b)] ≠ ∅ if and only if [T′] ∩ [h_{2}(b′)] ∩ [b] ≠ ∅. The proof is completed. □

Claim 4 Assume that T has a productive function in S_{M} and there exists an M-continuous function F from [T′] to [T]. Then [T′] is M-homeomorphic to [T′′] for some T′′ which has a productive function in S_{M}.

Proof. Our proof is just a formalization of a well-known fact on effectively inseparable sets (cf. [9, Lemma 3]). Let f be a code for F. Then, we have

[T] ⊆ [b_{n}^{i}] ⇒ [T′] ⊆ [f(b_{n}^{i})], i = 0, 1.

Let Γ be a propositional theory {⋁{⋀{a_{i}^{τ(i)} : i <_{M} n} : τ ∈ T′, lh(τ) = n} : n ∈ |M|}, where a_{i}’s are atoms, and we set a_{i}^{1} = a_{i} and a_{i}^{0} = ¬a_{i}. Let β be the natural interpretation of B into propositional formulas such that β(b_{n}^{1}) = a_{n} for all n ∈ |M|. Then,

[T] ⊆ [b_{n}^{i}] ⇒ [T_{Γ}] ⊆ [b_{β(f(b_{n}^{1}))}^{i}], i = 0, 1.

By the S_{n}^{m}-theorem, there exists a function t in S_{M} such that

∀x(φ_{Σ}(t(e), x) ↔ φ_{Σ}(e, β(f(x)))).

Let h(e, d) = β(f(b_{g(t(e),t(d)}^{1})). Then h is a productive function for T_{Γ}, which is M-homeomorphic to T′. □

Claim 5 T ∈ T_{M} is universal if and only if [T] is M-homeomorphic to [T′] for some T′ which has a productive function in S_{M}.

Proof. It follows from Claims 2 and 4. □

It is straightforward from the above five claims to obtain (1) through (3) of Lemma 3.4. □

Lemma 3.5 Let M be a principal model of RCA_{0}. If T_{1} and T_{2} are Muniversal trees, then T_{1} ⊩ φ if and only if T_{2} ⊩ φ for any sentence φ in L_{2}(|M| ∪ S_{M}).

Proof. Let T_{1} and T_{2} be universal trees. Let H be an M-homeomorphism from [T_{1}] to [T_{2}]. It is enough to show that for any sentence φ of L_{2}(|M| ∪ S_{M}), if T_{2} ⊩ φ then T_{1} ⊩_{1} φ. Assume that T_{2} ⊩ φ. Fix any T_{M}-generic G with G ∈ [T_{1}]. Since an M-homeomorphism preserves the genericity, H(G) is a T_{M}-generic path through T_{2}. Then S[H(G)] ⊧ φ. Since S[H(G)] = S[G], S[G] ⊧ φ. Then T_{1} ⊩ φ. □

Fix a universal tree U. ℙ_{1,M}^{U} be the set of all T ∈ T_{M} such that T ⊆ U. We always omit U unless there is a possibility of misunderstanding. G is said to be ℙ_{1,M}-generic if for any M-definable ℙ_{1,M}-dense set D, there exists T ∈ D such that G ∈ [T]. G is ℙ_{1,M}-generic if and only if G is T_{M}-generic with G ∈ [U]. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {G}). For any T ∈ ℙ_{1,M}, φ is said to be weakly forced by T (denoted T ⊩_{1} φ) if M[G] ⊧ φ for all ℙ_{1,M}-generic G with G ∈ [T]. That is, for any T ∈ ℙ_{1,M}, T ⊩_{1} φ if and only if T ⊩ φ. We write ⊩_{1} φ if T ⊩_{1} φ for all T ∈ ℙ_{1,M}.

Lemma 3.6 Let M be a principal model of RCA_{0}. Let φ be an L_{2}(|M| ∪ S_{M})- sentence. If G is ℙ_{1,M}-generic, then M[G] ⊧ φ if and only if ⊩_{1} φ.

Proof. Assume that M[G] ⊧ φ. Then there exists T ∈ ℙ_{1,M} such that G ∈ [T] and T ⊩_{1} φ. By Lemma 3.5, T′ ⊩ φ for any T′ ∈ ℙ_{1,M}. □

Corollary 3.7 Let M be a principal model of RCA_{0}. If G and H are ℙ_{1,M}- generic, then M[G] and M[H] satisfy the same L_{2}(|M| ∪ S_{M})-sentences.

Proof. It is straightforward from Lemma 3.6. □

Let C be a countable subset of P (|M|). G is said to be ℙ_{1,M}-C-generic if, for every ℙ_{1,M}-dense, M ∪ C-definable set D, there exists T ∈ D such that G ∈ [T].

Lemma 3.8 Let M be a countable model of RCA_{0}. Let C be a countable subset of P (|M|) such that S_{M} ∩ C = ∅. If G is ℙ_{1,M}-C-generic, then M[G] is a countable model of RCA_{0} with S_{M[G]} ∩ C = ∅.

Proof. Immediate from Lemma 2.9. □

4 A main result

We use iterated forcing to prove our main theorem that if WKL_{0} proves ∀X∃!Y φ(X, Y) with φ arithmetical, so does RCA_{0}. We first define the 2-forcing notion ⊩_{2}. Let M be a principal model of RCA_{0}. A 2-condition is defined to be a pair ⟨T_{1}, T_{2}⟩ such that T_{1} ∈ ℙ_{1,M} and T_{1} ⊩_{1} (Name(T_{2}) and T_{2} ∈ ℙ_{1,M[G_{1}]}). ⟨T_{1}, T_{2}⟩ ≤_{2} ⟨T′_{1}, T′_{2}⟩ if T_{1} ⊆ T′_{1} and T_{1} ⊩_{1} T_{2} ⊆ T′_{2}. Let ℙ_{2,M} be the set of 2-conditions. D ⊆ ℙ_{2,M} is ℙ_{2,M}-dense if, for each P ∈ ℙ_{2,M}, there exists P′ ∈ D such that P′ ≤_{2} P. Let G be a generic filter of ℙ_{2,M}, i.e., a filter such that for all definable ℙ_{2,M}-dense set D, G ∩ D ≠ ∅. Then, G_{1} = ⋂{T_{1} : ⟨T_{1}, T_{2}⟩ ∈ G for some T_{2}} is ℙ_{1,M}-generic. Moreover, G_{2} = ⋂{i_{G_{1}}(T_{2}) : ⟨T_{1}, T_{2}⟩ ∈ G for some T_{1} with G_{1} ∈ [T_{1}]} is ℙ_{1,M[G_{1}]}-generic. Here i_{G_{1}}(Y) = {n ∈ |M| : ∃T′ ∈ ℙ_{1,M}(G_{1} ∈ [T′] ∧ T′ ⊩ ψ_{1}(n)}, i.e., the evaluation of name Y = ⟨X, φ_{1}, φ_{2}⟩. Then, we regard G as a pair ⟨G_{1}, G_{2}⟩ and call it ℙ_{2,M}-generic. For any ℙ_{2,M}-generic G = ⟨G_{1}, G_{2}⟩ and any 2-condition P = ⟨T_{1}, T_{2}⟩, G ∈ [P] means that G_{j} ∈ [T_{j}] for j = 1, 2.

Definition 4.1 Let M be a principal model of RCA_{0}. Let φ be a sentence of L_{2}(|M| ∪ S_{M} ∪ {G_{1}, G_{2}}). For any P ∈ ℙ_{2,M}, φ is said to be weakly forced by P (denoted P ⊩_{2} φ) if M[G] ⊧ φ for all ℙ_{2,M}-generic G ∈ [P].

The next lemma can be proved in a standard way (cf. Lemma 3.2).

Lemma 4.2 Let M be a principal model of RCA_{0}. Let φ be a sentence of L_{2}(|M| ∪ S_{M} ∪ {G_{1}, G_{2}}). Then we have

(1) P ⊩_{2} φ is definable over M.

(2) For any ℙ_{2,M}-generic G ∈ [P], if M[G] ⊧ φ then there exists P′ ∈ ℙ_{2,M} such that P′ ≤_{2} P, G ∈ [P′] and P′ ⊩_{2} φ.

Lemma 4.3 Let M be a principal model of RCA_{0}. For G = ⟨G_{1}, G_{2}⟩ ∈ P_{M} × P_{M}, G is ℙ_{2,M}-generic if and only if G_{1} is ℙ_{1,M}-generic and G_{2} is ℙ_{1,M[G_{1}]}- generic.

Proof. Assume that G_{1} is ℙ_{1,M}-generic and G_{2} is ℙ_{1,M[G_{1}]}-generic. Set

G = {⟨T_{1}, T_{2}⟩ : G_{1} ∈ [T_{1}], G_{2} ∈ [i_{G_{1}}(T_{2})]}.

Then, it is easy to see that G is generic filter of ℙ_{2,M} with G = ⟨G_{1}, G_{2}⟩. So G is ℙ_{2,M}-generic. □

Corollary 4.4 Let M be a principal model of RCA_{0}. Let φ be a sentence of L_{2}(|M| ∪ S_{M} ∪ {G_{1}, G_{2}}). Then, for any ⟨T_{1}, T_{2}⟩ ∈ ℙ_{2,M}, ⟨T_{1}, T_{2}⟩ ⊩_{2} φ if and only if T_{1} ⊩_{1} T_{2} ⊩_{1} φ.

Proof. Immediate from Lemma 4.3. □

Lemma 4.5 Let M be a principal model of RCA_{0}. Let φ be an L_{2}(|M| ∪ S_{M})- sentence. If P and P′ are two 2-conditions, then P ⊩_{2} φ if and only if P′ ⊩_{2} φ.

Proof. Let P = ⟨T_{1}, T_{2}⟩ and P′ = ⟨T′_{1}, T′_{2}⟩ be 2-conditions. Suppose that P′ ⊩_{2} φ. We shall show P ⊩_{2} φ. To see this, let G = ⟨G_{1}, G_{2}⟩ ∈ [P] be ℙ_{2,M}- generic. Since T_{1} and T′_{1} are M-universal, there exists an M-homeomorphism H_{1} : [T_{1}] → [T′_{1}]. Then, M[G_{1}] = M[H_{1}(G_{1})]. Therefore, i_{G_{1}}(T_{2}) is M[H_{1}(G_{1})]- universal. Similarly, there exists an M[H_{1}(G_{1})]-homeomorphism H_{2} : [i_{G_{1}}(T_{2})] → [i_{H_{1}(G_{1})}(T_{2})]. Then, we have

M[⟨G_{1}, G_{2}⟩] = M[⟨H_{1}(G_{1}), H_{2}(G_{2})⟩] ⊧ φ,

since H(G) = ⟨H_{1}(G_{1}), H_{2}(G_{2})⟩ is ℙ_{2,M}-generic with H(G) ∈ [P′]. Thus, P ⊩_{2} φ. The other direction can be proved in the same way. □

Lemma 4.6 Let M be a principal model of RCA_{0}. Let φ be an L_{2}(|M| ∪ S_{M})- sentence. If G is ℙ_{2,M}-generic, then M[G] ⊧ φ is equivalent to ⊩_{2} φ, i.e., P ⊩_{2} φ for all P ∈ ℙ_{2,M}.

Proof. Suppose that G is ℙ_{2,M}-generic and M[G] ⊧ φ. Since M[G] ⊧ φ, there exists P ⊩_{2} φ. By Lemma 4.5, for any P′ ∈ ℙ_{2,M}, P′ ⊩_{2} φ. □

Lemma 4.7 Let M be a principal model of RCA_{0}. Let φ be an L_{2}(|M| ∪ S_{M})-sentence. If G and H are ℙ_{2,M}-generic, then M[G] ⊧ φ is equivalent to M[H] ⊧ φ.

Proof. Immediate from Lemma 4.6. □

Let C be a countable subset of P (|M|). A ℙ_{2,M}-generic G is said to be ℙ_{2,M}- C-generic if, for every ℙ_{2,M}-dense M ∪ C definable set D, there exists P ∈ D such that G ∈ [P]. Then, G = ⟨G_{1}, G_{2}⟩ ∈ P_{M}^{2} is ℙ_{2,M}-C-generic if and only if G_{1} is ℙ_{1,M}-C-generic and G_{2} is ℙ_{1,M[G_{1}]}-C-generic.

Lemma 4.8 Let M be a principal model of RCA_{0}. Let C be a countable subset of P (|M|) such that S_{M} ∩ C = ∅. If G is ℙ_{2,M}-C-generic, S_{M[G]} ∩ C = ∅.

Proof. Use Lemma 3.8 repeatedly. □

Now, by iterating 1-forcing notion, for any i > 0, we can define the i-forcing notion. Given the (i − 1)-forcing notion, the i-forcing notion is defined as follows. An i-condition is defined to be a pair ⟨P, P′⟩ such that P is an (i−1)- condition and P ⊩_{i} (Name(P′) and P′ is a 1-condition). ⟨P, P′⟩ ≤_{i} ⟨Q, Q′⟩ if P ≤_{i−1} Q and P ⊩_{i−1} P′ ⊆ Q′. ⟨P, P′⟩ ⊩_{i} Name(X) if P ⊩_{i−1} (P′ ⊩_{1} Name(X)). Let ℙ_{i} be the set of i-conditions. D ⊆ ℙ_{i,M} is ℙ_{i,M}-dense, if for each P ∈ ℙ_{i,M}, there exists P′ ∈ D such that P′ ≤_{i} P. Let G be a generic filter of ℙ_{i,M}. Then, we can regard G as a sequence ⟨G_{1}, …, G_{i}⟩ such that G_{k} is ℙ_{1,M[⟨G_{1},...G_{k−1}⟩]} for each k = 1, …, i. We call it ℙ_{i,M}-generic. For any ℙ_{i,M}-generic G = ⟨G_{1}, … G_{i}⟩ and any i-condition P = ⟨T_{1}, …, T_{i}⟩, G ∈ [P] means that G_{k} ∈ [T_{k}] for k = 1, … i. Let C be a countable subset of P (|M|). A ℙ_{i,M}-generic G is said to be ℙ_{i,M}-C-generic, if for every ℙ_{i,M}-dense M ∪ C definable set D, there exists P ∈ D such that G ∈ [P].

Definition 4.9 Let M be a principal model of RCA_{0}. Let φ be a sentence for L_{2}(|M| ∪ S_{M} ∪ {G_{1}, G_{2}, …, G_{i}}). For any P ∈ ℙ_{i,M}, φ is said to be weakly forced by P (denoted P ⊩_{i} φ) if M[G] ⊧ φ for all ℙ_{i,M}-generic G ∈ [P].

The above properties on 2-forcing notion (Lemma 4.2 to Lemma 4.8) can be automatically extended to any i-forcing notion.

Next we define the ω-forcing notion. Fix a sequence U = ⟨U_{i} : i > 0⟩ such that each U_{i}’s are i-names and ⟨… ⟨U_{1}, U_{2}⟩, …, U_{i−1}⟩ ⊩_{i−1} “U_{i} is a universal tree”. An ω-condition P is an i-condition such that P ≤_{i} ⟨… ⟨U_{1}, U_{2}⟩, …, U_{i}⟩ , for some i > 0. Let ℙ_{ω} be the set of ω-conditions. We may assume that ω is an initial segment of M closed under +_{M} and ·_{M} [7]. Then, P ∈ ℙ_{ω,M} is definable with parameters from |M| ∪ S_{M} ∪ {ω} over M. If P ∈ ℙ_{ω} is an i-condition and j > i, we can identify P with j-condition ⟨… ⟨⟨P, U_{i+1}⟩, …, U_{j}⟩. Then, for P, P′ ∈ ℙ_{ω}, we write P ≤_{ω} P′ if P is an i-condition, P′ is a j-condition, j ≤ i and P ≤_{i} P′. Let G be a generic filter of ℙ_{ω}, i.e., a filter G meets all dense subsets of ℙ_{ω} definable with parameters from |M| ∪ S_{M} ∪ {ω} over M. Then, we can regard G as a sequence ⟨G_{j} : j > 0⟩ such that the G_{j}’s are ℙ_{1,M[⟨G_{1},...G_{j−1}⟩]}. We call it ℙ_{ω,M}-generic. For any ℙ_{ω,M}-generic G = ⟨G_{j} : j > 0⟩ and any ω-condition P = ⟨…, ⟨T_{1}, T_{2}⟩, …, T_{i}⟩, G ∈ [P] means that G_{k} ∈ [T_{k}] for k = 1, …, i.

Lemma 4.10 Let M be a principal model of RCA_{0}. Let G = ⟨G_{j} : j > 0⟩ be ℙ_{ω,M}-generic. Then, M[G] ⊧ WKL_{0}.

Proof. For any T ∈ T_{M}, if T′ is an M-universal tree, there exists an Mcontinuous function F : [T′] → [T]. Therefore, T has a path in S_{M[G_{1}]} since G_{1} is a path through some M-universal tree. Thus, for each i ∈ ω_{>0}, any T ∈ T_{M[G_{1},...,G_{i−1}]} has a path in S_{M[G_{1},...,G_{i}]}. Then M[G] is a model of WKL_{0}. □

Definition 4.11 Let M be a principal model of RCA_{0}. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {G_{j} : j > 0}). For any P ∈ ℙ_{ω,M}, φ is said to be weakly forced by P (denoted P ⊩_{ω} φ) if M[G] ⊧ φ for all ℙ_{ω,M}-generic G ∈ [P].

The next lemma can be proved in the same way as Lemma 3.2.

Lemma 4.12 Let M be a principal model of RCA_{0}. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {G_{j} : j > 0}). Then we have

(1) P ⊩_{ω} φ is definable with parameter from |M| ∪ S_{M} ∪ {ω} over M.

(2) For any ℙ_{ω,M}-generic G ∈ [P], if M[G] ⊧ φ then there exists P′ ∈ ℙ_{ω,M} such that P′ ≤_{ω} P and P′ ⊩_{ω} φ.

Lemma 4.13 Let M be a principal model of RCA_{0}. If P_{1} and P_{2} are two ω-conditions, then P_{1} ⊩_{ω} φ if and only if P_{2} ⊩_{ω} φ for any sentence φ in L_{2}(|M| ∪ S_{M}).

Proof. The proof is an obvious modification of the proof of Lemma 4.5. Let P_{1} and P_{2} be two ω-conditions. Suppose that P_{2} ⊩_{ω} φ. Fix any ℙ_{ω,M}-generic G = ⟨G_{j} : j > 0⟩ ∈ [P_{1}]. We assume that P_{1} = ⟨… ⟨⟨T_{1}, T_{2}⟩, T_{3}⟩ …, T_{j}⟩ and P_{2} = ⟨… ⟨⟨T′_{1}, T′_{2}⟩, T′_{3}⟩ …, T′_{j}⟩. Since T_{1} and T′_{1} are M-universal, there exists an M-homeomorphism H_{1} : [T_{1}] → [T′_{1}]. Then, M[G_{1}] = M[H_{1}(G_{1})]. Therefore, i_{G}(T_{2})(= i_{G_{1}}(T_{2})) is M[H_{1}(G_{1})]-universal. Then, there exists an M[H_{1}(G_{1})]-homeomorphism H_{1} : [i_{G_{1}}(T_{2})] → [i_{H_{1}(G_{1})}(T′_{2})]. Thus we have

M[G] = M[⟨H_{1}(G_{1}), H_{2}(G_{2}), G_{3}, …, G_{j}, …⟩].

By iterating the above argument, let H be a sequence ⟨H_{k} : k ≤ j⟩ such that each H_{k} is M[⟨G_{1}, …, G_{k}⟩]-homeomorphism from [i_{G}(T_{k})] to [i_{G′}(T′_{k})], where G′ = ⟨H_{1}(G_{1}), …, H_{k}(G_{k})⟩. Then, we have a ℙ_{ω,M}-generic H(G) such that H(G) = ⟨H_{1}(G_{1}), …, H_{j}(G_{j}), G_{j+1}, …⟩. Therefore, M[G] = M[H(G)] ⊧ φ by H(G) ∈ [P_{2}]. Hence, P_{1} ⊩_{ω} φ ⇒ P_{2} ⊩_{ω} φ. Similarly, we can show that P_{2} ⊩_{ω} φ ⇒ P_{1} ⊩_{ω} φ. □

Lemma 4.14 Let M be a principal model of RCA_{0}. Let φ be an L_{2}(|M|∪S_{M})- sentence. If G is ℙ_{ω,M}-generic, then M[G] ⊧ φ is equivalent to ⊩_{ω} φ, i.e., P ⊩_{ω} φ for all P ∈ ℙ_{ω,M}.

Proof. Suppose that G is ℙ_{ω,M}-generic and M[G] ⊧ φ. Since M[G] ⊧ φ, there exists P ⊩_{ω} φ. By Lemma 4.13, for any P′ ∈ ℙ_{ω,M}, P′ ⊩_{ω} φ. □

Lemma 4.15 Let M be a principal model of RCA_{0}. Let φ be an L_{2}(|M| ∪ S_{M})-sentence. If G and H are ℙ_{ω,M}-generic, then M[G] ⊧ φ is equivalent to M[H] ⊧ φ.

Proof. Immediate from Lemma 4.14. □

Let C be a countable subset of P (|M|). A ℙ_{ω,M}-generic G is said to be ℙ_{ω,M}- C-generic if, for every ℙ_{ω,M}-dense, M ∪ C definable set D, there exists P ∈ D such that G ∈ [P]. Then, if G = ⟨G_{j} : j > 0⟩, each G_{j} is ℙ_{1,M[⟨G_{1},...G_{j−1}⟩]}-C-generic.

Lemma 4.16 Let M be a principal model of RCA_{0}. Let C be a countable subset of P (|M|) such that S_{M} ∩ C = ∅. If G is ℙ_{ω,M}-C-generic, then S_{M[G]} ∩ C = ∅.

Proof. Suppose that S_{M[G]} ∩ C ≠ ∅. Then, there exists A ∈ C such that A ∈ S_{M[⟨G_{1},...G_{j}⟩]} for some j > 0. Since ⟨G_{1}, …, G_{j}⟩ is ℙ_{j,M}-C-generic (cf. Lemma 4.3), this is a contradiction. □

Lemma 4.17 Let M be a principal model of RCA_{0}. Then there exist two countable models M_{1}, M_{2} of WKL_{0} such that:

(1) M_{1} and M_{2} have the same first order part as M,

(2) S_{M_{1}} ∩ S_{M_{2}} = S_{M},

(3) M_{1} and M_{2} satisfy the same L_{2}(|M| ∪ S_{M})-sentences.

Proof. Suppose that M is a principal model of RCA_{0}. Let G be ℙ_{ω,M}-generic. Set C = S_{M[G]} \ S_{M}. By Lemma 4.16, there exists ℙ_{ω,M}-generic H such that M[H] ∩ C = ∅. By Lemma 4.15, M[G] and M[H] satisfy the same sentences with parameters from |M|∪S_{M}. By Lemma 4.10, M[G] and M[H] are models of WKL_{0}. □

Now, we have the main result of this paper.

Theorem 4.18 Let φ(X, Y) be an arithmetical formula with only the free variables shown. If WKL_{0} proves ∀X∃!Y φ(X, Y), then so does RCA_{0}. (Indeed, RCA_{0} also proves ∀X∃Y (Y is recursive in X ∧ φ(X, Y)).)

Proof. Let φ(X, Y) be an arithmetical formula with only the free variables shown. Suppose that WKL_{0} proves ∀X∃!Y φ(X, Y). By way of contradiction, we assume RCA_{0} does not prove ∀X∃!Y (Y is recursive in X ∧ φ(X, Y)). Then by Gödel’s completeness theorem, there exists a countable model M of RCA_{0} in which ¬∃!Y (Y is recursive in A ∧ φ(A, Y) holds for some A ∈ S_{M}. Let S_{0} = {B ∈ S_{M} : M ⊧ B is recursive in A} and M_{0} = (|M|, S_{0}, +_{M}, ·_{M}, 0_{M}, 1_{M}, <_{M} ). Then M_{0} is a principal model of RCA_{0} such that M_{0} ⊧ ¬∃!Y φ(A, Y).

First suppose that ∃Y φ(A, Y) holds in M_{0}. Then there exist more than one sets in S_{0} which satisfy φ. By Lemma 2.6, there exists a model M′ of WKL_{0} such that M′ has the same first order part as M and S_{M_{0}} ⊆ S_{M′}. Therefore, WKL_{0} does not prove ∀X∃!Y φ(X, Y), which is a contradiction.

Next assume that ∀Y ¬φ(A, Y) holds within M_{0}. By Lemma 4.17, there exists two countable models M_{1} and M_{2} of WKL_{0} such that:

(1) M_{1} and M_{2} have the same first order part as M_{0},

(2) S_{M_{1}} ∩ S_{M_{2}} = S_{M_{0}},

(3) M_{1} and M_{2} satisfy the same sentences with parameters from |M| ∪ S_{M}.

Let Y_{i} ∈ S_{M_{i}} be such that M_{i} satisfies φ(A, Y_{i}) (i = 1, 2). Then, for each n ∈ |M| and each i = 1, 2,

n ∈ Y_{i} ⇔ M_{i} ⊧ ∃Y (φ(A, Y) ∧ n ∈ Y).

By (3), for each n in |M|,

M_{1} ⊧ ∃Y (φ(A, Y) ∧ n ∈ Y) ⇔ M_{2} ⊧ ∃Y (φ(A, Y) ∧ n ∈ Y).

Therefore, Y_{1}=Y_{2}. Then, by (2), Y_{1} ∈ S_{M_{0}}. Therefore, by (1) and (2), M_{0} satisfies φ(A, Y_{1}) since φ is arithmetical and M ⊧ φ(A, Y_{1}). This is a contradiction. □

Remark 4.19 We can also show that if M is a principal model of RCA_{0} + Σ_{k}^{0} induction (k = 1, 2, …, ∞), then M[G] ⊧ Σ_{k}^{0} induction for any ℙ_{ω,M}-generic G (Yamazaki [unpublished]). Therefore, Theorem 4.18 can be extended as follows: if WKL_{0} + Σ_{k}^{0} induction proves ∀X∃!Y φ(X, Y), then RCA_{0} + Σ_{k}^{0} induction also proves ∀X∃!Y (Y is recursive in X) ∧ φ(X, Y)), where φ(X, Y) is an arithmetical formula with only the free variables shown. In case k = 2 and φ is Σ_{3}^{0}, the above result was already proved by A. M. Fernandes [3], where general cases were mentioned as an open problem. Simpson [13] gives a different proof to Theorem 4.18 with more sophisticated recursion-theoretic investigations.

The following theorem tends to show that our main theorem is optimal.

Theorem 4.20 (1) There exists a Π_{1}^{1} formula φ_{1}(Y) such that WKL_{0} proves the sentence ∃!Y φ_{1}(Y), but WKL_{0} does not prove ∃Y (Y is recursive∧φ_{1}(Y)).

(2) There exists a Π_{1}^{1} formula φ_{2}(Y) such that WKL_{0} proves the sentence ∃!Y φ_{2}(Y), but RCA_{0} does not prove it.

(3) There exists a Σ_{1}^{1} formula φ_{3}(Y) such that WKL_{0} proves the sentence ∃!Y φ_{3}(Y), but RCA_{0} does not prove ∃Y φ_{3}(Y).

Proof. (1) Let φ_{1}(Y) be the Π_{1}^{1} formula

Y = K or (K does not exist and Y = ∅)

where K is a complete recursively enumerable set. Then, the ω-model P (ω) does not satisfy ∃Y (Y is recursive∧φ_{1}(Y)).

(2) Let φ_{2}(Y) be the Π_{1}^{1} formula Y = ∅∨(T has no path), where T is a certain recursive infinite 0-1 tree with no recursive path.

The ω-model REC does not satisfy ∃!Y φ_{2}(Y).

(3) Let φ_{3}(Y) be the Σ_{1}^{1} formula Y = ∅ ∧ (T has a path). Then REC does not satisfy ∃Y φ_{3}(Y). □

Problems. The following are still unknown to our circle.

(1) Suppose WKL_{0} ⊢ ∃!Xφ(X) where φ(X) is a Σ_{1}^{1} formula with no free set variables other than X. Is it the case that WKL_{0} ⊢ ∃X(X is recursive∧φ(X))?

(2) Suppose WKL_{0} ⊢ ∃X(X is not recursive∧φ(X)) where φ(X) is a Σ_{1}^{1} formula with no free set variables other than X. Is it the case that WKL_{0} ⊢ ∃X, Y (X ≠ Y ∧ φ(X) ∧ φ(Y))? A similar question has been asked by Friedman [4].

(3) In [1], Avigad constructed an effective translation of WKL_{0}-proofs of Π_{1}^{1} sentences to RCA_{0}-proofs of the same sentences, by formalizing Harrington’s forcing argument. In fact, his translation has at most a polynomial increase in the length of proofs. Unfortunately, we have not managed to find such an effective bound for our conservation result.

5 Forcing with uniformly pointed perfect trees

In this section, we introduce a forcing argument with universal pointed perfect trees, which is inspired by Sacks [11]. Then we show that for any countable model M of RCA_{0}, there exists a principal model M′ of RCA_{0} such that M′ has the same first order part as M and S_{M} ⊆ S_{M′}.

Let M be a countable model of RCA_{0}. For any T ∈ T_{M}, T is M-perfect if M ⊧(T is perfect). An M-perfect tree T is said to be uniformly pointed if for all X ∈ [T], T has the same index of M-recursiveness in X, that is, there exist e, d ∈ |M| such that for all X ∈ [T],

M[X] ⊧ ∀m(m ∈ T ↔ φ_{Σ}(e, m, X)) and ∀m(m ∈ T ↔ ¬φ_{Σ}(d, m, X)),

where φ_{Σ}(e, m, X) is a fixed universal lightface Σ_{1}^{0} formula.

Let ℙ_{0,M} be the set of uniformly pointed M-perfect trees. Then, it is easy to show that ℙ_{0,M} is M-definable. We say that D ⊆ ℙ_{0,M} is dense if ∀T ∈ ℙ_{0,M}∃T′ ∈ D(T′ ⊆ T). G is a ℙ_{0,M}-generic path if for any L_{2}(|M| ∪ S_{M} ∪ {ω})- definable dense set D, there exists T ∈ D such that G ∈ [T]. The following lemma can be proved in the same way as Lemma 2.2

Lemma 5.1 Let M be a countable model of RCA_{0}. For any T ∈ ℙ_{0,M}, there exists a ℙ_{0,M}-generic path G ∈ [T].

Lemma 5.2 Let M be a countable model of RCA_{0}. If G is ℙ_{0,M}-generic, then M[G] ⊧ RCA_{0}.

Proof. Let G be a ℙ_{0,M}-generic path. We only need to show that M[G] satisfies Σ_{1}^{0} induction. To see this, it suffices to prove the following. For any m ∈ |M| and any Σ_{1}^{0}-formula φ(x, G), the set {n : n <_{M} m ∧ φ(n, G)} is M-finite.

We may assume that φ(x, G) ≡ ∃yθ(x, G[y]) where θ(x, τ) is Σ_{0}^{0} with parameters from |M| ∪ S_{M}. Let D_{m} be the set of T ∈ ℙ_{0,M} such that there exists σ ∈ (2^{m})_{M} such that for each n <_{M} m, M satisfies either

(1) σ(n) = 0 and ∀τ ∈ T ¬θ(n, τ)

or

(2) σ(n) = 1 and ∃k∀τ ∈ T (lh(τ) = k → ∃τ′ ⊆ τθ(n, τ′)).

Then, the set {n : n <_{M} m ∧ φ(n, P)} is M-finite if P ∈ [T] for some T ∈ D_{m}. Therefore, it remains to show that D_{m} is dense. Let T ∈ ℙ_{0,M} be given. We say that σ ∈ (2^{m})_{M} is good if M ⊧ ∃τ ∈ T ∀x < m(σ(x) = 1 → ∃τ′ ⊆ τθ(x, τ′)). Set S_{m} = {σ ∈ (2^{m})_{M} : σ is good}. Since M satisfies bounded Σ_{1}^{0} comprehension, S_{m} is M-finite. Moreover, S_{m} is nonempty since ⟨0, …, 0⟩ (with m 0’s ) is an element of S_{m}. Let σ_{m} be the lexicographically largest element of S_{m}. Since σ_{m} is good, there exists τ_{m} ∈ T such that

M ⊧ ∀x < m(σ_{m}(x) = 1 → ∃τ′ ⊆ τ_{m}θ(x, τ′)).

Set T′ = {τ ∈ T : M ⊧ τ is compatible with τ_{m}}. We are going to show that T′ ∈ D_{m}. To see this, let n <_{M} m be given. If σ_{m}(n) = 1, then M ⊧ ∃τ′ ⊆ τ_{m}θ(n, τ′). Then

M ⊧ ∃k∀τ ∈ T′(lh(τ) = k → ∃τ′ ⊆ τθ(n, τ′)).

Suppose that σ_{m}(n) = 0. Let σ′ be a 0-1 string such that σ′(n) = 1 and σ′(x) = σ_{m}(x) for x ≠ n. Then, by the definition of σ_{m}, M ⊧ ∀τ ∈ T ¬θ(n, τ).

So M ⊧ ∀τ ∈ T′¬θ(n, τ). Therefore, T′ belongs to D_{m} □

Definition 5.3 Let T ∈ ℙ_{0,M}. For any L_{2}(|M|∪S_{M} ∪{ω, G})-sentence φ, we say that T ⊩_{0} φ if M[G] ⊧ φ for all ℙ_{0,M}-generic path G ∈ [T].

The next lemma can be proved.

Lemma 5.4 Let M be a countable model of RCA_{0}. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {ω, G}). Then we have

(1) T ⊩_{0} φ is definable with parameter from |M| ∪ S_{M} ∪ {ω} over M.

(2) For any ℙ_{0,M}-generic G ∈ [T], if M[G] ⊧ φ then there exists T′ ∈ ℙ_{0,M} such that T′ ⊆ T, G ∈ [T′] and T′ ⊩_{0} φ.

Lemma 5.5 Let M be a countable model of RCA_{0}. Let T and T′ be M-perfect trees. Then, there exists an M-homeomorphism H from [T] to [T′] with its code M-recursive in T ⊕ T′.

Proof. We shall first prove Lemma 5.5 under the assumption that T′ = P_{M}(= (2^{<ℕ})_{M}). Define a function h_{T} from P_{M} to T inductively as follows. h_{T} (⟨⟩) = the least τ ∈ T such that τ^{⌢}⟨i⟩ ∈ T for each i = 0, 1. For j = 0 or 1, h_{T} (σ^{⌢}⟨j⟩) = the least τ ∈ T such that h_{T} (σ)^{⌢}⟨j⟩ ⊆ τ and τ^{⌢}⟨i⟩ ∈ T for each i = 0, 1. Then, h_{T} is M-recursive in T. So, by the construction, Booleanpreserving extension h of h_{T} is a code for an M-homeomorphism from [T] to [P_{M}] which is M-recursive in T.

Let h_{T} (and h_{T′}) be the code for M-homeomorphisms from [T] (and [T′]) to [P_{M}]. Then a function h_{T} (h_{T′}^{−1}⌈rng(h_{T′})) can be extended to a code h_{T,T′} for an M-homeomorphism H_{T,T′} from [T] to [T′] , which is M-recursive in T ⊕ T′. □

H_{T,T′} : [T] → [T′] and h_{T,T′} in the proof of Lemma 5.5 are said be a canonical M-homeomorphism and a canonical code for H_{T,T′}, respectively.

Lemma 5.6 Let T and T′ be two M-trees in ℙ_{0,M} such that REC_{M}(T) = REC_{M}(T′). Let H : [T] → [T′] be a canonical M-homeomorphism. If T_{1} ∈ ℙ_{0,M} is a subtree of T, then there exists a subtree T′_{1} of T′ such that T′_{1} ∈ ℙ_{0,M} and H([T_{1}]) = [T′_{1}].

Proof. Let H : [T] → [T′] be a canonical M-homeomorphism. Fix T_{1} ∈ ℙ_{0,M} such that T_{1} ⊆ T. Then, let T′_{1} = {σ ∈ T′ : ∃τ ∈ T′(σ ⊆ τ ∧ h(τ) ∈ T_{1}}, where h is a canonical code for H. Since T is M-recursive in T′, h is Mrecursive in T′. So T′_{1} is M-recursive in T′ ⊕ T_{1}. Obviously, T′_{1} is M-perfect and H([T_{1}]) = [T′_{1}].

It remains to show that T′ is uniformly pointed. To see this, fix X ∈ [T]. Since H^{−1}(X) ∈ [T_{1}] and T_{1} is uniformly pointed, then

T′_{1} ≤_{T} T′ ⊕ T_{1} ≤_{T} T′ ⊕ H^{−1}(X) ≤_{T} T′ ⊕ X.

Since T is M-recursive in T′, h is M-recursive in T′. So T′_{1} is M-recursive in T′ ⊕ T_{1}. Since X ∈ [T′] and T′ is uniformly pointed, then T′_{1} is M-recursive in X. In fact, by the above argument, for any X ∈ [T], T′_{1} has the same index of M-recursiveness in X. □

Lemma 5.7 Let M be a countable model of RCA_{0}. Let T ∈ ℙ_{0,M}. Then, for any A ∈ S_{M}, if T is M-recursive in A, there exists a subtree T′ of T such that T′ ∈ ℙ_{0,M} and REC_{M}(A) = REC_{M}(T′).

Proof. Fix any T ∈ ℙ_{0,M} and any A ∈ S_{M}. Let h be a canonical code for a canonical M-homeomorphism H : [T] → [P_{M}]. We work over M. Define B ⊆ P_{M} inductively as follows:

(1) h(⟨⟩) ∈ B and

(2) if lh(σ) = 1 is odd and h(σ) ∈ B, then h(σ^{⌢}⟨i⟩) ∈ B (i = 0, 1) and

(3) if lh(σ) = 1 is even, (lh(σ) − 1)/2 ∈ A and h(σ) ∈ B, then h(σ^{⌢}⟨0⟩) ∈ B

(4) if lh(σ) = 1 is even, (lh(σ) − 1)/2 ∉ A and h(σ) ∈ B, then h(σ^{⌢}⟨1⟩) ∈ B.

Set T′ = {σ ∈ T : ∃τ ∈ B(σ ⊆ τ)}. By the construction, T′ is perfect, and it is recursive in A since T is recursive A. Moreover, for all m ∈ ℕ,

m ∈ A ↔ ∃σ ∈ 2^{<ℕ}(lh(σ) = 2n + 1 ∧ h(σ^{⌢}⟨0⟩) ∈ T′).

Therefore, A is recursive in T ⊕ T′. Consider the leftmost path P through T′. Then, P is recursive in T′. Since T is uniformly pointed, T is recursive in T′, so A is recursive in T′. Hence A and T′ are recursive in each other.

It remains to prove that T′ is uniformly pointed. To see this, fix X ∈ [T′].

Then, for all m ∈ ℕ,

m ∈ A ↔ ∃σ ∈ 2^{<ℕ}(lh(σ) = 2n + 1 ∧ h(σ^{⌢}⟨0⟩) = X[h(σ^{⌢}⟨0⟩)]).

Thus T′ is uniformly pointed since T′ is recursive in A. □

Lemma 5.8 Let M be a countable model of RCA_{0}. Let T_{1}, T_{2} ∈ ℙ_{0,M}. Then, T_{1} ⊩_{0} φ is equivalent to T_{2} ⊩_{0} φ for any sentence φ in L_{2}(|M| ∪ S_{M} ∪ {ω}).

Proof. Let T_{1} and T_{2} be uniformly pointed M-perfect trees. Suppose that T_{1} ⊩_{0} φ and T_{2} ⊮_{0} φ for some L_{2}(|M| ∪ S_{M} ∪ {ω})-sentence φ. Then, by Lemma 5.4 (2), there exists T′_{2} ∈ ℙ_{0,M} such that T′_{2} ⊆ T_{2} and T′_{2} ⊩_{0} ¬φ. According to Lemma 5.7, there exists T′_{1} and T′′_{2} such that T′_{1} ⊩_{0} φ, T′′_{2} ⊩_{0} ¬φ and REC_{M}(T′_{1}) = REC_{M}(T′′_{2})(= REC_{M}(T_{1} ⊕ T′_{2})). Let G be a ℙ_{0,M}-generic path through T′_{1}. Then M[G] ⊧ φ. Let H : [T′_{1}] → [T′′_{2}] be a canonical Mhomeomorphism. By Lemma 5.6, we can show that H(G′) is ℙ_{0,M}-generic through T′′_{2}. Since M[G] = M[H(G)], then M[H(G)] ⊧ φ, so T′′_{2} ⊮_{0} ¬φ. This is a contradiction. □

Lemma 5.9 Let M be a countable model of RCA_{0}. Let φ be an L_{2}(|M|∪S_{M} ∪ {ω})-sentence. If G is ℙ_{0,M}-generic, then M[G] ⊧ φ is equivalent to ⊩_{0} φ, i.e., T ⊩_{0} φ for all T ∈ ℙ_{0,M}.

Proof. Let ℙ_{0,M}-generic G be given. Suppose that T ⊮_{0} φ for some T ∈ ℙ_{0,M}. Since M[G] ⊧ φ, there exists T′ ∈ ℙ_{0,M} such that T′ ⊩_{0} φ. By Lemma 5.8, this is a contradiction. □

Lemma 5.10 Let M be a countable model of RCA_{0}. Then, ⊩_{0} ∃X∀Y (Y is recursive in X). That is, for any ℙ_{0,M}-generic G, M[G] is a principal model of RCA_{0}.

Proof. It is sufficient to show that for any Y ∈ S_{M}, ⊩_{0} (Y is recursive in G). Fix A ∈ S_{M}. Set D_{A} = {T ∈ ℙ_{0,M} : T ⊩_{0} (A is recursive in G)}. We want to show that D_{A} is dense. To see this, fix T ∈ ℙ_{0,M}. By Lemma 5.7, there exists T′ ∈ ℙ_{0,M} such that T′ ⊆ T and A is M-recursive in T′. Since T′ is uniformly pointed, for any ℙ_{0,M}-generic G through T′, T′ is M-recursive in G, that is, A is M-recursive in G. Then T′ ∈ D_{A}. □

Theorem 5.11 Any countable model of RCA_{0} is a submodel of a principal model of RCA_{0} with the same first order part.

Proof. This follows immediately from Lemma 5.10.

Let C be a countable subset of P (M). Then, G is said to be ℙ_{0,M}-C-generic if there exists T ∈ D such that G ∈ [T] for all dense subset D of ℙ_{0,M} definable with parameters from |M| ∪ S_{M} ∪ C ∪ {ω}. For any T ∈ ℙ_{0,M}, there exists a ℙ_{0,M}-C-generic path G through T.

Lemma 5.12 Let M be a countable model of RCA_{0}. Let C be a countable subset of P (|M|) such that S_{M} ∩ C = ∅. If G is ℙ_{0,M}-C-generic, then M[G] ∩ C = ∅.

Proof. We want to show that for any A ∈ C and any Σ_{1}^{0} formulas φ_{1}(x) and φ_{2}(x) with parameters from |M| ∪ S ∪ {G}, either A ≠ {n ∈ |M| : M[G] ⊧ φ_{1}(n)} or A ≠ {n ∈ |M| : M[G] ⊧ ¬φ_{2}(n)}.

We may assume that φ_{i}(x) is of the form ∃yθ_{i}(x, G[y]), where θ_{i}(x, τ) is Σ_{0}^{0} with parameter from |M| ∪ S_{M} (i = 1, 2). Let D_{A} be the set of all T ∈ ℙ_{0,M} such that one of the following holds for some m ∈ |M|:

A1. m ∈ A ∧ M ⊧ ∀τ ∈ T ¬θ_{1}(m, τ),

A2. m ∉ A ∧ M ⊧ ∃w∀τ ∈ T (lh(τ) = w → ∃τ′ ⊆ τθ_{1}(m, τ′)),

A3. m ∈ A ∧ M ⊧ ∃w∀τ ∈ T (lh(τ) = w → ∃τ′ ⊆ τθ_{2}(m, τ′)),

A4. m ∉ A ∧ M ⊧ ∀τ ∈ T ¬θ_{2}(m, τ).

Then it suffices to show that D_{A} is dense.

To see this, let T ∈ ℙ_{0,M} be given. Case 1. Suppose that there exists m ∈ |M| such that for all τ_{1}, τ_{2} ∈ T, either m ∈ A ∧ M ⊧ ∀τ′ ⊆ τ_{1}¬θ_{e}(m, τ′) or m ∉ A ∧ M ⊧ ∀τ′ ⊆ τ_{2}¬θ_{d}(m, τ′). Then T belongs to D_{A}.

Case 2. Suppose that there exists m ∈ |M| and τ_{1}, τ_{2} ∈ T such that either m ∉ A ∧ M ⊧ ∃τ′ ⊆ τ_{1}θ_{e}(m, τ′) or, m ∈ A ∧ M ⊧ ∃τ′ ⊆ τ_{2}θ_{d}(m, τ′). If m ∉ A, let T′ = {σ ∈ T : M ⊧ σ is compatible with τ_{1}}. If m ∈ A, let T′ = {σ ∈ T : M ⊧ σ is compatible with τ_{2}}. Then, T′ is M-perfect. It is also uniformly pointed since T′ is M-recursive in T. So, T′ belongs to D_{A}.

Case 3. Neither Case 1 nor Case 2. Then,

A = {m : M ⊧ ∃τ ∈ T θ_{1}(m, τ)} = {m : M ⊧ ∀τ ∈ T ¬θ_{2}(m, τ)}.

This is a contradiction. □

Let M be a countable model of RCA_{0} and G be ℙ_{0,M}-generic. Then M[G] is a principal model of RCA_{0} by Theorem 5.11. Therefore there exists a ℙ_{ω,M[G]}- generic G′.

Lemma 5.13 Let M be a countable model of RCA_{0}. Let φ be an L_{2}(|M|∪S_{M})- sentence. If G is ℙ_{0,M}-generic and G′ is ℙ_{ω,M[G]}-generic, then M[G][G′] ⊧ φ is equivalent to ⊩_{0}⊩_{ω} φ.

Proof. Let G be ℙ_{0,M}-generic and G′ be ℙ_{ω,M[G]}-generic. By Lemma 4.14,

M[G][G′] ⊧ φ ⇔ M[G] ⊧⊩_{ω} φ.

By Lemma 5.9,

M[G] ⊧⊩_{ω} φ ⇔ M ⊧⊩_{0}⊩_{ω} φ.

□

Theorem 5.14 Let G and H be ℙ_{0,M}-generic. Let G′ and H′ be ℙ_{ω,M[G]}- generic and ℙ_{ω,M[H]}-generic, respectively. Then, M[G][G′] and M[H][H′] satisfy the same L_{2}(|M| ∪ S_{M})-sentences.

Proof. Immediate from Lemma 5.13. □

Lemma 5.15 There exist ℙ_{0,M}-generic G, ℙ_{0,M}-generic H, ℙ_{ω,M[G]}-generic G′ and ℙ_{ω,M[H]}-generic H′ such that S_{M[G][G′]} ∩ S_{M[H][H′]} = S_{M}.

Proof. Fix any ℙ_{0,M}-generic G over M and any ℙ_{ω,M[G]}-generic G′. Let C = S_{M[G][G′]} \ S. Let H be ℙ_{0,M}-C-generic. Let H′ be ℙ_{ω,M[H]}-C-generic. Then, by Lemma 5.12 and Lemma 4.15, S_{M[G][G′]} ∩ S_{M[H][H′]} = S_{M}. □

Corollary 5.16 Let M be a countable model of RCA_{0}. Then there exist two countable models M_{1} and M_{2} of WKL_{0} such that:

(1) M_{1} and M_{2} have the same first order part as M,

(2) S_{M_{1}} ∩ S_{M_{2}} = S_{M}, (3) M_{1} and M_{2} satisfy the same L_{2}(|M| ∪ S_{M})-sentences.

Proof. Take G, H, G′ and H′ as in Lemma 5.15. Let M_{1} = M[G][G′] and M_{2} = M[H][H′]. By Lemma 4.10, M_{1} and M_{2} are models of WKL_{0}. Moreover, according to Theorem 5.14, they satisfy the same sentences with parameters from |M| ∪ S_{M}. □

Theorem 5.17 Let φ(X, Y) be a Π_{1}^{1} formula with exactly the free variables shown. If WKL_{0} proves ∀X∃!Y φ(X, Y), then RCA_{0} proves ∀X∃Y φ(X, Y).

Proof. Let φ(X, Y) be a Π_{1}^{1} formula with exactly the free variables shown. Suppose that WKL_{0} proves ∀X∃!Y φ(X, Y). By way of contradiction, we assume RCA_{0} does not prove ∀X∃Y φ(X, Y). Then by Gödel’s completeness theorem, there exists a countable model M of RCA_{0} in which ¬∃Y φ(A, Y) holds for some A ∈ S_{M}. By Corollary 5.16, there exist two countable models M_{1} and M_{2} of WKL_{0} such that (1) they have the same first order part as M, (2) S_{M_{1}} ∩ S_{M_{2}} = S_{M} and (3) they satisfy the same L_{2}(|M| ∪ S_{M})-sentences. Let Y_{i} ∈ S_{M_{i}} be such that M_{i} satisfies φ(A, Y_{i}) (i = 1, 2). Then, for each n ∈ |M| and each i = 1, 2,

n ∈ Y_{i} ⇔ M_{i} ⊧ ∃Y (φ(A, Y) ∧ n ∈ Y).

By (3), for each n in |M|,

M_{1} ⊧ ∃Y (φ(A, Y) ∧ n ∈ Y) ⇔ M_{2} ⊧ ∃Y (φ(A, Y) ∧ n ∈ Y).

Therefore, Y_{1}=Y_{2}. Then, by (2), Y_{1} ∈ S_{M_{0}}. Therefore, by (1) and (2), M satisfies φ(A, Y_{1}) since φ is Π_{1}^{1} and M_{1} satisfies φ(A, Y_{1}). This is a contradiction. □

6 A further conservation result

The system WKL_{0}^{+} (RCA_{0}^{+}) is obtained from WKL_{0} (RCA_{0}) by adding the following scheme:

∀n∀σ ∈ 2^{<ℕ}∃τ ∈ 2^{<ℕ}(σ ⊆ τ ∧ φ(n, τ)) → ∃X∀n∃kφ(n, X[k]),

where φ(x, y) is an arithmetical formula with no occurrence of X. We recall some backgrounds from Brown/Simpson [2]. There are two versions of the Baire category theorem, BCT-I and BCT-II. A version of Urysohn’s lemma for complete separable metric spaces follows from BCT-I, which is provable in RCA_{0} (cf. [12, Lemma II.7.3]). By contrast, the Bounded Inverse Mapping Theorem for separable Banach spaces is usually deduced from BCT-II, which is not provable in RCA_{0}, but in RCA_{0}^{+}. It is unknown whether or not the Bounded Inverse Mapping Theorem is provable in RCA_{0}. Brown/Simpson [2] proved also that WKL_{0}^{+} is conservative over RCA_{0} with respect to Π_{1}^{1} sentences.

In this section, we generalize our main theorem to show that if WKL_{0}^{+} ⊢ ∀X∃!Y φ(X, Y), then so does RCA_{0}, where φ(X, Y) is arithmetical. To prove it, for any principal model M of RCA_{0}, we will construct two countable models M_{1}, M_{2} of WKL_{0}^{+} with S_{M_{1}} ∩ S_{M_{2}} = S_{M} which have the same first order part, and satisfy the same sentences with parameters from |M| ∪ S_{M}.

Let M be a countable model of RCA_{0}. For each σ, τ ∈ (2^{<ℕ})_{M}, we write τ ≤_{1}^{+} σ if τ extends σ. We say that D ⊆ (2^{<ℕ})_{M} is dense if for each σ ∈ (2^{<ℕ})_{M}, there exists τ ∈ D such that τ ≤_{1}^{+} σ. A path G is said to be (2^{<ℕ})_{M}-generic if, for every M-definable dense set D ⊆ (2^{<ℕ})_{M}, there exists σ ∈ D such that G ∈ [σ].

Lemma 6.1 Let M be a countable model of RCA_{0} and suppose that G ∈ P_{M} is (2^{<ℕ})_{M}-generic. Then M[G] ⊧ RCA_{0}.

Proof. See [2, Lemma 6.1]. □

Definition 6.2 Let M be a countable model of RCA_{0}. Let φ be a sentence in L_{2}(|M| ∪ S_{M} ∪ {G}). For any σ ∈ (2^{<ℕ})_{M}, φ is said to be weakly forced by σ (denoted T ⊩_{1}^{+} φ) if M[G] ⊧ φ for all (2^{<ℕ})_{M}-generic G ∈ [σ].

Lemma 6.3 Let M be a countable model of RCA_{0}. Let φ be a sentence of L_{2}(|M| ∪ S_{M} ∪ {G}). Then we have

(1) σ ⊩_{1} φ is definable over M.

(2) For any (2^{<ℕ})_{M}-generic G ∈ [σ], if M[G] ⊧ φ then there exists σ ⊆ τ such that G ∈ [τ] and τ ⊩_{1}^{+} φ.

Proof. Similar to Lemma 3.2. □

Lemma 6.4 Let M be a countable model of RCA_{0}. If σ_{1} and σ_{2} are in (2^{<ℕ})_{M}, then σ_{1} ⊩_{1}^{+} φ if and only if σ_{2} ⊩_{1}^{+} φ for any sentence φ of L_{2}(|M| ∪ S_{M}).

Proof. For any σ, τ ∈ (2^{<ℕ})_{M}, let F be a function from [σ] to [τ] such that for each X ∈ [σ], F (X) = {n : τ(n) = 1} ∪ {lh(τ) + n : n ∈ X′} where X = {n : σ(n) = 1}∪{lh(σ)+n : n ∈ X′}. Obviously, F is an M-homeomorphism from [σ] to [τ]. Therefore, Lemma 6.4 can be proved in the same way as Lemma 3.5. □

Let C be a countable subset of P (|M|). G is said to be (2^{<ℕ})_{M}-C-generic if for every M ∪ C-definable dense D, there exists σ ∈ D such that G ∈ [σ].

Lemma 6.5 Let M be a countable model of RCA_{0}, and C a countable subset of P (|M|) such that C ∩ S_{M} = ∅. If G is (2^{<ℕ})_{M}-C-generic, then M[G] is a countable model of RCA_{0} with S_{M[G]} ∩ C = ∅.

Proof. It suffices to show that for any A ∈ C and any Σ_{1}^{0} formulas φ_{1}(x) and φ_{2}(x) with parameters from |M| ∪ S ∪ {G}, either A ≠ {n ∈ |M| : M[G] ⊧ φ_{1}(n)} or A ≠ {n ∈ |M| : M[G] ⊧ ¬φ_{2}(n)}. By way of contradiction, we suppose that A = {n ∈ |M| : M[G] ⊧ φ_{1}(n)} = {n ∈ |M| : M[G] ⊧ ¬φ_{2}(n)}.

We may assume that φ_{i}(x) is of the form ∃yθ_{i}(x, G[y]), where θ_{i}(x, τ) is Σ_{0}^{0} with parameter from |M| ∪ S_{M} (i = 1, 2). Let E^{A} be the set of all σ ∈ (2^{<ℕ})_{M} such that there exists m ∈ |M| such that for any extension τ of σ, one of the following holds:

A1. m ∈ A ∧ M ⊧ ∀τ′ ⊆ τ¬θ_{1}(m, τ′),

A2. m ∉ A ∧ M ⊧ ∃τ′ ⊆ τθ_{1}(m, τ′),

A3. m ∈ A ∧ M ⊧ ∃τ′ ⊆ τθ_{2}(m, τ′),

A4. m ∉ A ∧ M ⊧ ∀τ′ ⊆ τ¬θ_{2}(m, τ′).

We define D_{A} by

σ ∈ D_{A} if and only if σ ∈ E_{A} ∨ ¬∃τ ∈ E_{A}(σ ⊆ τ).

Then D_{A} is (2^{<ℕ})_{M}-dense, and M ∪ C-definable. Take σ_{0} ∈ D_{A} with G ∈ [σ_{0}]. We first claim that σ_{0} ∈ E_{A}. By way of contradiction, suppose that σ_{0} ∉ E_{A}.

Then for all τ ⊇ σ_{0},

∀x∃τ′ ⊇ τ((x ∈ A ↔ ∃τ′′ ⊆ τ′θ_{1}(x, τ′′)) ∧ (x ∈ A ↔ ∀τ′′ ⊆ τ′¬θ_{2}(x, τ′′))). Therefore, for any n ∈ |M|, n ∈ A ⇔ M ⊧ ∃τ ⊇ σ_{0}∃τ′ ⊆ τθ_{1}(n, τ′) ⇔ M ⊧ ∀τ ⊃ σ_{0}∀τ′ ⊆ τ¬θ_{2}(n, τ′). Then A ∈ S_{M}. This is a contradiction with C ∩ S_{M} = ∅. Thus, since σ_{0} is in E_{A}, there exists m_{0} ∈ |M| such that for all τ ⊃ σ_{0}, either

B1. m_{0} ∈ A ∧ M ⊧ (∀τ′ ⊆ τ¬θ_{1}(m_{0}, τ′)∨ ∃τ′ ≤ τθ_{2}(m, τ′)), or B2. m_{0} ∉ A ∧ M ⊧ (∀τ′ ⊆ τ¬θ_{2}(m_{0}, τ′)∨ ∃τ′ ≤ τθ_{1}(m, τ′)).

Assume that m_{0} ∈ A. Fix an initial segment τ of G such that τ is an endextension of σ_{0} and G[l] with θ_{1}(m_{0}, G[l]). By B1, ∃τ′ ≤ τθ_{2}(m, τ′)). Then, ∃yθ_{2}(m_{0}, G[y]), that is, m_{0} ∉ A. This is a contradiction. The case of x_{0} ∉ A can be treated similarly. This completes the proof. □ As in Section 4, by iterating the two forcing notions ⊩_{1} and ⊩_{1}^{+} alternatively, we can define the notion of +-ω-forcing ⊩_{ω}^{+}, which satisfies the following properties. Lemma 6.6 Let M be a principal model of RCA_{0}. Then the following hold.

(1) If G is generic for ⊩_{ω}^{+}, then M[G] ⊧ WKL_{0}^{+}.

(2) Any two +-ω-conditions weakly force the same L_{2}(|M| ∪ S_{M})-sentences.

(3) Let C be a countable subset of P (|M|) such that S_{M} ∩ C = ∅. Then there exists a generic G for ⊩_{ω}^{+} such that S_{M[G]} ∩ C = ∅. Lemma 6.7 Let M be a principal model of RCA_{0}. Then there exist two countable models M_{1}, M_{2} of WKL_{0}^{+} such that:

(1) M_{1} and M_{2} have the same first order part as M,

(2) S_{M_{1}} ∩ S_{M_{2}} = S_{M},

(3) M_{1} and M_{2} satisfy the same L_{2}(|M| ∪ S_{M})-sentences. Proof. It is straightforward from Lemma 6.6 (3). □

Theorem 6.8 Let φ(X, Y) be an arithmetical formula with only the free variables shown. If WKL_{0}^{+} proves ∀X∃!Y φ(X, Y), then so does RCA_{0}. (Then, RCA_{0} also proves ∀X∃Y (Y is recursive in X ∧ φ(X, Y)).)

Proof. The proof is an obvious modification of the proof of Theorem 4.18 with the help of Lemma 6.7. □

References

[1] J. Avigad, Formalizing forcing arguments in subsystems of second order arithmetic, Annals of Pure and Applied Logic 82 (1996) 165–191.

[2] D. K. Brown, S. G. Simpson, The Baire category theorem in weak subsystems of second order arithmetic, Journal of Symbolic Logic 58 (1993) 557–578.

[3] A. M. Fernandes, A new conservation result of WKL_{0} over RCA_{0}, submitted.

[4] H. Friedman, Subsystems of second order arithmetic and their use in the formalization of mathematics, 19 pages, unpublished (March 1974).

[5] P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1993, xIV + 460 pages.

[6] C. G. Jockusch, Jr., R. I. Soare, Π_{1}^{0} classes and degrees of theories, Transactions of the American Mathematical Society 173 (1972) 35–56.

[7] R. Kaye, Models of Peano Arithmetic, Oxford University Press, 1991, x + 292 pages.

[8] U. Kohlenbach, Effective modului from ineffective uniqueness proofs. An unwinding of de La Vallee Pousin’s proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 (1993) 27–94.

[9] M. B. Pour-El, S. Kripke, Deduction-preserving “recursive isomorphisms” between theories, Fundamenta Mathematicae 61 (1967) 141–163.

[10] H. Rogers, Jr., Theory of Recursive Functions and Effective Computability, McGraw-Hill, 1967, xIX + 482 pages.

[11] G. E. Sacks, Forcing with perfect closed sets, in: D. S. Scott (Ed.), Axiomatic Set Theory, Part 1, Vol. 13 of Proceedings of Symposia in Pure Mathematics, American Mathematical Society, 1971, pp. 331–355, vI + 474 pages.

[12] S. G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1999, xIV + 445 pages.

[13] S. G. Simpson, Π_{1}^{0} sets and models of WKL_{0} Preprint, 26 pages, to appear.

[14] K. Tanaka, More on models of WKL_{0}, 4 pages, handwritten (1995).

[15] T. Yamazaki, Some more conservation results on the Baire category theorem, Mathematical Logic Quarterly 46 (2000) 105–110.