A Symmetric β-Model

Stephen G. Simpson Department of Mathematics Pennsylvania State University

               www.math.psu.edu/simpson/

Draft: May 23, 2000

This research was partially supported by NSF grant DMS-0070718. Subject Classification: 03F35, 03C62, 03C25, 03D80, 03B30.

1 The Main Results

Our context is the study of ω-models of subsystems of second order arithmetic [5, Chapter VIII]. As in [5, Chapter VII], a β-model is an ω-model M such that, for all Σ_{1}^{1} sentences φ with parameters from M, φ is true if and only if M ⊧ φ. Theorems 1.1 and 1.3 below are an interesting supplement to the results on β-models which have been presented in Simpson [5, §§VII.2 and VIII.6].

Let HYP denote the set of hyperarithmetical reals. It is well known that, for any β-model M, HYP is properly included in M, and each X ∈ HYP is definable in M.

Theorem 1.1. There exists a countable β-model satisfying

∀X (if X is definable, then X ∈ HYP).

Proof. Fix a recursive enumeration S_{e}, e ∈ ω, of the Σ_{1}^{1} sets of reals. If p is a finite subset of ω × ω^{<ω}, say that ⟨X_{n}⟩_{n∈ω} meets p if X_{n_{1}} ⊕ ⋯ ⊕ X_{n_{k}} ∈ S_{e} for all (e, ⟨n_{1}, …, n_{k}⟩) ∈ p. Let P be the set of p such that there exists ⟨X_{n}⟩_{n∈ω} meeting p. Put p ≤ q if and only if p ⊇ q. Say that D ⊆ P is dense if for all p ∈ P there exists q ∈ D such that q ≤ p. Say that D is definable if it is definable over the ω-model HYP, i.e., arithmetical in the complete Π_{1}^{1} subset of ω. Say that ⟨G_{n}⟩_{n∈ω} is generic if for every dense definable D ⊆ P there exists p ∈ D such that ⟨G_{n}⟩_{n∈ω} meets p. We can show that for every p ∈ P there exists a generic ⟨G_{n}⟩_{n∈ω} meeting p. (This is a fusion argument, a la Gandy forcing.) Clearly {G_{n} : n ∈ ω} is a β-model. We can also show that, if C is countable and C ∩ HYP = ∅, then there exists a generic ⟨G_{n}⟩_{n∈ω} such that C ∩ {G_{n} : n ∈ ω} = ∅.

Let L_{2}(⟨X_{n}⟩_{n∈ω}) be the language of second order arithmetic with additional set constants X_{n}, n ∈ ω. Let φ be a sentence of L_{2}(⟨X_{n}⟩_{n∈ω}). We say that p forces φ, written p ⊩ φ, if for all generic ⟨G_{n}⟩_{n∈ω} meeting p, the β-model {G_{n} : n ∈ ω} satisfies φ[⟨X_{n}/G_{n}⟩_{n∈ω}]. It can be shown that, for all generic ⟨G_{n}⟩_{n∈ω}, the β-model {G_{n} : n ∈ ω} satisfies φ[⟨X_{n}/G_{n}⟩_{n∈ω}] if and only if ⟨G_{n}⟩_{n∈ω} meets some p such that p ⊩ φ.

If π is a permutation of ω, define an action of π on P and L_{2}(⟨X_{n}⟩_{n∈ω}) by π(p) = {(e, ⟨π(n_{1}), …, π(n_{k})⟩) : (e, ⟨n_{1}, …, n_{k}⟩) ∈ p} and π(X_{n}) = X_{π(n)}. It is straightforward to show that p ⊩ φ if and only if π(p) ⊩ π(φ). The support of p ∈ P is defined by supp(p) = ⋃{{n_{1}, …, n_{k}} : (e, ⟨n_{1}, …, n_{k}⟩) ∈ p}. Clearly if p, q ∈ P and supp(p) ∩ supp(q) = ∅, then p ∪ q ∈ P.

We claim that if ⟨G_{n}⟩_{n∈ω} and ⟨G′_{n}⟩_{n∈ω} are generic, then the β-models {G_{n} : n ∈ ω} and {G′_{n} : n ∈ ω} satisfy the same L_{2}-sentences. Suppose not. Then for some p, q ∈ P we have p ⊩ φ and q ⊩ ¬ φ, for some L_{2}-sentence φ. Let π be a permutation of ω such that supp(π(p)) ∩ supp(q) = ∅. Since π(φ) = φ, we have π(p) ⊩ φ, hence π(p) ∪ q ⊩ φ, a contradiction. This proves our claim.

Finally, let M = {G_{n} : n ∈ ω} where ⟨G_{n}⟩_{n∈ω} is generic. Suppose A ∈ M is definable in M. Let ⟨G′_{n}⟩_{n∈ω} be generic such that M′ = {G′_{n} : n ∈ ω} has M ∩ M′ = HYP. Let φ(X) be an L_{2}-formula with X as its only free variable, such that M ⊧ (∃ exactly one X) φ(X), and M ⊧ φ(A). Then M′ ⊧ (∃ exactly one X) φ(X). Let A′ ∈ M′ be such that M′ ⊧ φ(A′). Then for each n ∈ ω, we have that n ∈ A if and only if M ⊧ ∃X (φ(X) and n ∈ X), if and only if M′ ⊧ ∃X (φ(X) and n ∈ X), if and only if n ∈ A′. Thus A = A′. Hence A ∈ HYP. This completes the proof. □

Remark 1.2. Theorem 1.1 has been announced without proof by Friedman [3, Theorem 4.3]. Until now, a proof of Theorem 1.1 has not been available.

We now improve Theorem 1.1 as follows.

Let ≤_{HYP} denote hyperarithmetical reducibility, i.e., X ≤_{HYP} Y if and only if X is hyperarithmetical in Y.

Theorem 1.3. There exists a countable β-model satisfying

(∗) ∀X ∀Y (if X is definable from Y, then X ≤_{HYP} Y).

The β-model which we shall use to prove Theorem 1.3 is the same as for Theorem 1.1, namely M = {G_{n} : n ∈ ω} where ⟨G_{n}⟩_{n∈ω} is generic. In order to see that M has the desired property, we first relativize the proof of Theorem 1.1, as follows. Given Y, let P^{Y} be the set of p ∈ P such that there exists ⟨X_{n}⟩_{n∈ω} meeting p with X_{0} = Y. (Obviously 0 plays no special role here.) Say that ⟨G_{n}⟩_{n∈ω} is generic over Y if, for every dense D^{Y} ⊆ P^{Y} definable from Y over HYP(Y) = {X : X ≤_{HYP} Y }, there exists p ∈ D^{Y} such that ⟨G_{n}⟩_{n∈ω} meets p.

Lemma 1.4. If ⟨G_{n}⟩_{n∈ω} is generic over Y, then G_{0} = Y, and {G_{n} : n ∈ ω} is a β-model satisfying ∀X (if X is definable from Y, then X ≤_{HYP} Y).

Proof. The proof of this lemma is a straightforward relativization to Y of the proof of Theorem 1.1. □

Consequently, in order to prove Theorem 1.3, it suffices to prove the following lemma.

Lemma 1.5. If ⟨G_{n}⟩_{n∈ω} is generic, then ⟨G_{n}⟩_{n∈ω} is generic over G_{0}.

Proof. It suffices to show that, for all p forcing (D^{X_{0}} is dense in P^{X_{0}}), there exists q ≤ p forcing ∃r (r ∈ D^{X_{0}} and ⟨X_{n}⟩_{n∈ω} meets r).

Assume p ⊩ (D^{X_{0}} is dense in P^{X_{0}}). Since p ⊩ p ∈ P^{X_{0}}, it follows that p ⊩ ∃q (q ≤ p and q ∈ D^{X_{0}}). Fix p′ ≤ p and q′ ≤ p such that p′ ⊩ q′ ∈ D^{X_{0}}. Put S′ = {X_{0} : ⟨X_{n}⟩_{n∈ω} meets p′}. Then S′ is a Σ_{1}^{1} set, so let e ∈ ω be such that S′ = S_{e}. Claim 1: {(e, ⟨0⟩)} ⊩ q′ ∈ D^{X_{0}}. If not, let p′′ ≤ {(e, ⟨0⟩)} be such that p′′ ⊩ q′ ∉ D^{X_{0}}. Let π be a permutation such that π(0) = 0 and supp(p′) ∩ supp(π(p′′)) = {0}. Then p′ ∪ π(p′′) ∈ P and π(p′′) ⊩ q′ ∉ D^{X_{0}}, a contradiction. This proves Claim 1.

Claim 2: q′ ∪ {(e, ⟨0⟩)} ∈ P. To see this, let ⟨G′_{n}⟩_{n∈ω} be generic meeting {(e, ⟨0⟩)}. By Claim 1 we have q′ ∈ D^{G′_{0}}. Hence q′ ∈ P^{G′_{0}}, i.e., there exists ⟨X_{n}⟩_{n∈ω} meeting q′ with X_{0} = G′_{0}. Thus ⟨X_{n}⟩_{n∈ω} meets q′ ∪ {(e, ⟨0⟩)}. This proves Claim 2. Finally, put q′′ = q′ ∪ {(e, ⟨0⟩)}. Then q′′ ≤ q′ ≤ p and q′′ ⊩ (q′ ∈ D^{X_{0}} and ⟨X_{n}⟩_{n∈ω} meets q′). This proves our lemma. □

The proof of Theorem 1.3 is immediate from Lemmas 1.4 and 1.5.

2 Conservation Results

In this section we generalize the construction of §1 to a wider setting. We then use this idea to obtain some conservation results involving the scheme (∗) of Theorem 1.3.

Two important subsystems of second order arithmetic are ATR_{0} (arithmetical transfinite recursion with restricted induction) and Π_{∞}^{1}-TI_{0} (the transfinite induction scheme). For general background, see Simpson [5]. It is known [5, §VII.2] that ATR_{0} ⊆ Π_{∞}^{1}-TI_{0}, and that every β-model is a model of Π_{∞}^{1}-TI_{0}.

Let (N, S) be a countable model of ATR_{0}, where S ⊆ P (|N|). Define P_{(N,S)} = {p : (N, S) ⊧ (p is a finite subset of ω × ω^{<ω} and there exists ⟨X_{n}⟩_{n∈ω} meeting p)}. The notion of ⟨G_{n}⟩_{n∈|N|} being generic over (N, S) is defined in the obvious way. As in §1, the basic forcing lemmas can be proved. Let ⟨G_{n}⟩_{n∈|N|} be generic over (N, S). Put S′ = {G_{n} : n ∈ |N|}.

Lemma 2.1. (N, S′) satisfies the scheme (∗) of Theorem 1.3.

Proof. The proof is a straightforward generalization of the arguments of §1. □

Lemma 2.2. Let ψ be a Π_{2}^{1} sentence with parameters from |N|. If (N, S) ⊧ ψ, then (N, S′) ⊧ ψ.

Proof. Write ψ as ∀X (X ∈ S_{e}) for some fixed e ∈ |N|. If (N, S) ⊧ ψ, then for each n ∈ |N| we have that {p ∈ P_{(N,S)} : (e, ⟨n⟩) ∈ p} is dense in P_{(N,S)}, hence ∅ ⊩ X_{n} ∈ S_{e}. Thus ∅ ⊩ ∀X (X ∈ S_{e}), i.e., ∅ ⊩ ψ, so (N, S′) ⊧ ψ. □

Remark 2.3. Since (N, S) ⊧ ATR_{0} and ATR_{0} is axiomatized by a Π_{2}^{1} sentence, it follows by Lemma 2.2 that (N, S′) ⊧ ATR_{0}. Lemma 2.2 also implies that (N, S) and (N, S′) satisfy the same Π_{1}^{1} sentences with parameters from |N|. From this it follows that the recursive well orderings of (N, S) and (N, S′) are the same, and that HYP_{(N,S)} = HYP_{(N,S′)}. It can also be shown that HYP_{(N,S)} = S ∩ S′.

We now have:

Theorem 2.4. ATR_{0} + (∗) is conservative over ATR_{0} for Σ_{2}^{1} sentences.

Proof. Let φ be a Σ_{2}^{1} sentence. Suppose ATR_{0} ⊬ φ. Let (N, S) be a countable model of ATR_{0} + ¬ φ. Let S′ = {G_{n} : n ∈ |N|} as above. Since ¬ φ is a Π_{2}^{1} sentence, we have by Lemmas 2.1 and 2.2 that (N, S′) ⊧ ATR_{0} + (∗) + ¬ φ. Thus ATR_{0} + (∗) ⊬ φ. □

In order to obtain a similar result for Π_{∞}^{1}-TI_{0}, we first prove:

Lemma 2.5. (N, S′) ⊧ “all ordinals are recursive”, i.e., “every well ordering is isomorphic to a recursive well ordering”.

Proof. Recall from [5, §§VIII.3 and VIII.6] that all of the basic results of hyperarithmetical theory are provable in ATR_{0}. In particular, by [5, Theorem VIII.6.7], the Gandy/Kreisel/Tait Theorem holds in ATR_{0}. Thus for all p ∈ P_{(N,S)} we have

(N, S) ⊧ there exists ⟨X_{n}⟩_{n∈ω} meeting p such that ∀n (ω_{1}^{X_{n}} = ω_{1}^{CK}).

Now, it is provable in ATR_{0} that the predicate ω_{1}^{X} = ω_{1}^{CK} is Σ_{1}^{1}. Thus we have ∅ ⊩ ∀X (ω_{1}^{X} = ω_{1}^{CK}), i.e., ∅ ⊩ “all ordinals are recursive”. This proves our lemma. □

Remark 2.6. An alternative proof of Lemma 2.5 is to note that ATR_{0} + (∗) ⊢ “O does not exist”, because O would be definable but not hyperarithmetical. And “O does not exist” is equivalent over ATR_{0} to “all ordinals are recursive”. (Here O denotes the complete Π_{1}^{1} set of integers. See [5, §VIII.3].)

Theorem 2.7. Π_{∞}^{1}-TI_{0} + (∗) is conservative over Π_{∞}^{1}-TI_{0} for Σ_{2}^{1} sentences.

Proof. By Lemma 2.5 it suffices to prove: if (N, S) ⊧ transfinite induction for recursive well orderings, then (N, S′) ⊧ transfinite induction for recursive well orderings. Let e ∈ |N| be such that (N, S) ⊧ “<_{e} is a recursive well ordering”. Suppose p ⊩ ∃n (n ∈ field(<_{e}) and φ(n)). Put A = {n ∈ field(<_{e}) : p ⊮ ¬ φ(n)}. Clearly A ≠ ∅. By definability of forcing, A is definable over (N, S). Hence there exists a ∈ A such that (N, S) ⊧ “a is the <_{e}-least element of A”. For each n <_{e} a we have p ⊩ ¬ φ(n), but p ⊮ ¬ φ(a), so let q ≤ p be such that q ⊩ φ(a). Then q ⊩ “a is the <_{e}-least n such that φ(n)”. Thus (N, S′) ⊧ transfinite induction for recursive well orderings. □

Remark 2.8. Theorems 2.4 and 2.7 are best possible, in the sense that we cannot replace Σ_{2}^{1} by Π_{2}^{1}. An example is the Π_{2}^{1} sentence “all ordinals are recursive”, which is provable in ATR_{0} + (∗) but not in Π_{∞}^{1}-TI_{0}.

3 Recursion-Theoretic Analogs

The results of §§1 and 2 are in the realm of hyperarithmetical theory. We now present the analogous results in the realm of recursion theory, concerning models of WKL_{0}. For background on this topic, see Simpson [5, §§VIII.2 and XI.2].

Let REC denote the set of recursive reals. It is well known that, for any ω-model M of WKL_{0}, REC is properly included in M, and each X ∈ REC is definable in M. The recursion-theoretic analog of Theorem 1.1 is:

Theorem 3.1. There exists a countable ω-model of WKL_{0} satisfying

∀X (if X is definable, then X ∈ REC).

Proof. Use exactly the same construction and argument as for Theorem 1.1, replacing Σ_{1}^{1} sets by Π_{1}^{0} subsets of 2^{ω}. □

Remark 3.2. Theorem 3.1 is originally due to Friedman [2, Theorem 1.10, unpublished] (see also [3, Theorem 1.6]). It was later proved again by Simpson [6] (see also Simpson/Tanaka/Yamazaki [7]). All three proofs of Theorem 3.1 are different from one another.

Let ≤_{T} denote Turing reducibility, i.e., X ≤_{T} Y if and only if X is computable using Y as an oracle. The recursion-theoretic analog of Theorem 1.3 is:

Theorem 3.3. There exists a countable ω-model of WKL_{0} satisfying

(∗∗) ∀X ∀Y (if X is definable from Y, then X ≤_{T} Y).

Proof. Use exactly the same construction and argument as for Theorem 1.3, replacing Σ_{1}^{1} sets by Π_{1}^{0} subsets of 2^{ω}. □

The recursion-theoretic analog of Theorems 2.4 and 2.7 is:

Theorem 3.4. WKL_{0} + (∗∗) is conservative over WKL_{0} for arithmetical sentences.

Proof. The proof is analogous to the arguments of §2. □

Remark 3.5. Theorems 3.3 and 3.4 are originally due to Simpson [6]. The proofs given here are different from the proofs that were given in [6].

4 Some Additional Results

In this section we present some additional results and open questions.

Lemma 4.1. Let φ(X) be a Σ_{1}^{1} formula with no free set variables other than X. The following is provable in ATR_{0}. If ∃X (X ∉ HYP and φ(X)), then ∃P (P is a perfect tree and ∀X (if X is a path through P then φ(X))).

Proof. This is a well known consequence of formalizing the Perfect Set Theorem within ATR_{0}. See Simpson [5, §§V.4 and VIII.3]. See also Sacks [4, §III.6]. □

Lemma 4.2. Let φ(X) be a Σ_{2}^{1} formula with no free set variables other than X. The following is provable in ATR_{0} + “all ordinals are recursive”. If ∃X (X ∉ HYP and φ(X)), then ∃P (P is a perfect tree and ∀X (if X is a path through P then φ(X))).

Proof. Since φ(X) is Σ_{2}^{1}, we can write φ(X) ≡ ∃Y ∀f ∃n R(X[n], Y [n], f[n]) where R is a primitive recursive predicate. Let T_{X,Y} be the tree consisting of all τ such that ¬ (∃n ≤ lh(τ)) R(X[n], Y [n], τ[n]). For α < ω_{1}^{CK} put

φ_{α}(X) ≡ ∃Y (T_{X,Y} is well founded of height ≤ α).

Note that, for each α < ω_{1}^{CK}, φ_{α}(X) is Σ_{1}^{1}. Reasoning in ATR_{0} + “all ordinals are recursive”, we have ∀X (φ(X) if and only if (∃α < ω_{1}^{CK}) φ_{α}(X)). Thus Lemma 4.2 follows easily from Lemma 4.1. □

Theorem 4.3. Let T be ATR_{0} or Π_{∞}^{1}-TI_{0}. Let φ(X) be a Σ_{2}^{1} formula with no free set variables other than X. If T ⊢ ∃X (X ∉ HYP and φ(X)), then T ⊢ ∃P (P is a perfect tree and ∀X (if X is a path through P then φ(X))).

Proof. From Friedman [1] or Simpson [5, §VII.2], we have that T ⊢ the disjunction (1) all ordinals are recursive, or (2) there exists a countable coded β-model M satisfying T + “all ordinals are recursive”. In case (1), the desired conclusion follows from Lemma 4.2. In case (2), we have M ⊧ ∃X (X ∉ HYP and φ(X)), so the proof of Lemma 4.2 within M gives α < ω_{1}^{CK} such that M ⊧ ∃X (X ∉ HYP and φ_{α}(X)). It follows that ∃X (X ∉ HYP and φ_{α}(X)). We can then apply Lemma 4.1 to φ_{α}(X) to obtain the desired conclusion. □

Corollary 4.4. Let T and φ(X) be as in Theorem 4.3. If T ⊢ ∃X (X ∉ HYP and φ(X)), then T ⊢ ∀Y ∃X (φ(X) and ∀n (X ≠ (Y)_{n})).

Proof. This follows easily from Theorem 4.3. □

Theorem 4.5. Let T and φ(X) be as in Theorem 4.3. If T ⊢ (∃ exactly one X) φ(X), then T ⊢ ∃X (X ∈ HYP and φ(X)).

Proof. Consider cases (1) and (2) as in the proof of Theorem 4.3. In both cases it suffices to show that, for all α < ω_{1}^{CK}, if (∃ exactly one X) φ_{α}(X) then ∃X (X ∈ HYP and φ_{α}(X)). This follows from Lemma 4.1 applied to φ_{α}(X). □

Remark 4.6. Theorems 4.3 and 4.5 appear to be new. Corollary 4.4 has been stated without proof by Friedman [3, Theorems 3.4 and 4.4]. A recursiontheoretic analog of Corollary 4.4 has been stated without proof by Friedman [3, Theorem 1.7], but this statement of Friedman is known to be false, in view of Simpson [6]. A recursion-theoretic analog of Theorem 4.5 has been proved by Simpson/Tanaka/Yamazaki [7].

Question 4.7. Suppose WKL_{0} ⊢ ∃X (X ∉ REC and φ(X)) where φ(X) is Σ_{1}^{1}, or even arithmetical, with no free set variables other than X. Does it follow that WKL_{0} ⊢ ∃X ∃Y (X ≠ Y ∧ φ(X) ∧ φ(Y))? A similar question has been asked by Friedman [2, unpublished].

Question 4.8. Suppose WKL_{0} ⊢ (∃ exactly one X) φ(X) where φ(X) is Σ_{1}^{1} with no free set variables other than X. Does it follow that WKL_{0} ⊢ ∃X (X ∈ REC and φ(X))? If φ(X) is arithmetical or Π_{1}^{1} then the answer is yes, by Simpson/Tanaka/Yamazaki [7].

References

[1] Harvey Friedman. Bar induction and Π_{1}^{1}-CA. Journal of Symbolic Logic, 34:353–362, 1969.

[2] Harvey Friedman. Subsystems of second order arithmetic and their use in the formalization of mathematics. 19 pages, unpublished, March 1974.

[3] Harvey Friedman. Some systems of second order arithmetic and their use. In Proceedings of the International Congress of Mathematicians, Vancouver 1974, volume 1, pages 235–242. Canadian Mathematical Congress, 1975.

[4] Gerald E. Sacks. Higher Recursion Theory. Perspectives in Mathematical Logic. Springer-Verlag, 1990. XV + 344 pages.

[5] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999. XIV + 445 pages.

[6] Stephen G. Simpson. Π_{1}^{0} sets and models of WKL_{0}. April 2000. Preprint, 26 pages, to appear.

[7] Stephen G. Simpson, Kazuyuki Tanaka, and Takeshi Yamazaki. Some conservation results for weak König’s lemma. February 2000. Preprint, 26 pages, to appear.