1. Introduction
The separation problem was introduced in descriptive set theory by Luzin [
1]. In modern terms, the separation principle—or simply
Separation, for a given projective (boldface) class
or
—is the assertion that
Boldface Separation for
or : any pair of disjoint , resp, sets of reals can be separated by a set.
Accordingly,
the classical separation problem is a question of whether
Boldface Separation holds for this or another projective class
or
. Luzin and then Novikov [
2] underlined the importance and difficulty of this problem. (See [
3,
4,
5] for details and further references).
Luzin [
1,
6] and Novikov [
7] proved that
Boldface Separation holds for
but fails for the dual class
. Somewhat later, it was established by Novikov [
8] that the picture changes at the next projective level:
Boldface Separation holds for
but fails for
.
As for the higher levels of projective hierarchy, all attempts made in classical descriptive set theory to solve the separation problem above the second level did not work, until some additional set theoretic axioms were introduced—in particular, those by Novikov [
2] and Addison [
9,
10]. Gödel’s
axiom of constructibility implies that, for any
,
Boldface Separation holds for
but fails for
—pretty similar to second level.
In such a case, it is customary in modern set theory to look for models in which the separation problem is solved differently than under for at least some projective classes and , . This goal is split into two different tasks:
- (I)
Prove the independence of the -side Boldface Separation—that is, given , find models in which Boldface Separation fails for the class ;
- (II)
Prove the consistency of the -side Boldface Separation—that is, given , find models in which Boldface Separation holds for the class .
As for
models, we focus here only on
generic extensions of the constructible universe . Other set theoretic models, e.g., those based on strong determinacy or large cardinal hypotheses, are not considered in this paper. (We may only note in brackets that, by Addison and Moschovakis [
11], and Martin [
12], the
axiom of projective determinacy implies that, for any
, the separation problem is solved affirmatively for
and
and negatively for
and
—similar to what happens at the first and second level corresponding to
in this scheme. See also Steel [
13,
14], and Hauser and Schindler [
15] for some other relevant results.).
Problems (I) and (II) have been well-known since the early years of forcing, e.g., see problem P3030, and especially P3029 (= (II) for
) in a survey [
16] by Mathias.
Two solutions for part (I) are known so far. Harrington’s two-page handwritten note ([Addendum A1] [
17]) contains a sketch of a model, without going into details, defined by the technique of almost-disjoint forcing of Solovay and Jensen [
18], in which indeed
Separation fails for both
and
for a given
n. This research was cited in Moschovakis [
3] (Theorem 5B.3), and Mathias [
16] (Remark P3110 on page 166), but has never been published or otherwise detailed in any way. Some other models, with the same property of failure of
Separation for different projective classes, were recently defined and studied in [
5,
19].
As for (II), the problem as it stands is open so far, and no conclusive achievement, such as a model (a generic extension of
) in which
Boldface Separation holds for
for some
, is known. Yet, the following modification turns out to be easier to work with. The
effective or
lightface Separation, for a given lightface class
or
(we give [
3] as a reference on the lightface projective hierarchy), is the assertion that
Lightface Separation for or : any pair of disjoint , respectively, sets can be separated by a set—here, unlike the Boldface Separation case, the sets can be either sets of reals or sets of integers.
Accordingly, the
effective or
lightface separation problem is a question of whether
Lightface Separation holds for this or another class of the form
or
, with specific versions for sets of reals and sets of integers. Addison [
9,
10] demonstrated that, similar to the above,
Lightface Separation holds for
and
; fails for
and
; and under the axiom of constructibility
, it holds for
and fails for
for all
—both in the “real” and the “integer” versions. (See also [
3]).
In this context, Harrington announced in [
17] that there is a model in which
Lightface Separation holds both for the class
for sets of integers, and for the class
for sets of integers. A two-page handwritten sketch of a construction of such a model is given in ([Addendum A3] [
17]) without much elaboration of arguments.
The goal of this paper is to prove the next theorem, which generalizes the cited Harrington result and thereby is a definite advance in the direction of (II) in the context of
Lightface Separation for sets of integers. This is the main result of this paper.
Theorem 1. Let . There is a generic extension of in which
- (i)
Lightface Separationholds for sets of integers, so that any pair of disjoint sets can be separated by a set;
- (ii)
Lightface Separationalso holds for sets of integers, so that any pair of disjoint sets can be separated by a set.
Our proof of this theorem will follow a scheme that includes both some arguments outlined by Harrington in [
17], Addendum A3 (mainly related to the most elementary case
) and some arguments absent in [
17], in particular, those related to the generalization to the case
. (We may note here that [
17] is neither a beta-version of a paper, nor a preprint of any sort, but rather handwritten notes to a talk in which omissions of even major details can be expected.) All this will require both a fairly sophisticated construction of the model itself and a fairly complex derivation of its required properties by rather new methods for modern set theoretic research. Thus, we are going to proceed with filling-in all necessary details left aside in [
17]. We hope that the detailed acquaintance with the set theoretic methods first introduced by Harrington will serve to the benefits of the reader envisaged.
To prove Theorem 1, we make use of a generic extension of
defined in our earlier paper [
20] (and before that in [
17]—modulo some key details absent in [
17]) in order to prove the consistency of the equality
for a given
. (The equality claims that the constructible reals are the same as
reals. Its consistency was a major problem posed by Harvey Friedman [
21].) We present the construction of this generic model in all necessary detail.
This includes a version of almost-disjoint forcing considered in
Section 2, the cone-homogeneity lemma in
Section 3, the systems and product forcing construction in
Section 4, and a Jensen–Solovay-style construction of the actual countable support forcing product
in
Section 5. Theorem 2 and Definition 2 in
Section 5 present the construction of
in
via the union of a
-long increasing sequence of systems
,
, which satisfies suitable completeness and definability requirements (that depend on the choice of the value of an integer 𝕟 as in Theorem 1), and also follows the Jensen–Solovay idea of Cohen-generic extensions at each step
of the inductive construction of
.
Then, we consider corresponding
-generic extensions
in
Section 6, and their subextensions involved in the proof of Theorem 1 in
Section 7 (Theorem 4). Two key lemmas are established in
Section 8, and the proof of theorems 4 and 1 is finalized in
Section 9 (the
case) and in
Section 10 (the
case).
The final section on conclusions and discussion completes the paper.
2. Almost-Disjoint Forcing
Almost-disjoint forcing was invented by Jensen and Solovay [
18]. Here, we make use of a
-version of this tool considered in ([
Section 5] [
18]). The version we utilize here exactly corresponds to the case
developed in our earlier paper [
20] (and to less extent in [
22]). This will allow us to skip some proofs below. Assume the following:
, the first uncountable ordinal in .
= all -sequences of ordinals in .
is the set of all sequences of ordinals , of length .
By definition, the sets , belong to and whereas in . Note that , the empty sequence, does not belong to .
A set is dense iff for any there is such that .
If ; then, let .
If is unbounded in , then say that S covers f; otherwise, S does not cover f.
The general goal of the almost-disjoint forcing is the following: given a set in the ground set universe , find a generic set such that the equivalence “” holds for each in the ground universe.
Definition 1. is the set of all pairsof finite sets , . Note that . Elements of are called (forcing) conditions.
If , then put ; this is a tree in .
Let. Define(that is, q is stronger as a forcing condition) iff , and the difference does not intersect , i.e., . Clearly, we have iff , and .
If , then put .
Lemma 1 (Lemma 1 in [
20])
. Conditions are compatible in iff does not intersect , and does not intersect . Thus, any conditions are compatible in iff are compatible in iff the condition satisfies and .
3. The Almost-Disjoint Forcing Notions
Are Homogeneous
We are going to show that forcing notions of the form
are sufficiently homogeneous. This is not immediately clear here, unlike the case of many other homogeneity claims. Assume that conditions
satisfy the next requirement:
Then, a transformation acting on conditions is defined as follows.
If , then define for all , the identity.
Suppose that
. Then,
are incompatible by (
1) and Lemma 1. Define
, the
domain of
. Let
. We put
, where
and
In this case, the difference between
and
is located within the set
, so that
and
whenever
, while
and
whenever
. The next lemma is Lemma 6 in [
20].
Lemma 2. (i)
If is dense and , then there exist conditions with ,
, satisfying (
1).
- (ii)
Letsatisfy (1). If, thenis the identity transformation. If, thenis an order automorphism of, satisfyingand.
- (iii)
Ifandsatisfy (1), thenmaps the setonto itself order-preserving.
Proof (sketch). (i) By the density of u, there is a countable set satisfying and . Put and . Claims (ii) and (iii) are routine. □
Corollary 1 (in
).
If a set is dense, then is cone homogeneous in the sense of [
23]
, i.e., if , then there exist conditions with , , such that the cones and are order-isomorphic. 4. Systems and Product Almost-Disjoint Forcing
To prove Theorem 1, we make use of a forcing notion equal to the countable-support product of a collapse forcing ℂ and -many forcing notions of the form , .
We work in . Define , the set of all finite sequences of subsets of in , an ordinary forcing to collapse down to .
Let and , the index set of the mentioned product. Let a system be any map such that , each set () is dense in , and the components are pairwise disjoint.
Given a system U in , we let be the finite-support product of ℂ and the sets , . That is, consists of all maps p defined on a finite set so that for all , and if , then . If , then put and for all , so that .
We order component-wise: (p is stronger as a forcing condition) iff , in case , and in for all . Note that contains the empty condition satisfying ; obviously, ⊙ is the -least (and weakest as a forcing condition) element of .
Lemma 3 (in ). If U is a system, then the forcing notion satisfies -CC.
Proof. We argue in . Assume towards the contrary that is an antichain of cardinality . As , we can assume that for all . Consider the set ; it consists of finite subsets of .
Case 1: . Then, by the cardinality argument, there is a set and some such that for all and still . Note that if belongs to , then by the above; therefore, as are incompatible, we have . Thus, still satisfies . This is a contradiction since obviously the set has cardinality .
Case 2:
. Then, by the
-system lemma (see e.g., Lemma 111.2.6 in Kunen [
24]) there is a set
and a finite set
(the root) such that
for all
in
, and still
. For any
, pick a condition
with
; then,
still satisfies
. By construction, if
belong to
, then
and
are incompatible; hence, the restricted conditions
,
are incompatible as well. Thus, the set
still has cardinality
and is an antichain. On the other hand,
for all
. Therefore, we have a contradiction as in Case 1. □
5. Jensen–Solovay Construction
Our plan is to define a system such that any -generic extension of has a subextension that witnesses Theorem 1. Such a system will be defined in the form of a component-wise union of a -long increasing sequence of small systems, where the smallness means that, in , the system involves only -many functions in .
We work in .
A system U is small, if both and each set has cardinality .
If are systems, , and for all , then say that V extends U, in symbol .
If is a -increasing sequence of systems, then define a system by and for all .
We let
be
minus the Power Set axiom, with the schema of Collection instead of Replacement, with
AC in the form of the well-orderability principle, and with the axiom: “
exists”. See [
25] on versions of
sans the Power Set axiom in detail. Let
be
plus the axioms:
, and the axiom “every set
x satisfies
”.
Let be systems. Suppose that M is any transitive model of containing . Define iff and the following holds:
- (a)
the set is multiply -generic over M, in the sense that every sequence of pairwise different functions is generic over M in the sense of as the forcing notion in , and
- (b)
if , then the set is dense in , and therefore uncountable.
Note a corollary of (a): .
Let , Jensen–Solovay pairs, be the set of all pairs , where is a transitive model containing and is a system. Then, the sets also belong to M.
Let , small Jensen–Solovay pairs, be the set of all pairs such that U is a small system in the sense above and (in ).
( extends ) iff and ;
(strict) iff and .
A Jensen–Solovay sequence of length is any strictly -increasing -sequence of pairs , satisfying on limit steps. Let be the set of all such sequences.
A pair solves a set iff either or there is no pair that extends .
Let be the set of all pairs , whichsolve a given set .
Let . A sequence is -complete iff itintersects every set of the form , where is a set.
Recall that is the collection of all sets x whose transitive closure has cardinality . Further, means definability by a formula of the -language, in which any definability parameters in are allowed, while means the parameter-free definability. Similarly, in the next theorem means that is allowed as a sole parameter. It is a simple exercise that sets and are under . To account for as a parameter, note that the set is ; hence, the singleton is .
Generally, we refer to, e.g., [
26], Part B, 5.4, or [
27], Chap. 13, on the Lévy hierarchy of ∈-formulas and definability classes
for any transitive set
H.
Theorem 2 (Theorem 3 in [
20]).
It is true in that if , then there is a sequence of class ; hence, in case , and in addition -complete in case , such that for all . Similar theorems were established in [
28,
29,
30] for different purposes.
Definition 2 (in
)
. Fix a numberduring the following proof of Theorem 1.
Letbe any Jensen–Solovay sequence as in Theorem 2—that is,
- (i)
the sequence is of class,
- (ii)
we havefor all ξ;
- (iii)
if, then the sequence is-complete.
Put, sofor all. Thus,is a system andsincefor all ξ.
We define(thebasic forcing notion).Thus,is the finite-support product of the set ℂ and sets.
Lemma 4 (in ). The binary relation is .
Proof. Make use of (i) of Definition 2. □
6. Basic Generic Extension
We consider
(see Definition 2) as a forcing notion in
. Accordingly, we will study
-generic extensions
of the ground universe
. Define some elements of these extensions. Suppose that
. Let
for any
, where
. Thus,
.
Therefore, any -generic set splits into the family of sets , and a separate map . It follows from Lemma 3 by standard arguments that -generic extensions of satisfy .
Lemma 5 (Lemma 9 in [
20])
. Let be a set -generic over . Then,- (i)
is a-generic map from ω onto
- (ii)
if, then the setis-generic over—hence, if, theniff
Now suppose that
. If
, then a
restriction is defined by
and
for all
. In particular, if
, then let
If , then let (= in case ).
Put .
Writing , it is not assumed that .
The proof of Theorem 1 makes use of a generic extension of the form , where is a set -generic over and .
Define formulas
(
) as follows:
Lemma 6 (Lemma 22 in [
20])
. Suppose that a set is -generic over and , . Then, and- (i)
holds;
- (ii)
—generally, there are no sets insatisfying
- (iii)
if, then, and if, then.
The next key theorem is Theorem 4 in [
20]. Note that if
, then the result is an easy corollary of the Shoenfield absoluteness theorem.
Theorem 3 (elementary equivalence theorem). Assume that in , , sets satisfy and , the symmetric difference is at most countable and the complementary set is infinite.
Let be -generic over , and be any real.
Then, any closed formula φ, with real parameters in , is simultaneously true in the models and .
7. The Model
Here, we introduce a submodel of the basic
-generic extension
defined in
Section 6 that will lead to the proof of Theorem 1.
Recall that a number is fixed by Definition 2.
Under the assumptions and notation of Definition 2, consider a set
,
-generic over
. Then,
is a
-generic map from
onto
by Lemma 5 (i). We define
and
. We also define, for any
,
and accordingly,
and
.
With these definitions, each
kth slice
of
is necessarily infinite and coinfinite, and it codes the target set
since
Note that definition (
3) is
monotone w.r.t. ,
i.e., if
for all
k, then
and
. Anyway,
(the ordinal product) is a set in the model
for each
m, whereas
for all
m. Finally, let
Recall that if , then .
To prove Theorem 1, we consider the model .
Theorem 4. If G is a -generic set over , then the class suffices to prove Theorem 1. That is, Lightface Separationholds in both for sets of integers and for sets of integers.
The proof will include several lemmas.
For the next lemma, we let be the -forcing notion defined in . If and , then let . This can be identified with just , of course, but formally . If , then let (the empty condition). Let be the canonical -name for the generic set , be a name for the set , and be a canonical -name for .
Lemma 7 (reduction to the ℂ-component).
Let and let be a closed formula containing only and names for sets in as parameters. Assume thatThen, as well.
Proof. By the product forcing theorem, if
is
-generic over
, then the model
is a
-generic extension of
, where
is a forcing in
. However, it follows from Corollary 1 that
is a (finite-support) product of cone-homogeneous forcing notions. Therefore,
itself is a cone homogeneous forcing, and we are finished (see e.g., Lemma 3 in [
23] or Theorem IV.4.15 in [
24]). □
8. Two Key Lemmas
The following two lemmas present two key properties of models of the form involved in the proof of Theorem 4. The first lemma shows that all constructible reals are in such a model.
Lemma 8. Let a set be -generic over . Then, it holds in that is and each set is
Proof. Consider an arbitrary ordinal
;
. We claim that
holds in
. Indeed, assume that
. Then,
, and we have
in
by Lemma 6 (iii),(i). Conversely, assume that
. Then, we have
, but
contains no
S with
by Lemma 6 (ii).
However, the right-hand side of (
6) defines a
relation in the model
by Lemma 4. (Indeed, we have
in
; therefore,
is
in
). On the other hand, the sets
and
remain
singletons in
; they can be eliminated since
. This yields
in
. It follows that
in
by Lemma 25.25 in [
27], as required.
Now, let
. By genericity, there exists
such that
. Then,
by (
3); therefore,
x is
as well. However,
by the same argument. Thus,
x is
in
, as required. □
The proof of the next lemma involves Theorem 3 above as a key reference. The lemma holds for by Shoenfield.
Lemma 9. Suppose that is -generic over , , , . Then, any closed formula Φ, with reals in as parameters, is simultaneously true in and in .
It follows that if in , then any closed formula Ψ, with parameters in , true in , is true in the model as well.
Proof. There is an ordinal such that all parameters in belong to , where and . The set Y belongs to ; in fact, . Therefore, is equi-constructible with the pair . Here, is a map from onto . It follows that there is a real with . Then, all parameters of belong to .
To prepare an application of Theorem 3 of
Section 6, we put
It is easy to check that all requirements of Theorem 3 for these sets are fulfilled. Moreover, as
, we have
; hence,
. Therefore, we conclude by Theorem 3 that the formula
is simultaneously true in
and in
. However,
by construction, while
, and we are done. □
9. Finalization: Case
Here, we finalize the proof of Theorems 4 and 1 w.r.t.
sets of integers. We generally follow the line of arguments sketched by Harrington ([Addendum A3] [
17]) for the
case, with suitable changes mutatis mutandis. We will fill in all details omitted in [
17].
Recall that a number is fixed by Definition 2. We assume that
- (∗)
a set is -generic over , sets belong to , and it holds in that are disjoint sets.
The goal is to prove that can be separated by a set and then argue that Z is by Lemma 8. Recall that . Suppose that
- (†)
and
are parameter-free
formulas that provide
definitions for the sets, respectively,
of (∗)—that is,
in
. The assumed implication
(as
) is forced to be true in
by a condition
.
Here, is the canonical -name for the generic set while is a name for the set .
We observe that is a parameter-free sentence. Therefore, it can w. l. o. g. be assumed that , by Lemma 7. In this case, the condition can be identified with its only nontrivial component .
Lemma 10 (interpolation lemma). Under the assumptions of (†), if , conditions satisfy and , and we have
and .
Then, .
Proof (sketched in ([Addendum A3] [
17]) for
).
First of all, by Lemma 7, we can w. l. o. g. assume that
; so, the components
and
satisfy
and
in
ℂ.
We w. l. o. g. assume that the tuples
have the same length
. (Otherwise, extend the shorted one by a sufficient number of new terms equal to
⌀). Define another condition
such that
and
for all
. Accordingly, define
so that
and
. Despite that
q may well be incomparable with
in
, we claim that
To prove the
-part of (
7), let
be a set
-generic over
, and
. Then,
. We have to prove that
holds in
.
Define another generic set , slightly different from H, so that
- (A)
for all ;
- (B))
; and
- (C)
if , then .
In other words, the only difference between K and H is that but .
It follows that
; hence,
holds in
by the assumptions of the lemma. Now, we note that by definition,
Here, the sets
and
satisfy
(since
for all
). In addition,
(since
for all
). To conclude,
and
. On the other hand, it follows from (A) that
for any
, whereas
and
are recursively reducible to each other by (B),(C). Therefore,
by (
8). However,
holds in this model by the above. It follows by Lemma 9 that
holds in
as well. (Harrington circumvents Lemma 9 in [
17] by a reference to the Shoenfield absoluteness theorem.) We are finished.
After (
7) has been established, we recall that
in
by construction. It follows that
by the choice of
(see (†) above). □
Proof of Theorems 4 and 1:case). We work under the assumptions of (∗) and (†) above. Consider the following sets in
:
Note that by Lemma 10. On the other hand, it is clear that and by (†). Thus, either of the two sets separates x from y. It remains to apply Lemma 8. □
10. Finalization: Case
This will be a mild variation of the argument presented in the previous section.
Proof of Theorems 4 and 1:case, sketch. Emulating (∗) and (†) above, we assume that a set is -generic over , and are disjoint sets in , defined by parameter-free formulas, respectively, and . The implication is forced to hold in by a condition satisfying . The proof of Lemma 10 goes on for formulas the same way, with the only difference that we define for . Yet, this is compatible with the application of Lemma 9 because now, are formulas. □
11. Conclusions and Discussion
In this study, the method of almost-disjoint forcing was employed to the problem of obtaining a model of
in which the
Separation principle holds for lightface classes
and
, for a given
, for sets of integers. The problem of obtaining such models has been generally known since the early years of modern set theory, see, e.g., problems 3029 and 3030 in a survey [
16] by Mathias. Harrington ([
17], Addendum A3) claimed the existence of such models; yet, a detailed proof has never appeared.
From our study, it is concluded that the technique developed in our earlier paper [
20] solves the general case of the problem (an arbitrary
) by providing a generic extension of
in which the
Lightface Separation principle holds for classes
and
, for a given
, for sets of integers, for a chosen value
.
From this result, we immediately come to the following problem:
Problem 1. Define a generic extension of in which theLightface Separation principle holds for classes and , for all, for sets of integers.
The intended solution is expected to be obtained on the basis of a suitable product of the forcing notions
,
, defined in
Section 6.
And we recall the following major problem.
Problem 2. Given, define a generic extension ofin which the Separation principle holds for the classesandforsets of reals.
The case of sets of reals in the Separation problem is more general, and obviously much more difficult, than the case sets of integers.