This paper constructs a model of ZFC where every non-empty analytically definable set of reals contains an analytically definable real, yet there is no analytically definable wellordering of the continuum, showing the full basis theorem does not imply analytic wellordering.
Contribution
It demonstrates that the full basis theorem does not necessarily lead to an analytically definable wellordering of the continuum by constructing a specific model.
Findings
01
Every non-empty lightface analytically definable set of reals contains an analytically definable real.
02
There is no analytically definable wellordering of the continuum in the constructed model.
03
The model uses a finite support product of Jensen minimal $oldsymbol{
m extPi^1_2}$ singleton forcing.
Abstract
We make use of a finite support product of ω1 clones of the Jensen minimal Π21 singleton forcing to obtain a model of ZFC in which every non-empty lightface analytically definable set of reals contains a lightface analytically definable real (the full basis theorem), but there is no analytically definable wellordering of the continuum.
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Full text
The full basis theorem does not imply analytic wellordering
Vladimir Kanovei
IITP RAS and MIIT, Moscow, Russia, [email protected] —
contact author.Thankful the Department of Philosophy, Linguistics and Theory of
Science at the University of Gothenburg and
the Erwin Schrodinger International Institute for
Mathematics and Physics (ESI) at Vienna
for their hospitality and support in resp. May 2015 and
December 2016.
Vassily Lyubetsky
IITP RAS, Moscow, Russia, [email protected] in part by RNF Grant #14-50-00150.
(2 \acctonos 2024)
Abstract
We make use of a finite support product of ω1 clones
of the Jensen minimal Π21 singleton forcing to
define a model in which every non-empty
lightface analytically definable
set of reals contains a lightface analytically definable real
(the full basis theorem),
but there is no lightface analytically definable wellordering of the continuum.
The uniformization problem, introduced by Luzin
[22, 23],
as well as the related basis problem,
are well known in modern set theory.
(See Moschovakis [24], Kechris [21],
Hauser and Schindler [7] for
both older and more recent studies.)
In particular, it is known that every non-empty
Σ21 set of reals contains a Δ21 real,
but on the other hand,
it is consistent that there exists a non-empty Π21 set
of reals containing even no ordinal-definable real.
The negative part of this result was strengthened in
[19] to the
effect that the counter-example set X⊆ωω is a
Π21E0-equivalence class (hence, a countable set),
see related discussions at the Mathoverflow
exchange desk 111
A question about ordinal definable real numbers.
Mathoverflow, March 09, 2010.
http://mathoverflow.net/questions/17608.
and at FOM 222 Ali Enayat. Ordinal definable numbers. FOM Jul 23, 2010.
http://cs.nyu.edu/pipermail/fom/2010-July/014944.html.
Recall that E0 is an equivalence relation on ωω defined
so that xE0y iff x(n)=y(n) for all but finite n.
As for the positive direction, the most transparent way to
get a basis result is to make use of an analytically definable
wellordering < of the reals,
which enables one to pick the <-least
real in each non-empty set of reals.
This leads to the question:
is the existence of an analytically definable
wellordering < of the reals independent of the basis theorem.
We answer it in the positive:
Theorem 1.1**.**
In a suitable generic extension of L,
it is true that in which every non-empty
lightface analytically definable
set of reals contains a lightface analytically definable real
(the full basis theorem),
but there is no lightface analytically definable
wellordering of the continuum.
More precisely, there is a cardinal-preserving generic
extension L[X] of L, such that
X=⟨xξk⟩ξ<ω1L∧k<ω, where each
xξk is a real in 2ω, and in addition
(I)
if m<ω then the submodel L[Xm] admits a
Δm+31 wellordering of the reals
of length ω1, where
Xm=⟨xξk⟩ξ<ω1L∧k<m;
2. (II)
if m<ω then ωω∩L[Xm] is a
Σm+31 set in L[x];
3. (III)
if m<ω then L[Xm] is an
elementary submodel of L[x]w. r. t. all Σm+21 formulas with reals in
L[Xm] as parameters*;***
4. (IV)
it is true in L[X] that there is no
lightface analytically definable wellordering
of the reals*.***
To see that the additional claims imply the main claim
(the full basis theorem),
let, in L[X], Z⊆ωω be a non-empty Σm+21
set of reals.
Then Z′=Z∩L[Xm] is a Σm+31 set by (II),
and Z′=∅ by (III).
It remains to pick the least real in Z′ in the sense of
the lightface Δm+31 wellordering given by (I).
2 Comments
To prove the theorem, we define, in L, a system of
forcing notions Pξk, ξ<ω1 and k<ω,
whose finite-support product P=∏ξ,kPξk
adds an array X=⟨xξk⟩ξ<ω1,k<ω of reals
xξk to L, such that
(I), (II), (III), (IV) hold in L[X].
Regarding the history of this research, in goes down to
Jensen [10], where a forcing
J=⋃α<ω1Jα is defined in L,
the constructible universe, such that each Jα is
a countable set of perfect trees in 2<ω, the
canonical J-generic real is a single J-generic
real in the extension, and ‘being a J-generic real’
is a Π21 property, so as a result we get a Π21
nonconstructible singleton in any J-generic
extension of L.
See 28A in [8] for a more modern exposition of
Jensen’s forcing.
A nonconstructible Π21
singleton also was defined in [9] by
means of the almost-disjoint forcing, yet the construction in
[10] has the advantage of
minimality of J-generic reals
and some other advantages
(as well as some disadvantages).
Jensen’s forcing construction (including its iterations)
was exploited by Abraham [1, 2], including a
definable minimal collapsing real.
Another modification of Jensen’s forcing construction in
[11] yields such a forcing notion in L that
any extension of L, containing two generic reals
x=y, necessarily satisfies ω1L<ω1.
See [3, 15] on some other modifications in
coding purposes.
A different modification of Jensen’s forcing construction
was engineered in [16] in order to define an
extension of L in which, for a given n≥2, there
is a nonconstructible Πn1 singleton while all Σ21
reals are constructible.
(An abstract appeared in [14].)
The idea is to complicate the inductive construction of
Jensen’s sequence J=⟨Jα⟩α<ω1 in L
by the requirement that it intersects any set,
of a certain definability level,
dense in the collection of all possible countable
initial steps of the construction.
The same inner genericity idea, with respect to the
Jensen – Johnsbraten forcing notion in [11],
was developed in [18].
Such an inner genericity modification of the
Jensen – Solovay almost-disjoint forcing [9]
was developed in [6] towards some great results
which unfortunately have never been published in a
mathematical journal.
Except for a one result, a model in which the set of
all analytically definable reals is equal to the set
of all constructible reals, independently obtained in
[17].
We employ the inner definable genericity idea
here in such a way that if m<ω
then the m-tail
⟨Pξk⟩ξ<ω1∧k≥m of the
forcing construction, bears an amount of inner definable
genericity which strictly depends on m.
(See Definition 2.1, where a key concept is
introduced.)
Ali Enayat (Footnote 2) conjectured that
some definability questions can be solved by
finite-support products of Jensen’s [10]
forcing J.
Enayat demonstrated in [4]
that a symmetric part of the Jω-generic
extension of L
definitely yields a model of ZF
(not a model of ZFC!)
in which there is a Dedekind-finite infinite Π21 set of
reals with no OD elements.
Following the conjecture, we proved in [12] that
indeed it is true in a Jω-generic extension
of L that the set of J-generic reals is
a countable non-empty Π21 set with no OD elements.
We also proved in [13] that the existence of a
Π21E0-class with no OD elements is consistent
with ZFC, using a E0-invariant version of Jensen’s
forcing.
We further employed another finite-support product of Jensen’s
forcing to define a generic extension of L where
there is a Π21 set P⊆ωω×ωω which has countable
cross-sections Px={y:\linebreak[0]⟨x,y⟩∈P} and is
non-uniformizable by any projective set
[20].
Acknowledgement**.**
The idea of making use of a suitable finite-support product
of Jensen-like forcing notions in order to obtain a model,
in which the full basis theorem holds
but there is no lightface analytically definable
wellordering of the continuum,
was communicated to an author of this paper (VK)
by Ali Enayat in 2015, and
we thank Ali Enayat for fruitful discussions and helpful
ideas.
3 The structure of the paper
The general organization of the paper is as follows.
Chapter I contains a general formalism
related to forcing by perfect trees and finite-support
products, convenient for our goals.
Following Jensen [10],
we consider forcing notions of the form
P=⋃α<λPα, where λ<ω1 and
each Pα is a countable set of perfect trees
in 2<ω.
Each term Pα has to satisfy some routine
conditions of refinement with respect to the
previous terms, in particular, to make sure that
each Pα remains pre-dense at further steps.
Also, each Pα has to lock some dense sets
in ⋃ξ<αPξ so that they
remain pre-dense at further steps as well.
And this procedure has to be extended from single
forcing notions to their finite-support products.
These issues are dealt with in Chapter II.
Then we consider real names with respect to
finite-support products of perfect-tree forcing
notions in Chapter III.
Here the key issue is to make sure that if P
is a factor in a product forcing considered then
there is no other P-generic real in the whole
product extension except for the obvious one.
In Chapter IV
we define the forcing notion
P=∏ξ<ω1,k<ωPξk
to prove the main theorem, in the form of a limit
of a certain increasing sequence of countable
products of countable perfect-tree forcing notions.
Quite a complicated construction of this sequence
in L involves ideas related
to diamond-style constructions,
as well as to some sort of definable genericity,
as explained above.
The forcing P is not analytically definable;
basically, each k-th layer
⟨Pξk⟩ξ<ω1 belongs to Δk+41.
But it is a key property that the P-forcing
relation restricted to Σn1 formulas is essentially
Σn1.
We prove this in Chapter V, with the help of
an auxiliary forcing notion forc.
We also establish the invariance of forc with respect to
countable-support permutations of ω1×ω.
We finally prove Theorem 1.1 in
Chapter VI, on the base of the results
obtained in two previous chapters.
I Basic constructions
We begin with some basic things:
perfect trees in the Cantor space 2ω,
perfect tree forcing notions
(those which consist of perfect trees),
their finite-support products, and a
splitting construction of perfect trees.
1 Perfect trees
Let 2<ω be the set of all strings (finite sequences)
of numbers 0,1.
If t∈2<ω and i=0,1 then
t⌢k is the extension of t by k.
If s,t∈2<ω then s⊆t means that t extends s, while
s⊂t means proper extension.
If s∈2<ω then lh(s) is the length of s,
and 2n={s∈2<ω:\linebreak[0]lh(s)=n} (strings of length n).
A set T⊆2<ω is a tree iff
for any strings s⊂t in 2<ω, if t∈T then s∈T.
Every non-empty tree T⊆2<ω contains the empty
string Λ.
If T⊆2<ω is a tree and s∈T then put
T↾s={t∈T:\linebreak[0]s⊆t∨t⊆s}.
Let PT be the set of all perfect trees
∅=T⊆2<ω.
Thus a non-empty tree T⊆2<ω belongs to PT iff
it has no endpoints and no isolated branches.
Then there is a largest string s∈T such that
T=T↾s; it is denoted by s=stem(T)
(the stem of T);
we have s⌢1∈T and s⌢0∈T in this case.
Definition 1.1** (perfect sets).**
If T∈PT then
[T]={a∈2ω:\linebreak[0]∀n(a↾n∈T)}
is the set of all paths through T,
a perfect set in 2ω.
Conversely if X⊆2ω is a perfect set then
tree(X)={a↾n:\linebreak[0]a∈X∧n<ω}∈PT
and [tree(X)]=X.
Trees T,S∈PT are almost disjoint, a. d.
for brevity, iff
the intersection S∩T is finite;
this is equivalent to just [S]∩[T]=∅.
∎
The simple splitting of a tree T∈PT consists
of smaller trees
[TABLE]
in PT, so that [T(→i)]={x∈[T]:\linebreak[0]x(h)=i},
where h=lh(stem(T)).
We let
[TABLE]
for each string u∈2<ω,\linebreak[0]lh(u)=n;
and separately T(→Λ)=T.
Lemma 1.2**.**
Suppose that T∈PT.
Then:
(i)
if u∈2<ω then there is a string s∈2<ω such that
T(→u)=T↾s;
2. (ii)
if s∈2<ω then there is a string u∈2<ω
such that T↾s=T(→u);
3. (iii)
if ∅=U⊆[T]
is a (relatively) open subset of [T], or at least
U has a non-empty interior in [T], then
there is a string s∈T such that T↾s⊆U.
∎
If T∈PT and a∈2ω then the intersection
T(→a)=⋂n<ωT(→a↾n)={hT(a)}
is a singleton, and the map hT is a
canonical homeomorphism from 2ω onto [T].
Accordingly if S,T∈PT then the map
hST(x)=hT(hS−1(x)) is a
canonical homeomorphism from [S] onto [T].
2 Perfect tree forcing notions
A perfect-tree forcing notion is any non-empty set
P⊆PT such that if s∈T∈P then T↾s∈P,
or equivalently, by Lemma 1.2,
if u∈2<ω then T(→u)∈P.
Let PTF be the set of all such forcing notions
P⊆PT.
Example 2.1**.**
If s∈2<ω then the
tree [s]={t∈2<ω:\linebreak[0]s⊆t∨t⊆s}
belongs to PT.
The set Pcoh={[s]:\linebreak[0]s∈2<ω} of all such trees
(the Cohen forcing)
is a regular perfect-tree forcing notion.
∎
Lemma 2.2**.**
Let P∈PTF.
If T∈P and a set X⊆[T] is (relatively) open
(resp., clopen) in [T], then there is a countable
(resp., finite) set S of pairwise a. d. trees S∈P,
satisfying ⋃S∈S[S]=X.∎
Lemma 2.3**.**
(i)
If
s∈T∈P∈PTF then T↾s∈P.
2. (ii)
If P,P′∈PTF, T∈P, T′∈P′, then
there are trees S∈P, S′∈P′ such that
S⊆T, S′⊆T′, and [S]∩[S′]=∅.
Proof**.**
(i) use Lemma 1.2.
(ii)
If T=T′ then let S=T(→0),
S′=T(→1).
If say T⊆T′ then let s∈T∖T′,
S=T↾s, and simply S′=T′.
∎
Definition 2.4**.**
A set A⊆PT is an antichain iff any trees
T=T′ in A are a. d., that is,
[T]∩[T′]=∅.
A forcing notion P∈PTF is:
small,
if it is countable;
special,
if there is
an antichain A⊆P
such that P={T↾s:\linebreak[0]s∈T∈A} —
note that A
is unique if exists; we write
A=base(P) (the base of P);
regular,
if for any S,T∈P, the intersection
[S]∩[T] is clopen in [S] or clopen in [T]
(or clopen in both [S] and [T]).
∎
Lemma 2.5**.**
Let P∈PTF.
If P is special and
S,T∈P are not a. d., then they are comparable:S⊆T or T⊆S.
If P is special then P is regular.
If P is regular, then
(i)
if S,T∈P are not
a. d., then they are compatible in P, that is,
there is a tree R∈P such that R⊆S∩T.
2. (ii)
if
S1,…,Sk∈P then there is a finite set of
pairwise a. d. trees R1,…,Rn∈P such that
[S1]∩…∩[Sk]=[R1]∪…∪[Rn].
3. (iii)
if S1,…,Sk are
finite collections of trees in P then there
is a finite set of trees R1,…,Rn∈P such that
⋃S∈S1[S]∩…∩⋃S∈Sk[S]=[R1]∪…∪[Rn],
and for any Si and Rj,
there is S∈Si such that Rj⊆S.
Proof**.**
(iii)
Apply (ii) to every set of the form
[S1]∩…∩[Sk], where Si∈Si, ∀i,
then gather all
trees Ri obtained in one finite set.
∎
Remark 2.6**.**
Any set P∈PTF can be considered as a forcing notion
(if T⊆T′ then T is a stronger condition);
then P adds a real x∈2ω.
∎
Lemma 2.7**.**
If a set G⊆P is generic over a ground set universe
V(resp., over a transitive model, e. g. L)
then
(i)
the intersection ⋂T∈G[T] contains a
single real x=x[G]∈2ω, and
2. (ii)
*this real x is
P-generic,
*in the sense that if D⊆P is
dense in P and belongs to V(resp., to the ground model)
then x∈⋃T∈D[T].∎
As usual, a set D⊆P is:
−
open in P, if for any trees T⊆S in P,
T∈D⟹S∈D;
−
dense in P, if for any T∈P
there is S∈D, S⊆T;
−
pre-dense in P, if the set
D′={T∈P:\linebreak[0]∃S∈D(T⊆S)}
is dense in P.
3 Splitting construction
We proceed with an important splitting/fusion
construction of perfect trees by means of infinite
splitting systems of such trees.
Definition 3.1**.**
Let FSS be the set of all
finite splitting systems, that is,
systems of the form
φ=⟨Ts⟩s∈2≤n, where
n=hgt(φ)<ω (the height of φ),
each value Ts=Tsφ=φ(s) is a tree in PT, and
(∗)
if s∈2<n and i=0,1 (so s⌢i∈2≤n)
then Ts⌢i⊆Ts(→i) —
it easily follows that
[Ts⌢0]∩[Ts⌢1]=∅.
We add the empty systemΛ to FSS, with hgt(Λ)=−1.
∎
A tree Toccurs in φ∈FSS if
T=φ(s) for some s∈2≤hgt(φ).
If all trees occurring in φ belong to some P∈PTF then
say that φ is a finite splitting system
over P, symbolically φ∈FSS(P).
Let φ,ψ be systems in FSS.
Say that
φextendsψ, symbolically ψ≼φ, if
n=hgt(ψ)≤hgt(φ) and ψ(s)=φ(s) for
all s∈2≤n, and properly extends, ψ≺φ,
if in fact
hgt(ψ)<hgt(φ) strictly.
Each system φ∈FSS(P) with hgt(φ)=0 consists
essentially of a single tree TΛφ∈P.
The next lemma provides systems of arbitrary height.
Lemma 3.2**.**
Assume that P∈PTF.
If n≥1 and ψ=⟨Ts⟩s∈2≤n∈FSS(P)
then there is a system
φ=⟨Ts⟩s∈2≤n+1∈FSS(P)
which properly extends ψ.
Proof**.**
If s∈2n and i=0,1 then let
Ts⌢i=Ts(→i).
∎
The next well-known lemma belongs to the type of
splitting/fusion lemmas widely used in connection
with the perfect set forcing and some similar forcings.
Lemma 3.3**.**
Let P∈PTF.
Then there is an ≺-increasing sequence
⟨φn⟩n<ω of systems in FSS(P).
And if ⟨φn⟩n<ω is such then:
(i)
the limit system
φ=⋃nφn=⟨Ts⟩s∈2<ω
satisfies (∗) ‣ 3.1 of Definition 3.1
on the whole domain of strings s∈2<ω;
2. (ii)
T=⋂n⋃s∈2nTs* is
a perfect tree in PT
and [T]=⋂n⋃s∈2n[Ts];*
3. (iii)
if u∈2<ω then
T(→u)=T∩Tu=⋂n≥lh(u)⋃s∈2n,u⊆sTs.
∎
4 Multiforcings and multitrees
We’ll systematically make use of finite support products
of perfect tree forcings in this paper.
The following definitions introduce suitable notation.
Call a multiforcing
any map π:∣π∣→PTF, where
∣π∣=domπ⊆ω1×ω.
Thus each set π(ξ,k),
⟨ξ,k⟩∈∣π∣,
is a perfect tree forcing notion.
Such a π is:
−
small, if both ∣π∣ and each
forcing π(ξ,k), ⟨ξ,k⟩∈∣π∣, are countable;
−
special,
if each π(ξ,k) is special in the sense of
Definition 2.4;
−
regular, if each π(ξ,k) is regular,
in the sense of Definition 2.4.
Let MF be the set of all multiforcings.
Let a multitree be any map
p:∣p∣→PT, such that ∣p∣=domp⊆ω1×ω
is finite and each value
Tξkp=p(ξ,k) is a tree in PT.
In this case we define a cofinite-dimensional
perfect cube in 2ω1×ω
[TABLE]
Let MT be the set of all multitrees.
We order MT componentwise: q⩽p
(q is stronger)
iff ∣p∣⊆∣q∣ and
Tξkq⊆Tξkp for all ⟨ξ,k⟩∈∣p∣;
this is equivalent to [q]⊆[p], so that stronger
multitrees correspond to smaller cubes.
The weakest multitree Λ∈MT is just the empty map;
∣Λ∣=∅ and [Λ]=2ω1×ω.
Multitrees p,q are somewhere almost disjoint,
or s. a. d.,
if, for at least one pair of indices
⟨ξ,k⟩∈∣p∣∩∣q∣,
the trees Tξkp, Tξkq are a. d.,
that is, [Tξkp]∩[Tξkq]=∅,
or equivalently, Tξkp∩Tξkq is
finite.
If π is a regular multiforcing and multitrees
p,q∈MT(π) are not s. a. d., then p,q
are compatible in MT(π), so that there is a
multitree r∈MT(π) with
r⩽p, r⩽q.∎
If π is a multiforcing then
a π-multitree is any multitree p with
∣p∣⊆∣π∣ and
Tξkp∈π(ξ,k) for all
⟨ξ,k⟩∈∣p∣.
Let MT(π)
be the set of all π-multitrees;
it is equal to the finite support product
∏⟨ξ,k⟩∈∣π∣π(ξ,k).
If a multiforcing π is regular, ξ⊆∣π∣
is finite, and U1,…,Uk are
finite collections of multitrees in MT(π)
with ∣p∣=ξ for all p∈⋃iUi,
then there is a finite set of multitrees
u1,…,un∈MT(π) such that
∣uj∣=ξ, ∀j,
[TABLE]
and for any Ui and uj, there is
p∈Ui such that [uj]⊆[p].
∎
We consider sets of the form MT(π) in the
role of product forcing notions.
A set D⊆MT(π) is:
−
open in MT(π), if for any p⩽q in MT(π),
q∈D⟹p∈D;
−
dense in MT(π), if for any p∈MT(π),
there is q∈D, q⩽p;
−
pre-dense in MT(π), if the set
D′={p∈MT(π):\linebreak[0]∃q∈D(p⩽q)}
is dense in MT(π).
Remark 4.3**.**
As a forcing notion, each
MT(π) adds an array
⟨xξk⟩⟨ξ,k⟩∈∣π∣ of reals,
where each real xξk∈2ω
is a π(ξ,k)-generic real.
Namely if a set G⊆MT(π) is generic over the ground
set universe V then each factor
[TABLE]
(where ⟨ξ,k⟩∈∣π∣)
is accordingly a set π(ξ,k)-generic over V, the real
xξk=xξk[G]=x[G(ξ,k)]∈2ω is the only
real satisfying xξk∈⋂T∈G(ξ,k)[T], and
xξk is π(ξ,k)-generic over V as in
Lemma 2.7.
∎
The reals of the form xξk[G] will be called
principal generic reals in V[G].
Definition 4.4**.**
A componentwise union of multiforcings
π,\leavevmode is a multiforcing π∪cw\leavevmode satisfying
∣(π∪cw\leavevmode)∣=∣π∣∪∣\leavevmode∣ and
[TABLE]
Similarly, if \vvπ=⟨πα⟩α<λ is a sequence
of multiforcings then
define a multiforcing π=⋃cw\vvπ=⋃α<λcwπα so that
∣π∣=⋃α<λ∣πα∣ and if
⟨ξ,k⟩∈∣π∣ then
π(ξ,k)=⋃α<λ,⟨ξ,k⟩∈∣πα∣πα(ξ,k).
∎
5 Multisystems
The next definition introduces
multisystems, a multi version of the
splitting/fusion technique of Section 3,
whose intention is to define suitable multiforcings,
as will be shown in Section 3 below.
Definition 5.1**.**
A multisystem
is any map φ:∣φ∣→FSS,
such that
∣φ∣⊆ω1×ω×ω is finite.
This amounts to
(1)
the map
hφ(ξ,k,m)=hgt(φ(ξ,k,m)):∣φ∣→ω,
and
2. (2)
the finite collection of trees
Tξk,mφ(s)=φ(ξ,k,m)(s),
where ⟨ξ,k,m⟩∈∣φ∣
and s∈2≤hφ(ξ,k,m), such that if
⟨ξ,k,m⟩∈∣φ∣ then
φ(ξ,k,m)=⟨Tξk,mφ(s)⟩s∈2≤hφ(ξ,k,m)
is a finite splitting system in FSS.
If π is a multiforcing, ∣φ∣⊆(∣π∣)×ω, and
φ(ξ,k,m)∈FSS(π(ξ,k)) for all
⟨ξ,k,m⟩∈∣φ∣
(or equivalently,
Tξk,mφ(s)∈π(ξ,k) whenever
\langle\xi,k,m\rangle\in$$\boldsymbol{\varphi} and s∈2≤hφ(ξ,k,m)),
then say that φ is a π-multisystem,
φ∈MS(π).
∎
Let φ,ψ be multisystems.
Say that
φextendsψ,
symbolically ψ≼φ,
if ∣ψ∣⊆∣φ∣, and,
for every ⟨ξ,k,m⟩∈∣ψ∣,
φ(ξ,k,m) extends ψ(ξ,k,m), that is,
hφ(ξ,k,m)≥hψ(ξ,k,m) and
Tξk,mφ(s)=Tξk,mψ(s) for all
s∈2≤hψ(ξ,k,m).
It will be demonstrated in Section 3 that a
suitably increasing infinite sequence
φ0≼φ1≼φ2≼… of multisystems in
some MS(π) leads to a “limit” multiforcing
with ∣\leavevmode∣=⋃n∣φn∣, such that each
factor \leavevmode(ξ,k), ⟨ξ,k⟩∈∣π∣, is filled
in by trees Qξk,m, m<ω, in such a way, that
the (ξ,k,m)-components of the systems φn
are responsible for the construction of the
tree Qξk,m.
The next lemma introduces different ways to extend
a given multisystem.
Say that a multisystem φ is 2wise disjoint if
[Tξk,mφ(s)]∩[Tηℓ,nφ(t)]=∅
for all triples ⟨ξ,k,m⟩=⟨η,ℓ,n⟩
in ∣φ∣
and all s∈2hφ(ξ,k,m) and
t∈2hφ(η,ℓ,n).
Lemma 5.2**.**
Let π be a multiforcing and φ∈MS(π).
(i)
If ⟨ξ,k,m⟩∈∣φ∣ and h=hφ(ξ,k,m) then
the extension ψ of φ by
hψ(ξ,k,m)=h+1 and
Tξk,mψ(s⌢i)=Tξk,mφ(s)(→i)
for all s∈2h and i=0,1,
belongs to
MS(π) and φ≼ψ.
2. (ii)
If ⟨ξ,k,m⟩∈/∣φ∣ then
the extension ψ of φ by
∣ψ∣=∣φ∣∪{⟨ξ,k,m⟩},
hψ(ξ,k,m)=0 and
Tξk,mψ(Λ)=T, where T∈π(ξ,k)
and Λ is the empty string,
belongs to MS(π) and φ≼ψ.
3. (iii)
If ⟨ξ,k,m⟩∈∣φ∣ and a set D⊆π(ξ,k)
is open dense in π(ξ,k) then there is a multisystem ψ∈MT(π) such that
∣ψ∣=∣φ∣, φ≼ψ, and
Tξk,mψ(s)∈D whenever s∈2hψ(ξ,k,m).
4. (iv)
*There is a 2wise disjoint
ψ∈MT(π) such that
∣ψ∣=∣φ∣ and φ≼ψ.*
Proof**.**
To prove (iii) first use (i) to get a multisystem ψ∈MS(π) with φ≼ψ and
hψ(ξ,k,m)=h+1, where h=hφ(ξ,k,m).
Then replace each tree Tξk,mψ(s)=ψ(ξ,k,m)(s),
s∈2h+1, with a suitable tree T′∈D,
T′⊆Tξk,mψ(s).
To prove (iv) first apply (i) to get a multisystem ψ∈MS(π) with φ≼ψ, ∣ψ∣=∣φ∣,
and hψ(ξ,k,m)=hφ(ξ,k,m)+1 for all
⟨ξ,k,m⟩∈∣φ∣.
Now if ⟨ξ,k,m⟩=⟨η,ℓ,n⟩ are triples
in ∣φ∣ and s∈2hφ(ξ,k,m)+1,
t∈2hφ(η,ℓ,n)+1, then, by Lemma 2.3(ii),
there are trees S∈π(ξ,k) and T∈π(η,ℓ)
satisfying [S]∩[T]=∅ and S⊆Tξk,mψ(s),
T⊆Tηℓ,nψ(t).
Replace the trees Tξk,mψ(s),
T⊆Tηℓ,nψ(t) with resp. S, T.
Iterate this shrinking construction for all triples
⟨ξ,k,m⟩=⟨η,ℓ,n⟩ and strings s,t as above.
∎
II Refinements
Here we consider refinements of perfect tree forcings
and multiforcings, the key technical tool of definition of various
forcing notions in this paper.
1 Refining perfect tree forcings
If T∈PT (a perfect tree) and D⊆PT then
X⊆fin⋃D will mean
that there is a finite set D′⊆D such that
T⊆⋃D′, or equivalently [T]⊆⋃S∈D′[S].
Definition 1.1**.**
Let P,Q∈PTF be perfect tree forcing
notions.
Say that Q is a refinement of P
(symbolically P⊏Q) if
(1)
the set
Q is dense in P∪Q:
if T∈P then ∃Q∈Q(Q⊆T);
2. (2)
if Q∈Q
then Q⊆fin⋃P;
3. (3)
if Q∈Q and T∈P then [Q]∩[T] is
clopen in [Q] and T⊆Q.∎
Lemma 1.2**.**
(i)
If P⊏Q and S∈P, T∈Q, then
[S]∩[T] is meager in [S],
therefore P∩Q=∅ and Q is
open dense in P∪Q;.
2. (ii)
if P⊏Q⊏R then P⊏R,
thus ⊏ is a strict partial order*;***
3. (iii)
if ⟨Pα⟩α<λ
is a ⊏-increasing sequence in PTF and
0<μ<λ then
P=⋃α<μPα⊏Q=⋃μ≤α<λPα;
4. (iv)
if ⟨Pα⟩α<λ
is a ⊏-increasing sequence in PTF and each
Pα is special then P=⋃α<λPα
is a regular forcing in PTF;
5. (v)
in (iv), each Pγ is pre-dense in
P=⋃α<λPα.
Proof**.**
(i)
Otherwise there is a string u∈S such that
S↾u⊆[T]∩[S].
But S↾u∈P, which contradicts to
1.1(3).
(iv)
To check the regularity let
S∈Pα, T∈Pβ, α≤β.
If α=β then, as Pα is special, the trees
S,T are either a. d. or ⊆-comparable by
Lemma 2.5.
If α<β then [S]∩[T] is clopen in [T]
by 1.1(3).
(v)
Let S∈Pα, α=γ.
If α<γ then by 1.1(1) there is a tree
T∈Pγ, T⊆S.
Now let γ<α.
Then S⊆fin⋃Pγ by 1.1(2), in particular,
there is a tree T∈Pγ such that [S]∩[T]=∅.
However [S]∩[T] is clopen in [S] by 1.1(3).
Therefore S↾u⊆T for a string u∈S.
Finally S↾u∈Pα since Pα∈PTF.
∎
Note that if P,Q∈PTF and P⊏Q then a
dense set D⊆P is not necessarily dense or even
pre-dense in P∪Q.
Yet there is a special type of refinement which preserves
at least pre-density.
We modify the relation ⊏ as follows.
Definition 1.3**.**
Let P,Q∈PTF and
D⊆P.
Say that Qlocks D over P,
symbolically P⊏DQ, if P⊏Q holds and
every tree S∈Q satisfies S⊆fin⋃D.
Then simply P⊏Q is equivalent to P⊏PQ.
∎
As we’ll see now, a locked set has to be pre-dense both before
and after the refinement.
The additional importance of locking refinements lies in fact that,
once established, it preserves under further simple
refinements, that is, ⊏D is transitive in
a combination with ⊏ in the sense of (ii)
of the following lemma:
Lemma 1.4**.**
(i)
If P⊏DQ then D is pre-dense in P∪Q,
and if in addition P is regular then
D is pre-dense in P as well*;***
2. (ii)
if P⊏DQ⊏R(note: the second ⊏ is not ⊏D!)
then P⊏DR;
3. (iii)
if ⟨Pα⟩α<λ
is a ⊏-increasing sequence in PTF,
0<μ<λ, and
P=⋃α<μPα⊏DPμ, then
P⊏DQ=⋃μ≤α<λPα.
Proof**.**
(i)
To see that D is pre-dense in P∪Q,
let T0∈P∪Q.
By 1.1(1), there is a tree T∈Q, T⊆T0.
Then T⊆fin⋃D, in particular, there is a tree
S∈D with X=[S]∩[T]=∅.
However X is clopen in [T] by 1.1(3).
Therefore, by Lemma 2.2,
there is a tree T′∈Q
with [T′]⊆X, thus T′⊆S∈D and T′⊆T⊆T0.
We conclude that T0 is compatible with S∈D in P∪Q.
To see that D is pre-dense in P (assuming P is regular),
let S0∈P.
It follows from the above that S0 is compatible with some
S∈D, hence, S and S0 are not absolutely incompatible.
It remains to use Lemma 2.5(i).
To prove (ii) on the top of Lemma 1.2(ii),
let R∈R.
Then R⊆fin⋃Q, but each T∈Q satisfies
T⊆fin⋃D.
The same for (iii).
∎
The existence of ⊏D-refinements will be established below.
2 Refining multiforcings
Let π,\leavevmode be multiforcings.
Say that is an refinement of π,
symbolically π⊏\leavevmode, if ∣π∣⊆∣\leavevmode∣
and
π(ξ,k)⊏\leavevmode(ξ,k) whenever ⟨ξ,k⟩∈∣π∣.
If π⊏\leavevmode then the multiforcing MT(\leavevmode)
is open dense in MT(π∪cw\leavevmode).
∎
Our next goal is to introduce a version of
Definition 1.3 suitable for multiforcings;
we expect an appropriate version of
Lemma 1.4 to hold.
First of all, we accomodate the definition of the
relation ⊆fin in Section 1 for multitrees.
Namely if u is a multitree and D a collection of multitrees,
then u⊆fin⋁D
will mean that there is a finite
set D′⊆D satisfying
∣v∣=∣u∣ for all v∈D′, and
[u]⊆⋃v∈D′[v].
Definition 2.2**.**
Let π,\leavevmode be multiforcings, and π⊏\leavevmode.
Say that
locks a set D⊆MT(π) over π*,
symbolically π⊏D\leavevmode
if the following condition holds:
(∗)
if
p∈MT(π), u∈MT(\leavevmode), ∣u∣⊆∣π∣,
∣u∣∩∣p∣=∅,
then there is q∈MT(π)
such that q⩽p, still ∣q∣∩∣u∣=∅,
and u⊆fin⋁Dq∣u∣, where
[TABLE]
Note that if p,u,D,q are as indicated then still
u∪q⊆fin⋁D holds via the finite set
D′={u′∪q:\linebreak[0]u′∈Dq∣u∣}⊆D.
Anyway the definition of ⊏D in 2.2
looks somewhat different and more complex
then the definition of ⊏D in 1.3,
which reflects the fact
that finite-support products of
forcing notions in PTF behave
differently (and in more complex way)
than single perfect-tree forcings.
Accordingly, the next lemma, similar to Lemma 1.4, is
way harder to prove.
Lemma 2.3**.**
Let π,\leavevmode,σ be multiforcings and
D⊆MT(π).
Then:
(i)
if π⊏D\leavevmode then D is
dense in MT(π) and
pre-dense in MT(π∪cw\leavevmode);
2. (ii)
if π⊏D\leavevmode and D⊆D′⊆MT(π)
then π⊏D′\leavevmode;
3. (iii)
if π is regular,
π⊏Di\leavevmode for i=1,…,n, all sets
Di⊆MT(π)
are open dense in MT(π), and D=⋂iDi,
then π⊏D\leavevmode;
4. (iv)
if D is open dense in MT(π)
and π⊏D\leavevmode⊏σ then π⊏Dσ;
5. (v)
if ⟨πα⟩α<λ
is a ⊏-increasing sequence in MF,
0<μ<λ, π=⋃α<μcwπα,
D is open dense in MT(π),
and π⊏Dπμ, then
π⊏D\leavevmode=⋃μ≤α<λcwπα.
Proof**.**
(i)
To check that D is pre-dense in MT(π∪cw\leavevmode),
let r∈MT(π∪cw\leavevmode).
Due to the product character of MT(π∪cw\leavevmode), we can assume
that ∣r∣⊆∣π∣.
Let
[TABLE]
Then r=u∪p, where
u=r↾X∈MT(\leavevmode), p=r↾Y∈MT(π).
As locks D, there is a multitree q∈MT(π)
such that q⩽p, ∣q∣∩∣u∣=∅,
and u⊆fin⋃Dq∣u∣.
By an easy argument,
there is a multitree u′∈Dq∣u∣ compatible
with u in MT(\leavevmode); let w∈MT(\leavevmode), w⩽u,
w⩽u′, ∣w∣=∣u′∣=∣u∣.
Then the multitree r′=w∪q∈MT(π∨\leavevmode)
satisfies r′⩽r and r′⩽u′∪q∈D.
To check that D is dense in MT(π),
suppose that p∈MT(π).
Let u=Λ (the empty multitree)
in (∗) ‣ 2.2 of Definition 2.2,
so that ∣u∣=∅ and Dq∣u∣=D.
(ii) is obvious.
To prove (iii), let p∈MT(π),
u∈MT(\leavevmode), ∣u∣⊆∣π∣,
∣u∣∩∣p∣=∅.
Iterating (∗) ‣ 2.2 for Di, i=1,…,n, we find
a multitree q∈MT(π)
such that q⩽p, ∣q∣∩∣u∣=∅,
and u⊆fin⋁(Di)q∣u∣ for all i, where
[TABLE]
Thus there are finite sets Ui⊆(Di)q∣u∣
such that [u]⊆⋃v∈Ui[v] for all i.
Using the regularity assumption and Lemma 4.2,
we refine multitrees in ⋃iUi,
getting a finite set W⊆MT(π)
such that still ∣w∣=∣u∣ for all w∈W,
⋂i⋃v∈Ui[v]=⋃w∈W[w],
and if i=1,…,n and w∈W then
[w]⊆[v] for some v∈Ui — therefore
w∪q∈Di.
We conclude that if w∈W then w∪q∈D,
hence w∈Dq∣u∣.
Thus W⊆Dq∣u∣.
However [u]⊆⋃w∈W[w] by the choice of W.
We conclude that u⊆fin⋁Dq∣u∣, as required.
(iv)
It follows from Corollary 2.1 that π⊏σ,
hence it remains to check that σ locks D over π.
Assume that u∈MT(σ),
∣u∣⊆∣π∣,
p∈MT(π), ∣u∣∩∣p∣=∅.
As \leavevmode⊏σ, there is a finite set U⊆MT(\leavevmode) such that
∣v∣=∣u∣ for all v∈U, and
[u]⊆⋃v∈U[v].
As π⊏D\leavevmode,
by iterated application of (∗) ‣ 2.2 of Definition 2.2,
we get a multitree q∈MT(π)
such that q⩽p, still ∣q∣∩∣u∣=∅,
and if v∈U then v⊆fin⋁Dq∣u∣, where
[TABLE]
Note finally that u⊆fin⋁U by construction, hence
u⊆fin⋁Dq∣u∣ as well.
(v)
We have to check that locks D over π.
Let u∈MT(\leavevmode),
∣u∣⊆∣π∣,
p∈MT(π), ∣u∣∩∣p∣=∅.
As above, there is a finite set U⊆MT(πμ) such that
∣v∣=∣u∣ for all v∈U and
[u]⊆⋃v∈U[v].
And so on as in the proof of (iv).
∎
3 Generic refinement of a multiforcing
Here we introduce a construction,
due to Jensen in its original form, which implies
the existence of refinements
of forcings and multiforcings, of types ⊏D and ⊏D.
Definition 3.1**.**
Suppose that π is a small multiforcing, and M∈HC is
any set.
(Recall that HC = all hereditarily countable sets.)
This is the input.
The set M+ of all sets X∈HC, ∈-definable
in HC by formulas with sets in M as parameters, is
still countable.
Therefore there exists a ≼-increasing sequence
⟨φ(j)⟩j<ω of multisystems φ(j)∈MS(π),
M+-generic in the sense that it intersects
any set Δ⊆MS(π), Δ∈M+,
dense in MS(π).
(The density means that for any ψ∈MS(π) there is
a multisystem φ∈Δ with ψ≼φ.)
Let us fix any such a M+-generic sequence
Φ=⟨φ(j)⟩j<ω.
Suppose that ⟨ξ,k⟩∈∣π∣ and m<ω.
In particular, the sequence Φ intersects
every (dense by Lemma 5.2(i),(ii)) set
of the form
[TABLE]
Hence a tree Tξk,mΦ(s)∈π(ξ,k)
can be associated to any
s∈2<ω, such that, for all j, if
⟨ξ,k,m⟩∈∣φ(j)∣ and lh(s)≤hφ(j)(ξ,k,m)
then Tξk,mφ(j)(s)=Tξk,mΦ(s).
Then it follows from Lemma 3.3 that each set
Qξk,mΦ=⋂h⋃s∈2hTξk,mΦ(s)
is a tree in PT (not necessarily in π(ξ,k)),
as well as the trees
[TABLE]
and obviously Qξk,mΦ=Qξk,mΦ(Λ).
Let QξkΦ={Qξk,mΦ(s):\linebreak[0]m<ω∧s∈2<ω}.
If ⟨ξ,k⟩∈∣π∣ then let
\leavevmode(ξ,k)=QξkΦ={Qξk,mΦ(s):\linebreak[0]m<ω∧s∈2<ω}.
Finally if \leavevmode=\leavevmode[Φ] is obtained this way from an
M+-generic sequence Φ of multisystems in MS(π),
then is called
an M-generic refinement of π.
∎
Proposition 3.2** (by the countability of M+).**
If
π is a small multiforcing and M∈HC
then there is an
M-generic refinement of π.
∎
Theorem 3.3**.**
If π is a small multiforcing,
a set M∈HC contains π, ∣π∣⊆M,
and is an M-generic refinement of π,
then:
(i)
is a small special multiforcing, ∣\leavevmode∣=∣π∣,
and *π⊏\leavevmode;
(ii)
if ⟨ξ,k⟩∈∣π∣ and a set D∈M,
D⊆π(ξ,k) is pre-dense in π(ξ,k) then
π(ξ,k)⊏D\leavevmode(ξ,k);
3. (a)
if ⟨ξ,k⟩∈∣π∣, m<ω, and
s∈2<ω then Qξk,mΦ(s)=Qξk,mΦ(→s);
4. (b)
if ⟨ξ,k⟩∈∣π∣, m<ω, and
s∈2<ω then Qξk,mΦ(s)⊆Tξk,mΦ(s);
5. (c)
if ⟨ξ,k⟩∈∣π∣, m<ω,
and strings t′=t in 2<ω
are ⊆-incomparable then
[Qξk,mΦ(t′)]∩[Qξk,mΦ(t)]=[Tξk,mΦ(t′)]∩[Tξk,mΦ(t)]=∅;
6. (d)
if ⟨ξ,k,m⟩=⟨η,ℓ,n⟩ then
[Qξk,mΦ]∩[Qηℓ,nΦ]=∅;
7. (e)
if ⟨ξ,k⟩∈∣π∣, S∈\leavevmode(ξ,k) and T∈π(ξ,k)
then [S]∩[T] is clopen in [S]
and T⊆S,
in particular, π(ξ,k)∩\leavevmode(ξ,k)=∅;
8. (f)
if ⟨ξ,k⟩∈∣π∣ then
the set \leavevmode(ξ,k) is open dense in \leavevmode(ξ,k)∪π(ξ,k).
If in addition π=⋃α<λcwπα, where
λ<ω1, ⟨πα⟩α<λ
is a ⊏-increasing sequence of small special multiforcings,
and M contains ⟨πα⟩α<λ
and all α<λ, then
(iii)
*if α<λ then πα⊏\leavevmode.
*
Proof**.**
Let \leavevmode=\leavevmode[Φ] be obtained from an
M+-generic sequence Φ of multisystems in MS(π),
as above.
We argue in the notation of Definition 3.1.
If ⟨ξ,k⟩∈∣π∣ and m<ω then by construction
the system of trees
Tξk,mΦ(s)∈π(ξ,k), s∈2<ω,
satisfies 3.1(∗) ‣ 3.1 on the whole domain s∈2<ω.
This leads to (a), (b)
(essentially corollaries of Lemma 3.3)
and (c).
To prove (d) note that the set Δ
of all 2wise disjoint multisystems φ such that
∣φ∣ contains both ⟨ξ,k,m⟩ and ⟨η,ℓ,n⟩,
is dense in MS(π) by Lemma 5.2, and obviously
Δ∈M+.
Therefore there is j<ω such that φ(j)∈Δ.
Let h=hφ(j)(ξ,k,m) and h′=hφ(j)(η,ℓ,n).
Then the sets
[TABLE]
are disjoint as φ(j)∈Δ.
However [Qξk,mΦ]⊆A and [Qηℓ,nΦ]⊆B.
(i)
It follows that the sets \leavevmode(ξ,k)=QξkΦ are
special PTFs (Definition 2.4), and hence
is a small special multiforcing, as in (i), and
∣\leavevmode∣=∣π∣.
(e)
To prove the clopenness claim, note that
the set Δ of all multisystems φ∈MS(π) such that
⟨ξ,k,m⟩∈∣φ∣ and if s∈2h, where
h=hφ(ξ,k,m), then either
Tξk,mφ(s)⊆T or [Tξk,mφ(s)]∩[T]=∅,
is dense.
To prove T⊆S,
the set Δ′ of all multisystems φ∈MS(π) such that
⟨ξ,k,m⟩∈∣φ∣ and
T⊆⋃s∈2hTξk,mφ(s),
where h=hφ(ξ,k,m), is dense.
Note that Δ,Δ′∈M+ and argue as above.
(f)Density.
If T∈π(ξ,k) then
the set Δ(T) of all multisystems
φ∈MS(π),
such that Tξk,mφ(Λ)=T for some m,
is dense in MS(π) by Lemma 5.2(ii),
therefore φ(j)∈Δ(T) for some j.
Then Tξk,mΦ(Λ)=T for some m<ω.
However Qξm,kΦ(Λ)⊆Tξk,mΦ(Λ).
Openness.
Suppose that S∈\leavevmode(ξ,k), T∈\leavevmode(ξ,k)∪π(ξ,k),
T⊆S.
Then T∈/π(ξ,k) by (e).
Therefore T∈\leavevmode(ξ,k).
(i), continuation.
To establish π⊏\leavevmode,
let ⟨ξ,k⟩∈∣π∣.
We have to prove that π(ξ,k)⊏\leavevmode(ξ,k).
This comes down to conditions (1), (2), (3)
of Definition 1.1, of which (1) follows from
(f) and (3) from (e), and (2)
is obvious since
Qξk,mΦ(s)⊆Tξk,mΦ(s)∈π(ξ,k)
for all m.
(ii)
As π⊏\leavevmode has been checked, it remains to prove
Qξk,mΦ⊆fin⋃D for all m.
It follows from the pre-density of D that the set
D′={T∈π(ξ,k):\linebreak[0]∃S∈D(T⊆S)}
is open dense in π(ξ,k), and still D′∈M+.
Then the set Δ∈M+ of all multisystems
φ∈MS(π) such that ⟨ξ,k,m⟩∈∣φ∣ and
Tξk,mφ(s)∈D for all s∈hφ(ξ,k,m),
is dense in MS(π) by Lemma 5.2(iii).
Thus φ(j)∈Δ for some j, which witnesses
Qξk,mΦ⊆fin⋃D.
(iii)
We have to prove that πα(ξ,k)⊏\leavevmode(ξ,k)
whenever ⟨ξ,k⟩∈∣πα∣.
And as π(ξ,k)⊏\leavevmode(ξ,k) has been checked,
it suffices to prove that
Qξk,mΦ⊆fin⋃πα(ξ,k) for all m.
However D=πα(ξ,k) is pre-dense in
π(ξ,k) by Lemma 1.2(v), and still
D∈M+, hence we can refer to
(ii).
∎
Corollary 3.4**.**
In the assumptions of Proposition 3.2, if
∣π∣⊆Z⊆ω1×ω and Z is at most countable
then there is a small special multiforcing
such that ∣\leavevmode∣=Z
and π⊏\leavevmode.
Proof**.**
If ∣π∣=Z then let M be any countable set containing
π, pick by Proposition 3.2,
and apply Theorem 3.3.
If ∣π∣⫋Z then we trivially extend the
construction by \leavevmode(ξ,k)=Pcoh (see Example 2.1)
for all ⟨ξ,k⟩∈Z∖∣π∣.
∎
Corollary 3.5**.**
Suppose that λ<ω1, and
⟨Pα⟩α<λ is an
⊏-increasing sequence of countable special forcings
in PTF.
Then there is a countable special forcing Q∈PTF
such that Pα⊏Q for each α<λ.
Proof**.**
If α<λ then let a multiforcing πα be defined
by ∣πα∣={⟨0,0⟩} and
by πα(0,0)=Pα.
By Proposition 3.2
and Theorem 3.3 there is a multiforcing satisfying
∣\leavevmode∣={⟨0,0⟩} and
πα⊏\leavevmode, ∀α.
Let Q=\leavevmode(0,0).
∎
4 Preservation of density
This Section proves a special consequence of
M+-genericity of multiforcing refinements,
the relation ⊏ of Definition 2.2 between
a multiforcing and its refinement.
Theorem 4.1**.**
In the assumptions of Theorem 3.3, if
D∈M+, D⊆MT(π), and
D is open dense in MT(π),
then π⊏D\leavevmode.
Proof**.**
We suppose that \leavevmode=\leavevmode[Φ] is obtained from an
increasing
M+-generic sequence Φ of multisystems in MS(π),
as in Definition 3.1, and argue in the notation of
3.1.
Suppose that p∈MT(π), u∈MT(\leavevmode),
∣u∣∩∣p∣=∅, as in (∗) ‣ 2.2 of
Definition 2.2; the extra condition
∣u∣⊆∣π∣ holds automatically as we still have
∣\leavevmode∣=∣π∣.
Let X=∣u∣, Y=∣π∣∖X.
If ⟨ξ,k⟩∈X then
Tξku=Qξk,mξkΦ(sξk),
where mξk<ω and sξk∈2<ω.
By obvious reasons we can assume that sξk=Λ,
hence Tξku=Qξk,mξkΦ,
for all ⟨ξ,k⟩∈X.
Consider the set Δ of all multisystems
φ∈MS(π) such that there is a number H>0
and a multitree q∈MS(π)
satisfying (1), (2), (3), (4) below.
(1)
∣q∣∩X=∅ and q⩽p;
2. (2)
if ⟨ξ,k⟩∈X then
⟨ξ,k,mξk⟩∈∣φ∣;
3. (3)
if ⟨ξ,k,m⟩∈∣φ∣ then
hφ(ξ,k,m)=H.
To formulate the last requirement, we need one more definition.
Suppose that τ=⟨tξk⟩⟨ξ,k⟩∈X is a
system of strings τ(ξ,k)=tξk∈2H, symbolically
τ∈(2H)X.
Define a multitree s(φ,τ)∈MT(π) so that
∣s(φ,τ)∣=X and
Tξks(φ,τ)=Tξk,mξkφ(tξk)
for all ⟨ξ,k⟩∈X.
Note that ∣s(φ,τ)∣=∣u∣,
and hence the multitree s(φ,τ)∪q belongs to MT(π) as well. 333 Here, if p,q are multitrees satisfying
∣p∣∩∣q∣=∅ (disjoint domains),
then p∪q, a disjoint union, is a multitree such that
∣p∪q∣=∣p∣∪∣q∣ and
Tξkp∪q=Tξkp whenever ⟨ξ,k⟩∈∣p∣
but
Tξkp∪q=Tξkq whenever ⟨ξ,k⟩∈∣q∣.
Now goes the last condition.
(4)
If τ∈(2H)X
then s(φ,τ)∪q∈D.
Lemma 4.2**.**
The set Δ is dense in MS(π).
Proof** (Lemma).**
Suppose that ψ∈MS(π); we have to find
a multisystem φ∈MS(π) with ψ≼φ.
First of all, by Lemma 5.2(i)(ii)
we can assume that
(a)
if ⟨ξ,k⟩∈X then
⟨ξ,k,mξk⟩∈∣ψ∣;
2. (b)
there is a number g>0
such that hψ(ξ,k,m)=g for all ⟨ξ,k,m⟩∈∣ψ∣.
Let H=g+1.
Define
χ∈MS(π) so that
∣χ∣=∣ψ∣, and
hχ(ξ,k,m)=H,
Tξk,mχ(s⌢i)=Tξk,mψ(s)(→i)
for all ⟨ξ,k,m⟩∈∣ψ∣ and s⌢i∈2H;
then ψ≼χ.
It follows from the open density of D that there is a multitree q∈MT(π) satisfying (1), and a multisystem φ∈MS(π) satisfying (4)
and such that still ∣φ∣=∣ψ∣
and hφ(ξ,k,m)=H for all ⟨ξ,k,m⟩∈∣ψ∣,
and in addition
(c)
if ⟨ξ,k⟩∈X and s∈2H then
Tξk,mξkφ(s)⊆Tξk,mξkχ(s);
2. (d)
Tξk,mφ(s)=Tξk,mχ(s) for all
applicable ξ,k,m,s not covered by (c).
Namely to achieve (4) for one particular
τ∈(2H)X,
consider the multitree r=s(χ,τ)∪p.
There is a multitree r′∈D, r′⩽r.
Let a new multisystem χ′ be obtained from χ by the reassignment
Tξk,mξkχ′(τ(ξ,k))=Tξkr′ for
all ⟨ξ,k⟩∈X.
To get the input for the next step,
let p′=r′↾Y, 444 Here r′↾Y is the plain restriction of the function
r′:∣r′∣→PT to the set ∣r′∣∩Y.
so that
r′=s(χ′,τ)∪p′∈D.
Now consider another τ′∈(2H)X and the multitree r′=s(χ′,τ′)∪p′.
There is r′′∈D, r′′⩽r′.
Define χ′′ from χ′ by the reassignment
Tξk,mξkχ′′(τ′(ξ,k))=Tξkr′′ for
all ⟨ξ,k⟩∈X.
Let p′′=r′′↾Y, so that
r′′=s(χ′′,τ′)∪p′′∈D.
And so on.
The final multisystem and multitree of this construction will be φ
and q satisfying (1), (2), (3),
(4).
Note that ψ≼φ,
as we only amend
the H-th level of χ absent in ψ.
□ (Lemma)
Note that Δ is defined in HC using sets
D, π, p, X, and the map
⟨ξ,k⟩→mξk:X→ω as parameters.
Now, D, π belong to M+ straightforwardly,
X belongs to M+ since it is a finite subset of a
set ∣π∣⊆M, and p belongs to M+ by
similar reasons.
It follows that Δ belongs to M+ as well.
Therefore, by the lemma and the choice of Φ,
there is an index j
such that the multisystem φ(j) belongs
to Δ, which is witnessed by a number H>0 and a multitree q∈MT(π)
satisfying (1), (2), (3), (4)
for φ(j) instead of φ.
To prove that
u⊆fin⋁Dq∣u∣,
note that
the multitrees s(φ(j),τ)∪q, τ∈(2H)X,
belong to D by (4), and easily
[u]⊆⋃τ∈(2H)X[s(φ(j),τ)].
∎
III Structure of real names
Here we turn to some details of the structure of reals in
models of MT(π)-generic type, π being a multiforcing.
We are going focus on non-principal reals, i. e.,
those different from the principal generic reals
xξk[G] (Remark 4.3).
We’ll work towards the goal of making every non-principal
real to be non-generic with respect to each of
the factor forcing notions π(ξ,k).
1 Real names
Our next goal is to
introduce a suitable notation related to names of reals
in the context of forcing notions of the form
MT(π).
Definition 1.1**.**
A real name
is any set c⊆MT×(ω×ω) such that the
sets Knic={p∈MT:\linebreak[0]⟨p,n,i⟩∈c}
satisfy the following:
(∗)
if n,k,ℓ<ω, k=ℓ, and p∈Knkc,
q∈Knℓc, then
p,q are a. d..
A real name c
is small if each set Knic is at most countable —
then the sets
domc=⋃n,iKnic⊆MT and
∣c∣=⋃n,i⋃p∈Knic∣p∣⊆ω1×ω,
and c itself, are countable, too.
∎
Definition 1.2**.**
Let c be a real name and
G⊆MT a pairwise compatible set.
Define the
evaluationc[G]∈ωω so that
c[G](n)=i iff:
−
either ∃p∈G∃q∈Knic(p⩽q)
(recall that p⩽q means p is stronger),
−
or just i=0 and
¬∃p∈G∃q∈⋃iKnic(p⩽q)
(default case).
∎
Definition 1.3**.**
Let π be a multiforcing.
A real name c is said to be a
π-real name
if, in addition to (∗) ‣ 1.1 above, the following
condition holds:
(†)
each set Knc=⋃iKnic is
pre-dense for MT(π), in the sense that
the set
Knc↑π={p∈MT(π):\linebreak[0]∃q∈Knc(p⩽q)}
is dense (then obviously open dense) in MT(π).∎
Generally speaking, we do not assume that
Knc⊆MT(π).
However if, in addition to (∗) ‣ 1.1, (†) ‣ 1.3
above, Knc⊆MT(π) holds for all n,
then say
that c is a true π-real name.
Then each set Knc=⋃iKnic
is a pre-dense subset of MT(π).
Remark 1.4**.**
Let π be a multiforcing, c be a π-real name, and
a set G⊆MT(π) be MT(π)-generic over
the collection of all sets Knc↑π as in
(†) ‣ 1.3
(All of Knc↑π are dense by the choice of c.)
Then the “or” case in Definition 1.2
never happens as we have G∩(Knc↑π)=∅
by the choice of G.
∎
Remark 1.5**.**
If π is a regular multiforcing then the notions of being a. d. and being incompatible in MT(π) are equivalent by
Lemma 2.5(i), so that
a true π-real name is the same as a MT(π)-name
for an element of
ωω in the general theory of (unramified) forcing.
∎
Example 1.6**.**
If ξ<ω1, k<ω, then {\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi k}
is a real name such that if i=0,1 then
the set C_{ni}^{\xi k}=K^{{\overset{\text{\hskip 1.50694pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi k}}_{ni}
consists of a lone multitree r=rniξk with
∣r∣={⟨ξ,k⟩} and
Tξkr={t∈2<ω:\linebreak[0]lh(t)≤n∨t(n)=i},
and if i≥2 then Cniξk=∅.
∎
Remark 1.7**.**
If π∈MT and ⟨ξ,k⟩∈∣π∣
then {\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi k} is a π-real name of the real
xξk=xξk[G]∈2ω,
the (ξ,k)th term of a MT(π)-generic sequence
⟨xξk[G]⟩⟨ξ,k⟩∈∣π∣.
That is, if G⊆MT(π) is generic then
the real xξk[G] defined by 4.3
coincides with the real {\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi k}[G]
defined by 1.2.
∎
2 Direct forcing
The following definition of the direct forcing
relation is not
explicitly associated with
any concrete forcing notion, but in fact the direct forcing
relation (in all three instances) is compatible with any
forcing notion of the form MT(π).
Let c be a real name.
Let us say that a multitree p:
•
directly forces c(n)=i,
where n,i<ω, iff there is a
multitree q∈Knic
such that p⩽q (meaning: p is stronger);
•
directly forces s⊂c,
where s∈ω<ω, iff for all n<lh(s), p
directly forces c(n)=i, where i=s(n);
•
directly forces c∈/[T],
where T∈PT, iff there is a string s∈ω<ω∖T
such that p directly forces s⊂c.
Lemma 2.1**.**
If π is a multiforcing and c
is a π-real name, p∈MT(π),
⟨ξ,k⟩∈∣π∣, T∈PT, n<ω,
then
(i)
there is a number i<ω and
a multitree q∈MT(π),\linebreak[0]q⩽p,
which directly forces c(n)=i;
2. (ii)
there is
a multitree q∈MT(π),\linebreak[0]q⩽p,
which directly forces c∈/[T(→0)]
or directly forces c∈/[T(→1)].
Note that if T∈π(ξ,k)
then the trees T(→i), i=0,1 belong to
π(ξ,k).
(ii)
Let r=stem(T), n=lh(r).
By (i), there is a multitree q∈MT(π),\linebreak[0]p′⩽p,
and, for any m≤n, — a number im=0,1, such that q
directly forces c(m)=im, ∀m<n.
Let s∈2n+1 be defined by s(m)=im for every m≤n.
Then q directly forces s⊂c.
On the other hand, s cannot belong to both T(→0) and
T(→1).
∎
3 Locking real names
The next definition extends Definition 2.2
to real names.
Definition 3.1**.**
Assume that π,\leavevmode are multiforcings,
c is a real name, and π⊏\leavevmode.
Say that
locks c over π*,
symbolically π⊏c\leavevmode,
if locks, over π, each set Knc↑π defined in
1.3(†) ‣ 1.3, in the sense of Definition 2.2.
∎
In the assumptions of Theorem 3.3, if
c∈M+ and c is a π-real name then π⊏c\leavevmode.
Proof**.**
Note that each set Knc↑π belongs to M+
(as so do c and π) and is dense in MT(π),
so it remains to apply
Theorem 4.1.
∎
Lemma 3.3**.**
Let π,\leavevmode,σ be multiforcings and c be a real name.
Then
(i)
if π⊏c\leavevmode then c is a
π-real name and a
(π∪cw\leavevmode)-real name*;***
2. (ii)
if π⊏c\leavevmode⊏σ then
π⊏cσ;
3. (iii)
if ⟨πα⟩α<λ
is a ⊏-increasing sequence in MF,
0<μ<λ, π=⋃α<μcwπα,
and π⊏cπμ, then
π⊏c\leavevmode=⋃μ≤α<λcwπα.
Proof**.**
(i)
By definition, we have π⊏Knc↑π\leavevmode
for each n,
therefore Knc↑π is dense in MT(π)
(then obviously open dense)
and pre-dense in MT(π∪cw\leavevmode) by Lemma 2.3(i).
It follows that Knc↑(π∪cw\leavevmode) is dense in MT(π∪cw\leavevmode).
Let π be a multiforcing.
Then MT(π) adds a collection of reals xξk,
⟨ξ,k⟩∈∣π∣,
where each principal realxξk=xξk[G] is π(ξ,k)-generic
over the ground set universe.
Obviously many more reals are added, and given a
π-real name c, one can elaborate different requirements
for a condition p∈MT(π) to force that c is a name
of a real of the form xξk or to force the opposite.
But we are mostly interested in simple conditions
related to the “opposite” part.
The next definition provides such a condition.
Definition 4.1**.**
Let π be a multiforcing, ⟨ξ,k⟩∈∣π∣.
A real name c is
non-principal over π at ξ,k
if the following set
is open dense in MT(π):
[TABLE]
We’ll show below (Theorem 6.2(i)) that the
non-principality implies c being not a name
of the real xξk[G].
And further, the avoidance condition in the next definition
will be shown to imply c being a name
of a non-generic real.
Definition 4.2**.**
Let π,\leavevmode be multiforcings, π⊏\leavevmode,
⟨ξ,k⟩∈∣π∣.
Say that
avoids a real name c over π
at ξ,k*,
in symbol π⊏ξkc\leavevmode,
if for each
Q∈\leavevmode(ξ,k), locks, over π, the set
[TABLE]
in the sense of Definition 2.2 —
formally π⊏D(c,Q,π)\leavevmode.
∎
Lemma 4.3**.**
Assume that π,\leavevmode,σ are multiforcings,
⟨ξ,k⟩∈∣π∣, and
c is a π-real name.
Then:
(i)
if π⊏ξkc\leavevmode and Q∈\leavevmode(ξ,k) then
the set D(c,Q,π) is open dense in MT(π)
and pre-dense in MT(π∪cw\leavevmode);
2. (ii)
if π⊏ξkc\leavevmode⊏σ then
π⊏ξkcσ;
3. (iii)
if ⟨πα⟩α<λ
is a ⊏-increasing sequence in MF,
0<μ<λ, π=⋃α<μcwπα,
and π⊏ξkcπμ, then
π⊏ξkc\leavevmode=⋃μ≤α<λcwπα.
(ii)
Let ⟨ξ,k⟩∈∣π∣ and S∈σ(ξ,k).
Then, as \leavevmode⊏σ, there is a finite set
{Q1,…,Qm}⊆\leavevmode(ξ,k) such that
S⊆Q1∪⋯∪Qm.
We have
π⊏D(c,Qi,π)\leavevmode for all i
since π⊏ξkc\leavevmode, therefore
π⊏D(c,Qi,π)σ, ∀i,
by Lemma 2.3(iv).
Note that ⋂iD(c,Qi,π)⊆D(c,S,π)
since S⊆⋃iQi.
We conclude that π⊏D(c,S,π)σ
by Lemma 2.3(ii),(iii).
Therefore π⊏ξkcσ.
∎
5 Generic refinements avoid non-principal names
The following theorem says that generic refinements as
in Section 3 avoid nonprincipal names.
It resembles Theorem 4.1 to some extent, yet the
latter is not directly applicable here as both
the multitree Q and
the set D(c,Q,π) depend on , and hence the
sets D(c,Q,π) do not necessarily belong to M+.
However the proof will be based on rather similar
arguments.
Theorem 5.1**.**
In the assumptions of Theorem 3.3, if
⟨η,K⟩∈∣π∣⊆M and
c∈M is a π-real name non-principal
over π at η,K then π⊏ηKc\leavevmode.
Proof**.**
Assume that \leavevmode=\leavevmode[Φ] is obtained from an
M+-generic sequence Φ of multisystems in MS(π),
as in Definition 3.1.
We stick to the notation of 3.1.
Let
Q∈\leavevmode(η,K);
we have to prove that locks the set
D(c,Q,π) over π.
By construction Q=QηK,mΦ(s0)⊆QηK,mΦ
for some m<ω;
it can be assumed that Q=QηK,mΦ.
Following the proof of Theorem 4.1,
we suppose that p∈MT(π), u∈MT(\leavevmode),
∣u∣∩∣p∣=∅,
define X=∣u∣, Y=∣π∣∖X, and
assume that
Tξku=Qξk,mξkΦ,
where mξk<ω,
for each ⟨ξ,k⟩∈X.
Consider the set Δ of all multisystems
φ∈MS(π) such that there is a number H>0
and a multitree q∈MS(π) satisfying conditions
(1)
∣q∣∩X=∅ and q⩽p;
2. (2)
if ⟨ξ,k⟩∈X then
⟨ξ,k,mξk⟩∈∣φ∣;
3. (3)
if ⟨ξ,k,m⟩∈∣φ∣ then
hφ(ξ,k,m)=H;
(but not (4) though)
as in the proof of Theorem 4.1,
along with two more requirements
(5)
⟨η,K,m⟩∈∣φ∣ —
hence still hφ(η,K,m)=H by (3);
2. (6)
if s∈2H and τ∈(2H)X
then s(φ,τ)∪q
directly forces c∈/[TηK,mφ(s)].
Lemma 5.2**.**
Δ* is dense in MS(π).*
Proof**.**
Suppose that ψ∈MS(π); we can assume that
ψ already satisfies
(a)
if ⟨ξ,k⟩∈X then
⟨ξ,k,mξk⟩∈∣ψ∣;
2. (b)
there is a number g<ω
such that hψ(ξ,k,m)=g for all ⟨ξ,k,m⟩∈∣ψ∣;
Let H=g+1.
Define a multisystem χ∈MS(π) so that
∣χ∣=∣ψ∣, and
hχ(ξ,k,m)=H, Tξk,mχ(s⌢i)=Tξk,mψ(s)(→i)
for all ⟨ξ,k,m⟩∈∣ψ∣ and s⌢i∈2H;
then ψ≼χ.
We claim that there is a multitree q∈MT(π) satisfying (1), and a multisystem φ∈MS(π) satisfying (6)
and such that still ∣φ∣=∣ψ∣
and hφ(ξ,k,m)=H for all ⟨ξ,k,m⟩∈∣ψ∣,
and in addition
(c)
if ⟨ξ,k⟩∈X and s∈2H then
Tξk,mξkφ(s)⊆Tξk,mξkχ(s),
and we also have TηK,mφ(s)⊆TηK,mχ(s);
2. (d)
Tξk,mφ(s)=Tξk,mχ(s) for all
applicable ξ,k,m,s not covered by (c).
To achieve (6) in one step for one particular
τ∈(2H)X, consider the multitree r=s(χ,τ)∪p.
By Lemma 2.1 and the density assumption
of the theorem,
there is a multitree r′∈MT(φ), r′⩽r, which
directly forces c∈/[TηKr′], and there are
multitrees Us∈MT(φ), s∈2H, such that
Us⊆TηK,mχ(s) and r′ directly forces
c∈/[Us], ∀s.
Let χ′ be obtained from χ by the following
reassignment.
(I)
We set
Tξk,mξkχ′(τ(ξ,k))=Tξkr′
for all ⟨ξ,k⟩∈X.
2. (II)
If s∈2H, and either ⟨η,K⟩∈/X,
or m=mηK, or s=τ(η,K) then
we set
TηK,mχ′(s)=Us.
(Note that if ⟨η,K⟩∈X and m=mηK
then the tree
TηK,mχ′(τ(η,K))=TηKr′
is already defined by (I).)
Let p′=r′↾Y, so that r′=s(χ′,τ)∪p′.
By construction the tree p′ satisfies (6),
for the system τ chosen,
in the case ⟨η,K⟩∈X, m=mηK, s=τ(η,K)
by (I) and in all other cases by (II).
Now consider another
τ′∈(2H)X and the multitree r′=s(χ′,τ′)∪p′.
There is a multitree r′′∈MT(π), r′′⩽r′,
which which directly forces c∈/[TηKr′]
and c∈/[Us′] for each s∈2H, where
Us′∈MT(φ) and
Us′⊆TηK,mχ′(s) .
Let χ′′ be obtained from χ′ by the the same
reassignment (for τ′ instead of τ).
And so on.
The final multisystem and multitree of this construction will be φ
and q satisfying (1), (2), (3),
(5), (6).
□ (Lemma)
Come back to the theorem.
Note that Δ∈M+, similarly to the proof of
Theorem 4.1.
Therefore, by the lemma, there is an index j
such that the system φ(j) belongs to Δ.
Let this be witnessed by a number H>0 and a
multitree q∈MT(π), such that conditions
(1), (2), (3),
(5), (6)
are satisfied for φ=φ(j).
It remains to prove that
u⊆fin⋁D(c,Q,π)q∣u∣.
Let V consist of all multitrees
v=s(φ(j),τ), where
τ∈(2H)X;
[u]⊆⋃v∈V[v]
by construction.
Further, if s∈2H and v∈V then v∪q
directly forces c∈/[TηK,mφ(j)(s)] by
(6), that is, directly forces
c∈/[TηK,mΦ(s)] in the notation of
Definition 3.1.
Therefore v∪q directly forces
c∈/[QηK,mΦ(s)] since
QηK,mΦ(s)⊆TηK,mΦ(s)
by Lemma 3.3(b).
However Q=QηK,mΦ=⋃s∈2HQηK,mΦ(s)
by Lemma 3.3(a).
It follows that v∪q directly forces
c∈/[Q], that is, v∈D(c,Q,π)q∣u∣.
We conclude that V is a (finite) subset of
D(c,Q,π)q∣u∣.
And this accomplishes the proof of
u⊆fin⋁D(c,Q,π)q∣u∣.
∎
6 Consequences for reals in generic extensions
We first prove a result saying that all reals in
MT(π)-generic extensions are adequately represented
by real names.
Then Theorem 6.2 will show effects of the
property of being a non-principal name.
Proposition 6.1**.**
Suppose that π is a regular multiforcing, G⊆MT(π) is
generic over the ground set universe V,
and x∈V[G]∩ωω. Then
(i)
there is a true π-real name c∈V
such that x=c[G];
2. (ii)
if MT(π) is a CCC forcing in V
then there is a small true
π-real name d∈V with x=d[G].
Proof**.**
(i)
is an instances of a general forcing theorem
(see Remark 1.5 on the effect of regularity).
To prove (ii), pick a real name c by (i),
extend each set Knc=⋃iKnic
to an open dense set On by closing strongwards,
choose maximal antichains An⊆On in those sets
— which have to be countable by CCC, and then let
Ani=An∩Knic and
d={⟨p,n,i⟩:\linebreak[0]p∈Ani}.
∎
Theorem 6.2**.**
Let π be a regular multiforcing.
Then
(i)
if a set G⊆MT(π) is generic over the ground set
universe V, ⟨ξ,k⟩∈∣π∣,
and x∈V[G]∩ωω,
then x=xξk[G] if and only if
there is a
true π-real name c,
non-principal over π at ξ,k
and such that x=c[G].
2. (ii)
if c is a π-real name, ⟨ξ,k⟩∈∣π∣,
** is a multiforcing,
π⊏ξkc\leavevmode, and a set G⊆MT(π∪cw\leavevmode) is generic
over V then
c[G]∈/⋃Q∈\leavevmode(ξ,k)[Q].
Proof**.**
(i)
Suppose that x=xξk[G].
By a known forcing theorem, there is a
true π-real name c such that x=c[G] and
MT(π) forces that c=xξk[G].
It remains to show that
c is a non-principal name over π at ξ,k.
We have to prove that the set
[TABLE]
is open dense in MT(π).
The openness is clear, let us prove the density.
Consider an arbitrary q∈MT(π).
Then qMT(π)-forces c=xξk[G] by the
choice of c, hence we can assume that, for some n,
it is MT(π)-forced by q that
c(n)=xξk[G](n).
Then by Lemma 2.1(i) there is a multitree p∈MT(π), p⩽q, and a string s∈ωn+1,
such that pMT(π)-forces s⊆c.
Now it suffices to show that s∈/Tξkp.
Suppose otherwise: s∈Tξkp.
Then the tree T=Tξkp↾s still belongs to MT(π).
Therefore the multitree r defined by
Tξkr=T and
Tξ′k′r=Tξ′k′p for each pair
⟨ξ′,k′⟩=⟨ξ,k⟩, belongs to MT(π) and
satisfies r⩽p⩽q.
However r directly forces both
c(n) and xξk[G](n)
to be equal to one and the same value ℓ=s(n), which
contradicts to the choice of n.
To prove the converse let c∈V
be a real name non-principal over π at ξ,k,
and x=c[G].
Assume to the contrary that ⟨ξ,k⟩∈∣π∣ and
x=xξk[G].
There is a multitree q∈G which MT(π)-forces
c=xξk[G].
As c is non-principal,
there is a stronger multitree p∈G∩Dξkπ(c),
p⩽q.
Thus p directly forces c∈/[Tξkp], and hence
MT(π)-forces the same statement.
Yet pMT(π)-forces {\overset{\text{\hskip 2.15277pt{}_{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi k}\in[T^{{\boldsymbol{p}}}_{\xi k}],
of course, and this is a contradiction.
(ii)
Suppose towards the contrary that
Q∈\leavevmode(ξ,k) and
c[G]∈[Q].
By definition, locks, over π, the set
[TABLE]
Therefore in particular D(c,Q,π) is pre-dense in
MT(π∪cw\leavevmode) by Lemma 2.3.
We conclude that G∩D(c,Q,π)=∅.
In other words, there is a multitree r∈MT(π)
which directly forces c∈/[Q].
It easily follows that c[G]∈/[Q],
which is a contradiction.
∎
7 Combining refinement types
Here we summarize the properties
of generic refinements considered above.
The next definition combines the
refinement types ⊏D, ⊏D, ⊏ξkc.
Definition 7.1**.**
Suppose that π⊏\leavevmode are multiforcings
and M∈HC is any set.
Let π⊏⊏M\leavevmode
mean that the four following requirements hold:
(1)
if ⟨ξ,k⟩∈∣π∣, D∈M, D⊆π(ξ,k),
D is pre-dense in
π(ξ,k), then
π(ξ,k)⊏D\leavevmode(ξ,k);
2. (2)
if D∈M, D⊆MT(π),
D is open dense in MT(π),
then π⊏D\leavevmode;
3. (3)
if c∈M is a π-real name then π⊏c\leavevmode;
4. (4)
if ⟨ξ,k⟩∈∣π∣ and c∈M is a
π-real name, non-principal over π at ξ,k,
then π⊏ξkc\leavevmode.∎
Let π,\leavevmode,σ be multiforcings and
M be a countable set.
Then:
(i)
if π⊏⊏M\leavevmode⊏σ then π⊏⊏Mσ;
2. (ii)
if ⟨πα⟩α<λ
is a ⊏-increasing sequence in MF,
0<μ<λ, π=⋃α<μcwπα,
and π⊏⊏Mπμ, then
π⊏⊏M\leavevmode=⋃μ≤α<λcwπα.∎
Corollary 7.3**.**
If π is a small multiforcing, M∈HC, and
is an M-generic refinement of π(exists by Proposition 3.2!),
then
π⊏⊏M\leavevmode.
Proof**.**
We have π⊏⊏M\leavevmode by a combination of
3.3(ii), 4.1, 3.2, and
5.1.
∎
IV The forcing notion
In this chapter we define the forcing notion to prove
the main theorem.
It will have the form MT(\nmiΠ), for a certain multiforcing \nmiΠ with ∣\nmiΠ∣=ω1×ω.
The multiforcing \nmiΠ will be equal to the componentwise
union of terms of a certain
increasing sequence \vv\nmiΠ of small multiforcings.
And quite a complicated construction of this sequence
in L will make use
of some ideas related to diamond-style constructions,
as well as to some sort of definable genericity.
1 Increasing sequences of small multiforcings
Recall that MF is the set of all multiforcings (Section 4).
Let sMF⊆MF be the set of all
small special multiforcings; s accounts for both
small and special.
Thus a multiforcing π∈MF belongs to sMF if ∣π∣
is (at most) countable and if ⟨ξ,k⟩∈∣π∣ then
π(ξ,k) is a small special (Definition 2.4)
forcing in PTF.
Definition 1.1**.**
Let \vvsMF, resp., \vvsMFω1 be the set of all
⊏-increasing sequences
\vvπ=⟨πα⟩α<κ of
multiforcings πα∈sMF,
of length κ=dom(\vvπ)<ω1, resp., κ=ω1,
which are domain-continuous, in the sense that
if λ<κ is a limit ordinal then
∣πλ∣=⋃α<λ∣πα∣.
Sequences in \vvsMF∪\vvsMFω1 are called multisequences.
We order \vvsMF∪\vvsMFω1 by the usual
relations ⊆ and ⊂ of extension of sequences.
•
Thus
\vvπ⊂\vv\leavevmode iff κ=dom(\vvπ)<λ=dom(\vv\leavevmode) and
πα=\leavevmodeα for all α<κ.
•
In this case, if M is any set, and \leavevmodeκ
(the first term of \vv\leavevmode absent in \vvπ)
satisfies π⊏⊏M\leavevmodeκ, where
π=⋃α<κcwπα,
then we write \vvπ⊂M\vv\leavevmode.
If \vvπ is a multisequence in \vvsMF∪\vvsMFω1 then
let MT(\vvπ)=MT(π), where
π=⋃cw\vvπ=⋃α<κcwπα
(componentwise union), and κ=dom\vvπ.
Accordingly a (true) \vvπ-real name will mean
a (true) π-real name.
∎
Corollary 1.2**.**
Suppose that κ<λ<ω1, M is a countable set,
and \vvπ=⟨πα⟩α<κ is a multisequence in \vvsMF.
Then:
(i)
the componentwise union
π=⋃cw\vvπ=⋃α<κcwπα is
a regular multiforcing*;***
2. (ii)
there is a multisequence \vv\leavevmode∈\vvsMF satisfying
dom(\vv\leavevmode)=λ and \vvπ⊂M\vv\leavevmode;
3. (iii)
if moreover ⟨sα⟩α<λ is
an ⊂-increasing sequence of countable sets
sα⊆ω1×ω,
sα=∣πα∣ for all α<κ,
and sγ=⋃α<γsα for all
limit γ<λ, then
there is a multisequence \vv\leavevmode∈\vvsMF satisfying
dom(\vv\leavevmode)=λ,
∣\leavevmodeα∣=sα for all α<λ,
and \vvπ⊂M\vv\leavevmode;
4. (iv)
if \vvπ,\vvρ,\vv\leavevmode∈\vvsMF
and \vvπ⊂M\vvρ⊆\vv\leavevmode then
\vvπ⊂M\vv\leavevmode;
5. (v)
if \vv\leavevmode=⟨\leavevmodeα⟩α<λ∈\vvsMF and
\vvπ⊂M\vv\leavevmode then
π=⋃α<κcwπα⊏⊏M\leavevmodeβ
whenever λ≤β<μ, and also
π⊏⊏M\leavevmode′=⋃λ≤β<μcw\leavevmodeβ,
therefore
(a)
MT(\leavevmode′)* is open dense in MT(\vv\leavevmode),*
2. (b)
if ⟨ξ,k⟩∈∣π∣, D∈M, D⊆π(ξ,k),
D is pre-dense in π(ξ,k), then
D remains pre-dense in π(ξ,k)∪\leavevmode(ξ,k),
3. (c)
*if D∈M, D⊆MT(\vvπ),
D is open dense in MT(\vvπ),
then D is pre-dense in MT(π∪cw\leavevmode′)=MT(\vv\leavevmode).
*
(ii)
We define terms \leavevmodeα of the multisequence required
by induction.
Naturally put \leavevmodeα=πα for each α<κ.
Now suppose that κ≤γ<λ, multiforcings
\leavevmodeα, α<γ, are defined, and
\vvρ=⟨\leavevmodeα⟩α<γ is a multisequence in \vvsMF.
To define \leavevmodeγ, assume first that γ is limit.
Let ρ=⋃cw\vvρ=⋃α<γcw\leavevmodeα
(componentwise union).
We can assume that M contains \vvρ and satisfies
γ⊆M (otherwise take a bigger set).
By Proposition 3.2, there is an M-generic
refinement of ρ.
By Theorem 3.3, is small special multiforcing,
ρ⊏\leavevmode, and ρα⊏\leavevmode for all α<γ.
In addition ρ⊏⊏M\leavevmode by Corollary 7.3.
We let ργ=\leavevmode.
The extended multisequence \vvρ+=⟨ρα⟩α<γ+1
belongs to \vvsMF and satisfies \vvρ⊂M\vvρ+.
(iii)
The proof is similar, with the extra care of
∣\leavevmodeα∣=sα.
To prove the main claim of (v) make use of
Corollary 7.2.
(iv)
The relation \vvπ⊂M\vv\leavevmode involves only the first
term of \vv\leavevmode absent in \vvπ.
(v)(b)
As π⊏⊏M\leavevmode′ and D∈M,
we have π(ξ,k)⊏D\leavevmode(ξ,k).
Therefore D is pre-dense in \leavevmode(ξ,k) by
Lemma 1.4(ii).
(v)(c)
Similarly π⊏D\leavevmode′, D is pre-dense in
MT(\vv\leavevmode) by
Lemma 2.3(i).
∎
Our plan regarding the forcing notion for Theorem 1.1
will be to define a certain multisequence \vv\nmiΠ in \vvsMFω1 and
the ensuing multiforcing \nmiΠ=⋃cw\vv\nmiΠ with
remarkable properties related to definability and its own
genericity of some sort.
But we need first to introduce an important notion
involved in the construction.
2 Layer restrictions of multiforcings and deciding sets
The construction of the mentioned multiforcing \nmiΠ will
be maintained in such a way that different
layers⟨\nmiΠ(k,ξ)⟩ξ<ω1, k<ω,
appear rather independent of each other, albeit the
principal inductive parameter will be ξ rather than k.
To reflect this feature, we introduce here a suitable
notation related to layer restrictions.
If m<ω then, using a special “layer restriction”
symbol ↾↾ to provide a transparent
distinction from the ordinary restriction ↾,
we define sets of multitrees:
[TABLE]
and, given a multiforcing π, define
MT(π)↾↾<m, MT(π)↾↾≥m, MT(π)↾↾m similarly.
Accordingly if p∈MT then define
the layer restrictionp↾↾<m∈MT↾↾<m so that
∣p↾↾<m∣={⟨ξ,k⟩∈∣p∣:\linebreak[0]k<m}
and p↾↾<m(ξ,k)=π(ξ,k) whenever
⟨ξ,k⟩∈∣p↾↾<m∣.
Define
p↾↾≥m∈MT↾↾≥m,
p↾↾m∈MT↾↾m similarly.
The same definitions are maintained with multiforcings:
[TABLE]
and MF↾↾<m, MF↾↾≥m, MF↾↾m are defined similarly.
Accordingly if π∈MF (in particular if π∈sMF)
and m<ω then define
the layer restrictionπ↾↾<m∈MF↾↾<m (resp., ∈sMF↾↾<m), so that
∣π↾↾<m∣={⟨ξ,k⟩∈∣π∣:\linebreak[0]k<m}
and π↾↾<m(ξ,k)=π(ξ,k) whenever
⟨ξ,k⟩∈∣π↾↾<m∣.
Define
π↾↾≥m∈MF↾↾≥m,
π↾↾m∈MF↾↾m similarly.
A similar notation applies to multisequences
(Definition 1.1).
If m<ω then we let \vvsMF↾↾<m, \vvsMF↾↾≥m, \vvsMF↾↾m
be the set of all multisequences in \vvsMF
whose all terms belong to resp. sMF↾↾<m, sMF↾↾≥m, sMF↾↾m.
Define similarly \vvsMFω1↾↾<m, \vvsMFω1↾↾≥m, \vvsMFω1↾↾m
(multisequences of length ω1).
And further,
if \vvπ=⟨πα⟩α<κ∈\vvsMF and m<ω then
define
\vvπ↾↾<m=⟨πα↾↾<m⟩α<κ∈\vvsMF↾↾<m,
and define
\vvπ↾↾≥m∈\vvsMF↾↾≥m, \vvπ↾↾m∈\vvsMF↾↾m similarly.
The same for \vvπ=⟨πα⟩α<ω1∈\vvsMFω1
Definition 2.1**.**
Assume that m<ω.
A multisequence \vvπ∈\vvsMFm-decides a set W if either
\vvπ↾↾≥m
belongs to W (positive decision)
or there is no multisequence \vv\leavevmode∈W∩\vvsMF↾↾≥m
extending \vvπ↾↾≥m (negative decision).
∎
Lemma 2.2**.**
If \vvπ∈\vvsMF,
M is countable, W is any set, and m<ω,
then there is a multisequence \vv\leavevmode∈\vvsMF such that
\vvπ⊂M\vv\leavevmode and \vv\leavevmodem-decides W.
Proof**.**
By Corollary 1.2, there is a multisequence \vvρ∈\vvsMF such that \vvπ⊂M\vvρ.
Then either \vvρ outright m-decides W negatively,
or there is a sequence \vvσ∈W∩\vvsMF↾↾≥m
satisfying \vvρ↾↾≥m⊆\vvσ.
On the other hand, using Corollary 1.2(iii),
we get a multisequence \vvσ′∈\vvsMF↾↾<m of the same length as \vvσ,
such that \vvρ↾↾<m⊆\vvσ′.
Therefore there exists a multisequence \vv\leavevmode∈\vvsMF of that
same length, satisfying \vv\leavevmode↾↾≥m=\vvσ and
\vv\leavevmode↾↾<m=\vvσ′ — then obviously \vvρ⊆\vv\leavevmode
and by definition \vv\leavevmode decides W positively.
Finally we have \vvπ⊂M\vvρ⊆\vv\leavevmode,
and hence \vvπ⊂M\vv\leavevmode by Corollary 1.2(iv).
∎
3 Auxiliary diamond sequences
Recall that HC is the set of all
hereditarily countable sets (those with finite or
countable transitive closures).
The next theorem employs the technique of diamond sequences
in L.
Theorem 3.1** (in L).**
There exist Δ1HC sequences
⟨\vvπ⌈μ⌉⟩μ<ω1,
⟨D⌈μ⌉⟩μ<ω1,
⟨z⌈μ⌉⟩μ<ω1,
such that, for every μ,
D⌈μ⌉ and z⌈μ⌉ are sets in HC,
\vvπ⌈μ⌉∈\vvsMF,
dom(\vvπ⌈μ⌉)=μ,
and in addition if
\vv\nmiΠ=⟨\nmiΠν⟩ν<ω1∈\vvsMFω1,
z∈HC, and D⊆MT(\vv\nmiΠ),
then the set M of all ordinals μ<ω1 such that
(a)
z⌈μ⌉=z;**
2. (b)
\vvπ⌈μ⌉* is equal to the restricted sub-multisequence
\vv\nmiΠ↾μ=⟨\nmiΠν⟩ν<μ;*
3. (c)
D⌈μ⌉=D∩MT(\vv\nmiΠ↾μ);**
is stationary in ω1.
Proof**.**
Arguing in L, the constructible universe,
we
let ⩽L be the canonical wellordering of L.
It is known that ⩽L orders HC similarly to
ω1, and that ⩽L is Δ1HC and has the
goodness property: the set of
all ⩽L-initial segments
Ix(⩽L)={y:\linebreak[0]y⩽Lx}, x∈HC, is still Δ1HC.
We begin with a Δ1HC sequence of sets
Sα⊆α, α<ω1, such that
(A)
if
X⊆HC then the set {α<ω1:\linebreak[0]Sα=X∩α}
is stationary in ω1.
This is a well-known instance of the diamond
principle true in L.
The additional definability property can be achieved
by taking the ⩽L-least possible Sα at each
step α.
We get the following two results as easy corollaries.
First, let Aμ={cα:\linebreak[0]α∈Sμ}, where cα is
the α-th element of HC in the sense of the
ordering ⩽L.
Then ⟨Aμ⟩μ<ω1 is still a Δ1HC sequence,
and
(B)
if Xα∈HC for all α<ω1 then
the set {μ:\linebreak[0]Aμ={Xα:\linebreak[0]α<μ}}
is stationary in ω1.
Second, for any α, if
Aα=⟨aγ⟩γ<α, where each aγ itself is
equal to an ω-sequence ⟨aγn⟩n<ω,
then let Bαn=⟨aγn⟩γ<α for all n.
Otherwise let Bαn=∅, ∀n.
Then \big{\langle}B_{\alpha}\big{\rangle}{}^{n<\omega}_{\alpha<\omega_{1}} is still a Δ1HC
system of sets in HC, such that
(C)
if Xαn∈HC for all α<ω1, n<ω, then,
for every μ<ω1, the set {μ:\linebreak[0]∀n(Bμn={Xαn:\linebreak[0]α<μ}}
is stationary in ω1.
Now things become more routinely complex.
Let μ<ω1.
We define z⌈μ⌉=⋃Bμ0.
If Bμ1∈\vvsMF and dom(Bμ1)=μ
then let \vvπ⌈μ⌉=Bμ1;
otherwise let \vvπ⌈μ⌉ be equal to the ⩽L-least
multisequence in \vvsMF of length μ.
(Those exist
by Corollary 1.2(ii).)
Finally we let D⌈μ⌉=⋃Bμ+12.
Let’s show that the sequences of sets \vvπ⌈μ⌉,
D⌈μ⌉, z⌈μ⌉ prove the theorem.
Suppose that \vv\nmiΠ=⟨\nmiΠν⟩ν<ω1∈\vvsMFω1,
z∈HC, and D⊆MT(\vv\nmiΠ).
Let Xα0=z, Xα1=⟨α,\nmiΠα⟩,
Xα2=D∩MT(\vv\nmiΠ↾α) for all α.
The set
[TABLE]
is stationary by (C).
Assume that μ∈M.
Then Bμ0={Xα0:\linebreak[0]α<μ}={z},
therefore z⌈μ⌉=z.
Further
Bμ1={Xα1:\linebreak[0]α<μ}={⟨α,\nmiΠα⟩:\linebreak[0]α<μ}=\vv\nmiΠ↾μ∈\vvsMF,
therefore \vvπ⌈μ⌉=\vv\nmiΠ↾μ.
Finally we have
D⌈μ⌉=⋃Bμ+12=⋃α≤μXα2=D∩MT(\vv\nmiΠ↾μ), as required.
∎
4 Key sequence theorem
Now we prove a theorem which
introduces the key multisequence \vv\nmiΠ.
Theorem 4.1** (V=L).**
There exists a multisequence
\vv\nmiΠ=⟨\nmiΠα⟩α<ω1∈\vvsMFω1 satisfying
the following requirements:
(i)
if m<ω then the multisequence
\vv\nmiΠ↾↾m belongs to the class Δm+2HC;
2. (ii)
if m′<ω and W⊆\vvsMF is a Σm′+1HC set
then there is an ordinal γ<ω1 such that the multisequence
\vv\nmiΠ↾γm′-decides W;
3. (iii)
if a set D⊆MT(\vv\nmiΠ) is dense in MT(\vv\nmiΠ),
then the set Z of all ordinals γ<ω1 such that
\vv\nmiΠ↾γ⊂{D∩MT(\vv\nmiΠ↾γ)}\vv\nmiΠ,
is stationary in ω1.
Proof**.**
If m<ω then let unm(p,x) be a canonical universal
Σm+1 formula, so that
the family of all Σm+1HC sets X⊆HC
(those definable in HC by Σm+1 formulas with
parameters in HC)
is equal to the family of all sets
of the form Υm(p)={x∈HC:\linebreak[0]HC⊨unm(p,x)},
p∈HC.
(I)
Fix Δ1HC sequences
⟨\vvπ⌈μ⌉⟩μ<ω1,
⟨D⌈μ⌉⟩μ<ω1, and
⟨z⌈μ⌉⟩μ<ω1
satisfying Theorem 3.1; the terms
D⌈μ⌉,\linebreak[0]z⌈μ⌉,\linebreak[0]\vvπ⌈μ⌉
of the sequences belong to HC, and
in addition
\vvπ⌈μ⌉∈\vvsMF, dom(\vvπ⌈μ⌉)=μ.
2. (II)
Let μ<ω1.
If z⌈μ⌉ is a pair of the form
z⌈μ⌉=⟨m,p⟩ then let m⌈μ⌉=m and
p⌈μ⌉=p, otherwise let
m⌈μ⌉=p⌈μ⌉=0.
3. (III)
If m<ω then let, by Lemma 2.2,
\vvπ⌈μ,m⌉∈\vvsMF be the ⩽L-least multisequence in
\vvsMF which satisfies
\vvπ⌈μ⌉⊂{D⌈μ⌉}\vvπ⌈μ,m⌉ and
m-decides the set Υm(p⌈μ⌉).
Let ⌈μ,m⌉+=dom(\vvπ⌈μ,m⌉);
then μ<⌈μ,m⌉+<ω1.
Proposition 4.2** (in L).**
The sequences
⟨m⌈μ⌉⟩μ<ω1 and
⟨p⌈μ⌉⟩μ<ω1
belong to the definability class Δ1HC.
If m<ω then the sequences
⟨\vvπ⌈μ,m⌉⟩μ<ω1
and ⟨⌈μ,m⌉+⟩μ<ω1
belong to the class Δm+2HC.
Proof**.**
Routine.
Note that \vvπ⌈μ,m⌉ and ⌈μ,m⌉+ depend on m
through the formulas unm(⋅,⋅), whose complexity
strictly increases with m→∞.
∎
Now define a multisequence \vv\nmiΠ=⟨\nmiΠα⟩α<ω1∈\vvsMFω1 and a
family of strictly increasing, continuous
maps μm:ω1→ω1, m<ω,
as follows:
1∘.
Let μm(0)=0 and μm(λ)=supγ<λμm(γ)
for all m and all limit λ<ω1.
2. 2∘.
Suppose that m<ω, γ<ω1, μ=μm(γ), and
the twofold-restricted sequence
(\vv\nmiΠ↾μ)↾↾m=(\vv\nmiΠ↾↾m)↾μ is already
defined.
If the following holds:
(∗)
m≥m′=m⌈μ⌉ and
(\vv\nmiΠ↾μ)↾↾m
coincides with \vvπ⌈μ⌉↾↾m,
then let
μm(γ+1)=⌈μ,m′⌉+ and
(\vv\nmiΠ↾⌈μ,m′⌉+)↾↾m=\vvπ⌈μ,m′⌉↾↾m.
3. 3∘.
In the assumptions of 2∘, if 2^{\circ}$$(*) fails,
then let \vvρ is the ⩽L-least multisequence in \vvsMF with (\vv\nmiΠ↾μ)↾↾m⊂\vvρ
(we refer to Corollary 1.2),
and define μm(γ+1)=dom(\vvρ) and
(\vv\nmiΠ↾μm(γ+1))↾↾m=\vvρ↾↾m.
To conclude, given γ<ω1 and m, if an ordinal
μ=μm(γ), and a multisequence (\vv\nmiΠ↾μ)↾↾m=(\vv\nmiΠ↾↾m)↾μ
are defined, then items 2∘, 3∘ define
a bigger ordinal μm(γ+1)>μ=μm(γ) and
a longer multisequence (\vv\nmiΠ↾μm(γ+1))↾↾m
satisfying
(\vv\nmiΠ↾μ)↾↾m⊂(\vv\nmiΠ↾μm(γ+1))↾↾m.
Thus overall items 1∘, 2∘, 3∘
of the definition
contain straightforward instructions as how to uniquely define
the layers \vv\nmiΠ↾↾m and maps μm for
different m<ω, independently from each other.
From now on, fix a multisequence \vv\nmiΠ=⟨\nmiΠα⟩α<ω1∈\vvsMFω1
of multiforcings \nmiΠα∈sMF and
increasing continuous maps μm:ω1→ω1
defined by 1∘, 2∘, 3∘.
As the maps μm are continuous, the following holds:
Proposition 4.3** (in L).**
C={γ<ω1:\linebreak[0]∀m(γ=μm(γ))}* is a club
in ω1.∎*
To show that \vv\nmiΠ proves Theorem 4.1,
we check items (i), (ii), (iii).
(i)
Let m<ω.
Then the multisequence
\vv\nmiΠ↾↾m
and the map μm
belong to the class Δm+2HC by Proposition 4.2;
a routine proof is omitted.
(ii)
Suppose that m′<ω and W⊆\vvsMF is a Σm′+2HC set.
Pick p∈HC such that W=Υm′(p).
Let z=⟨m′,p⟩.
As C is a club, it follows
from the choice of terms
\vvπ⌈μ⌉, D⌈μ⌉, and z⌈μ⌉,
by (I) and Theorem 3.1,
that there is an ordinal γ∈C such that
\vvπ⌈γ⌉=\vv\nmiΠ↾γ and
z⌈γ⌉=z — hence, m⌈γ⌉=m′ and p⌈γ⌉=p.
Let μ=γ; then also μ=μm(γ), ∀m — since
γ∈C, and \vv\nmiΠ↾μ=\vvπ⌈μ⌉.
Then it follows from the choice of \vv\nmiΠ that
item 2∘
of the construction applies for the ordinal γ chosen
and all m≥m′.
It follows that the multisequence \vvρ=\vvπ⌈μ,m′⌉ and
the ordinal ν=μm(γ+1)=⌈μ,m′⌉+ satisfy
ν=dom(\vvρ) and
(\vv\nmiΠ↾ν)↾↾m=\vvρ↾↾m for all m≥m′.
In other words, (\vv\nmiΠ↾ν)↾↾≥m′=\vvρ↾↾≥m′.
However by definition \vvρm′-decides the set
W=Υm′(p), and the definition of this property
depends only on \vvρ↾↾≥m′.
(iii)
Assume that a set D⊆MT(\vv\nmiΠ) is dense in MT(\vv\nmiΠ),
and C⊆C is a club in ω1.
Following the proof of (ii), we find
an ordinal γ∈C such that
\vvπ⌈γ⌉=\vv\nmiΠ↾γ, m⌈γ⌉=0, and
D⌈γ⌉=D∩MT(\vv\nmiΠ↾γ),
Note that γ=μm(γ), ∀m.
We have \vvπ⌈γ⌉⊂{D⌈γ⌉}\vvπ⌈γ,0⌉
by (III) (with μ=γ),
that is,
[TABLE]
Yet it follows from the choice of γ that
condition 2^{\circ}$$(*) holds (for μ=γ) for all m≥0.
Then, by definition 2∘, the ordinal
μ+=⌈γ,m⌉+ satisfies μ+=μm(γ+1)
and (\vv\nmiΠ↾μ+)↾↾m=(\vvπ⌈γ,0⌉)↾↾m
for all m, that is, just \vv\nmiΠ↾μ+=\vvπ⌈γ,0⌉.
We conclude that
\vv\nmiΠ↾γ⊂{D∩MT(\vv\nmiΠ↾γ)}\vv\nmiΠ↾μ+
by (†), therefore we have
\vv\nmiΠ↾γ⊂{D∩MT(\vv\nmiΠ↾γ)}\vv\nmiΠ,
as required.
□ (Theorem 4.1)
Definition 4.4** (in L).**
From now on we fix a multisequence
\vv\nmiΠ=⟨\nmiΠα⟩α<ω1∈\vvsMFω1 satisfying
requirements
of Theorem 4.1, that is,
(i)
if m<ω then the multisequence
\vv\nmiΠ↾↾m belongs to the class Δm+2HC;
2. (ii)
if m′<ω and W⊆\vvsMF is a Σm′+1HC set
then there is an ordinal γ<ω1 such that the multisequence
\vv\nmiΠ↾γm′-decides W;
3. (iii)
if a set D⊆MT(\vv\nmiΠ) is dense in MT(\vv\nmiΠ),
then the set Z of all ordinals γ<ω1 such that
\vv\nmiΠ↾γ⊂{D∩MT(\vv\nmiΠ↾γ)}\vv\nmiΠ,
is stationary in ω1.
We call \vv\nmiΠthe key multisequence.
∎
A set U⊆sMF↾↾≥m is dense in sMF↾↾≥m if
for each \vvπ∈sMF↾↾≥m there is a multisequence \vv\leavevmode∈U
satisfying \vvπ⊆\vv\leavevmode.
Lemma 4.5**.**
If m<ω and W⊆sMF↾↾≥m is a Σm+1HC set
dense in sMF↾↾≥m then there is an ordinal
γ<ω1 such that (\vv\nmiΠ↾γ)↾↾≥m∈W.
In particular, if W⊆\vvsMF is a Σ1HC set
dense in \vvsMF then there is
γ<ω1 such that \vv\nmiΠ↾γ∈W.
Proof**.**
Apply 4.4(ii).
The negative decision is impossible by the density.
∎
5 Key product forcing
We continue to argue in L, and we’ll make use of
the key multisequence \vv\nmiΠ=⟨\nmiΠα⟩α<ω1
introduced by Definition 4.4.
Definition 5.1** (in L).**
Define the multiforcings
[TABLE]
We further define P=MT(\nmiΠ)=MT(\vv\nmiΠ),
and, for all γ<ω1,
[TABLE]
The multiforcing P will be our principal forcing notion,
the key forcing.
Lemma 5.2** (in L).**
\nmiΠ* is a regular multiforcing.
In addition,
∣\nmiΠ∣=ω1×ω, thus if ξ<ω1
and k<ω then there is an ordinal
α<ω1 such that
⟨ξ,k⟩∈∣\nmiΠα∣.
Therefore
P=∏ξ<ω1,k<ω\nmiΠ(ξ,k)
(with finite support).*
Proof**.**
To prove the additional claim, note that
the set W of all multisequences \vvπ∈\vvsMF satisfying
⟨ξ,k⟩∈∣⋃cw\vvπ∣ is Σ1HC
(with ξ as a parameter of definition).
In addition W is dense in \vvsMF.
(First extend \vvπ by Corollary 1.2
so that is has a non-limit length and the last term,
then make use of Corollary 3.4.)
Therefore by Lemma 4.5
there is an ordinal γ<ω1 such that
\vv\nmiΠ↾γ∈W, as required.
∎
If ξ<ω1 and k<ω then, following the lemma,
let α(ξ,k)<ω1
be the least ordinal α satisfying
⟨ξ,k⟩∈∣\nmiΠα∣.
Thus a forcing \nmiΠα(ξ,k)∈PTF
is defined whenever α satisfies
α(ξ,k)≤α<ω1, and
⟨\nmiΠα(ξ,k)⟩α(ξ,k)≤α<ω1 is a
⊏-increasing sequence of countable special forcings
in PTF.
Note that
\nmiΠ(ξ,k)=⋃α(ξ,k)≤α<ω1\nmiΠα(ξ,k)
by construction.
Corollary 5.3** (in L).**
If k<ω then the sequence of ordinals
⟨α(ξ,k)⟩ξ<ω1 and the sequence of
multiforcings
⟨\nmiΠα(ξ,k)⟩ξ<ω1,α(ξ,k)≤α<ω1
are Δk+2HC.
Proof**.**
By construction the following double equivalence holds:
[TABLE]
However π=\nmiΠα↾↾k is a Δk+2HC relation by
Theorem 4.1(i).
It follows that so is the sequence ⟨α(ξ,k)⟩ξ<ω1.
The second claim easily follows by the same
Definition 4.4(i).
∎
The set C′={γ<ω1:\linebreak[0]∣\nmiΠ<γ∣=γ×ω}
is a club in ω1.∎
Lemma 5.6** (in L).**
P* is CCC.*
Proof**.**
Let A⊆P be a maximal antichain in P.
The set
[TABLE]
is a club in ω1.
Let D={p∈P:\linebreak[0]∃q∈A(p⩽q)};
this is an open dense set.
By Definition 4.4(iii), there is an ordinal
γ∈C such that
\vv\nmiΠ↾γ⊂{D∩P<γ}\vv\nmiΠ.
Recall that γ∈C, hence A∩P<γ is
a maximal antichain in P<γ, thus
D∩P<γ is open dense in P<γ.
Therefore the set D∩P<γ
is pre-dense in the forcing MT(\vv\nmiΠ)=P by
Corollary 1.2(v)(c).
We claim that A=A∩P<γ, so A is countable.
Indeed suppose that r∈A∖P<γ.
Then r is compatible with some q∈D∩P<γ;
let p∈D∩P<γ, p⩽q, p⩽r.
As q∈D, there is some r′∈A with q⩽r′.
Then r=r′ as A is an antichain;
thus q⩽r∈A∖P<γ.
However q∈P<γ and A∩P<γ is
a maximal antichain in P<γ, thus q, and hence r,
is compatible with some r′′∈A∩P<γ.
Which is a contradiction.
∎
Corollary 5.7** (in L).**
If a set D⊆P is pre-dense in P
then there is an ordinal
γ<ω1 such that D∩P<γ is already pre-dense
in P.
Proof**.**
We can assume that in fact D is dense.
Let A⊆D be a maximal antichain in D; then A is
a maximal antichain in P because of the density of D.
Then A⊆P<γ for some γ<ω1 by Lemma 5.6.
But A is pre-dense in P.
∎
V Auxiliary forcing relation
Recall that P=MT(\nmiΠ), the key forcing,
is a product forcing notion defined (in L) in
Section 5.
Its components \nmiΠ(ξ,k) have different complexity
in HC, depending on k by Corollary 5.3,
hence there
is no way the forcing notion P (or \nmiΠ)
as a whole is definable in HC.
Somewhat surprisingly, the P-forcing relation turns
out to be definable in HC when restricted to
analytic formulas
of a certain level of complexity within the usual hierarchy.
This will be established on the base of an auxiliary
forcing relation.
1 Auxiliary forcing: preliminaries
We argue in L.
Consider the 2nd order arithmetic language, with
variables k,l,m,n,… of type [math] over ω and
variables a,b,x,y,… of type 1 over ωω,
whose atomic formulas are those of the form x(k)=n.
Let L be the extension of this language,
which allows to substitute
free variables of type [math] with natural numbers
(as usual) and free variables of type 1 with
small real namesc∈L.
By L-formulas we understand formulas of this
extended language.
We define natural classes LΣn1, LΠn1 (n≥1)
of L-formulas.
Let L(Σ+Π)11 be the closure of LΣ11∪LΠ11 under
¬,\linebreak[0]∧,\linebreak[0]∨ and quantifiers over ω.
If φ is a formula in LΣn1 (resp., LΠn1), then
let φ− be
the result of canonical transformation of ¬φ
to the LΠn1 (resp., LΣn1) form.
If φ is a L-formula and G⊆MT is a
pairwise compatible set of multitrees then let φ[G]
be the result of substitution of c[G] for any
name c in φ.
(Recall Definition 1.2.)
Thus φ[G] is an ordinary 2nd order arithmetic
formula, which may include natural numbers and
elements of ωω as parameters.
We are going to define
a relation pforc\vvπφ between multitrees p,
multisequences \vvπ, and L-formulas φ,
which suitably approximates the true P-forcing
relation.
But it depends on a two more definitions.
Definition 1.1**.**
If m<ω then
\vvsMF[\vv\nmiΠ↾↾<m] consists of all multisequences \vvπ∈\vvsMF such that
\vvπ↾↾<m⊂\vv\nmiΠ↾↾<m, that is,
\vvπ↾↾<m=(\vv\nmiΠ↾↾<m)↾δ, where δ=dom(\vvπ)
— multisequences which agree with the key multisequence \vv\nmiΠ
on layers below m.
Obviously \vvsMF[\vv\nmiΠ↾↾<m+1]⊆\vvsMF[\vv\nmiΠ↾↾<m]⊆\vvsMF[\vv\nmiΠ↾↾<0]=\vvsMF.
∎
If γ<ω1 then the subsequence \vv\nmiΠ↾γ of the
key multisequence \vv\nmiΠ belongs to ⋂m\vvsMF[\vv\nmiΠ↾↾<m], of course.
To prove the next lemma use 4.4(i).
Lemma 1.2**.**
\vvsMF[\vv\nmiΠ↾↾<m]* is a subset of HC of definability class
Δm+1HC.∎*
The other definition deals with models of a
subtheory of ZFC.
Definition 1.3**.**
Let ZFL– be the theory containing all axioms of
ZFC− (minus the Power Set axiom) plus the axiom
of constructibility V=L.
Any transitive model (TM) of ZFL– has the form
Lα, where α∈Ord.
Therefore it is true in L that for any set x
there is a least TM M=M(x) of ZFL–
containing x.
If x∈HC
(HC= all hereditarily countable sets) then
M(x) is a countable transitive model (CTM),
equal to the least CTM of ZFL– containing x.
∎
2 Auxiliary forcing
The definition of pforc\vvπφ goes on by
induction on the complexity of φ.
1∘.
Let φ is a closed L(Σ+Π)11 formula, \vvπ∈\vvsMF,
p∈MT, but p∈MT(\vvπ) is not necessarily assumed.
We define:
(a)
pforc\vvπφ iff
there is a CTM M⊨ZFL–,
an ordinal ϑ<dom\vvπ,
and a multitree p0∈MT(\vvπ↾ϑ),
such that p⩽p0 (meaning: p is stronger),
the model M contains \vvπ↾ϑ
(then contains MT(\vvπ↾ϑ) as well)
and contains φ
(that is, all names in φ),
\vvπ↾ϑ⊂M\vvπ, and
p0MT(\vvπ↾ϑ)-forces φ[G]
over M (in the usual sense)
;
2. (b)
pwforc\vvπφ (weak forcing) iff
there is no multisequence \vvπ′∈\vvsMF and p′∈MT(\vvπ′)
such that \vvπ⊆\vvπ′, p′⩽p,
and p′forc\vvπ′¬φ.
2. 2∘.
If φ(x) is a LΠn1 formula, n≥1, then
we define pforc\vvπ∃xφ(x) iff there is a
small real name c
such that pforc\vvπφ(c).
3. 3∘.
If φ is a closed LΠn1 formula, n≥2,
then we define pforc\vvπφ iff
\vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2], and there is no multisequence \vvπ′∈\vvsMF[\vv\nmiΠ↾↾<n−2] and multitree p′∈MT(\vvπ′)
such that \vvπ⊆\vvπ′,
p′⩽p,
and p′forc\vvπ′φ−. 555 If \vvπ does not belong to \vvsMF[\vv\nmiΠ↾↾<n−2]
in 3∘, then pforc\vvπφ holds
for any LΠn1 formula φ
by default as a multisequence not in \vvsMF[\vv\nmiΠ↾↾<n−2] is
definitely not
extendable to a multisequence in \vvsMF[\vv\nmiΠ↾↾<n−2].
This motivates the condition \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2]
in 3∘.
Remark 2.1**.**
With p0 and ϑ given, the premise
“p0MT(\vvπ↾ϑ)-forces φ[G]
over M”
of 1∘a does not depend on the
choice of a CTM M containing \vvπ↾ϑ
and φ,
since if φ is L(Σ+Π)11 then the formula φ[G]
(in which all names are evaluated by some
MT(\vvπ↾ϑ)-generic set G as in 1.2)
in simultaneously true or false in all transitive
models by the Shoenfield absoluteness theorem.
∎
Remark 2.2**.**
It easily holds by induction that if pforc\vvπφ
then \vvπ∈\vvsMF,
φ is a closed formula in one of
the classes L(Σ+Π)11,LΣn1,LΠn1, n≥2,
and if n≥2 and φ∈LΠn1∪LΣn+11
then \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2].
∎
Lemma 2.3**.**
Assume that multisequences \vvπ⊆\vv\leavevmode belong to \vvsMF,
q,p∈MT,
q⩽p,
φ is an L-formula as in 2.2,
and if n≥2 and φ∈LΠn1∪LΣn+11
then \vvπ,\vv\leavevmode∈\vvsMF[\vv\nmiΠ↾↾<n−2].
Then pforc\vvπφ implies qforc\vv\leavevmodeφ,
and if φ belongs to L(Σ+Π)11 then
pwforc\vvπφ implies qwforc\vv\leavevmodeφ
as well.
Proof**.**
If φ is a L(Σ+Π)11 formula,
pforc\vvπφ, and this is witnessed
by M, ϑ, p0 as in 1∘a,
then the exactly same M, ϑ, p0
witness qforc\vv\leavevmodeφ.
Now the induction step ∀, as in 3∘.
Let φ be a closed LΠn1-formula, n≥2, and
pforc\vvπφ.
Assume to the contrary that qforc\vv\leavevmodeφ
fails.
Then by 3∘ there exist:
a multisequence \vv\leavevmode′∈\vvsMF[\vv\nmiΠ↾↾<n−2] and multitree q′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊆\vv\leavevmode′, q′⩽q,
and q′forc\vv\leavevmode′φ−.
But then \vvπ⊆\vv\leavevmode′ and q′⩽p,
hence pforc\vvπφ fails by 3∘, which is
a contradiction.
The additional result for wforc and L(Σ+Π)11 formulas
is entirely similar to the induction step ∀ as
just above.
∎
If K is one of the classes
L(Σ+Π)11, LΣn1, LΠn1 (n≥2), then let FORC[K] consist
of all triples ⟨\vvπ,p,φ⟩ such that
\vvπ∈\vvsMF, p∈MT(\vvπ), φ
is a closed L-formula of class K,
and if n≥2 and φ∈LΣn1∪LΠn1
then \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2],
and finally pforc\vvπφ.
Then FORC[K] is a subset of HC.
Lemma 2.4** (definability, in L).**
FORC[L(Σ+Π)11]*
belongs to Δ1HC.
If n≥2 then
FORC[LΣn1] belongs to Σn−1HC
and FORC[LΠn1] belongs to Πn−1HC.*
Proof**.**
Relations like “being an MSP”,
“being a formula in L(Σ+Π)11, LΣn1, LΠn1”,
p∈MT(\vvρ), forcing over a CTM, etc. are definable in HC by bounded formulas, hence
Δ1HC.
On the top of this, the model M can be
tied by both ∃ and ∀ in 1∘a,
see Remark 2.1.
This wraps up the Δ1HC estimation for L(Σ+Π)11.
Now the step by 3∘.
Assume that
n≥2, and it is already established that
FORC[LΣn1]∈Σn−1HC.
Then ⟨\vvπ,p,φ⟩∈FORC[LΠn1]
iff \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2], p∈MT, φ
is a closed LΠn1 formula in M(\vvπ),
and, by 3∘, there exist no triple
⟨\vvπ′,p′,ψ⟩∈FORC[LΣn1]
such that \vvπ′∈\vvsMF[\vv\nmiΠ↾↾<n−2],
\vvπ⊆\vvπ′, p′∈MT(\vvπ′), p′⩽p,
and ψ is φ−.
Evaluating the key conjunct \vvπ′∈\vvsMF[\vv\nmiΠ↾↾<n−2] by
Lemma 1.2 as Δn−1HC, we get a required
estimation Πn−1HC of FORC[LΠn1].
∎
3 Forcing simple formulas
We still argue in L.
The following results are mainly related to
the relation forc with respect to
formulas in the class L(Σ+Π)11.
Lemma 3.1** (in L).**
*Assume that \vvπ∈\vvsMF, \vv\leavevmode∈\vvsMF∪\vvsMFω1,
\vvπ⊆\vv\leavevmode, p∈MT(\vvπ),
φ is a formula in L(Σ+Π)11,
N⊨ZFL– is a TM containing \vv\leavevmode and φ,
and pforc\vvπφ.
Then pMT(\vv\leavevmode)-forces φ[G]
over N.
*
Proof**.**
By definition there is an ordinal ϑ<dom\vvπ,
a multitree p0∈MT(\vvπ↾ϑ),
and a CTM M⊨ZFL– containing φ and
\vvπ↾ϑ, such that
\vvπ↾ϑ⊂M\vvπ, p⩽p0,
and
p0MT(\vvπ↾ϑ)-forces φ[G]
over M.
We can w. l. o. g. assume that M⊆N
(by the same reference to Shoenfield as in Remark 2.1).
Now suppose that G⊆MT(\vv\leavevmode) is a set
MT(\vv\leavevmode)-generic
over N and p∈G — then p0∈G, too.
We have to prove that φ[G] is true in N[G].
We claim that the set G′=G∩MT(\vvπ↾ϑ) is
MT(\vvπ↾ϑ)-generic over M.
Indeed, let a set D∈M, D⊆MT(\vvπ↾ϑ),
be open dense in MT(\vvπ↾ϑ).
Then, as \vvπ↾ϑ⊂M\vv\leavevmode by
Corollary 1.2(iv),
D is pre-dense in MT(\vv\leavevmode)
by 1.2(v)(c),
and hence G∩D=∅ by the choice of G.
It follows that G′∩D=∅.
We claim that c[G]=c[G′] for any name
c∈M, in particular, for any name in φ.
Indeed, as G′⊆G, the otherwise occurs
by Definition 1.2 only if for some n,i
and q′∈Knic there is q∈G satisfying
q⩽q′, but there is no such q in G′.
Let D consist of
all multitrees r∈MT(\vvπ↾ϑ) either satisfying
r⩽q′ or somewhere a. d. with q′.
Then D∈M and D is open dense in
MT(\vvπ↾ϑ).
Therefore D∩G′=∅ by the above, so let
r∈D∩G′.
If r⩽q′ then we get a contradiction with the
choice of q′.
If r is somewhere a. d. with q′ then
we get a contradiction with the choice of q as
both q,r belong to the generic filter G.
It follows that φ[G] coincides with φ[G′].
Note also that p0∈G′.
We conclude that φ[G′] is true in M[G′] as
p0 forces φ[G] over M.
The same formula φ[G] is true in
N[G] by Shoenfield.
∎
Lemma 3.2**.**
Let \vvπ∈\vvsMF, p∈MT(\vvπ),
φ be a formula in L(Σ+Π)11.
Then
(i)
pforc\vvπφ* and pforc\vvπ¬φ
cannot hold together**;***
2. (ii)
if pforc\vvπφ then pwforc\vvπφ;
3. (iii)
if pwforc\vvπφ then there is a multisequence \vv\leavevmode∈\vvsMF such that \vvπ⊂M(\vvπ)\vv\leavevmode
and pforc\vv\leavevmodeφ;
4. (iv)
pwforc\vvπφ* and pwforc\vvπ¬φ
cannot hold together.*
Proof**.**
(i)
Otherwise pMT(\vvπ)-forces both φ[G]
and ¬φ[G] over a large enough CTM M, by
Lemma 3.1, which cannot happen.
(ii)
Assume that pwforc\vvπφ fails, hence there is
a multisequence \vv\leavevmode∈\vvsMF and a multitree q∈MT(\vv\leavevmode)
such that q⩽p and qforc\vvπ¬φ.
But Lemma 2.3 implies qforc\vvπφ,
which contradicts to (i).
(iii)
Let M⊨ZFL– be a CTM containing φ and \vvπ.
By Corollary 1.2(ii),
there is a multisequence multisequence \vv\leavevmode∈\vvsMF with \vvπ⊂M\vv\leavevmode.
We claim that pMT(\vvπ)-forces
φ[G]
over M in the usual sense — then by
definition pforc\vv\leavevmodeφ (via ϑ=dom\vvπ),
and we are done.
To prove the claim suppose otherwise.
Then there is a multitree q∈MT(\vvπ) such that
q⩽p and qMT(\vvπ)-forces ¬φ[G]
over M, thus
qforc\vv\leavevmode¬φ.
But this contradicts to pwforc\vvπφ.
(iv)
There is a multisequence \vv\leavevmode∈\vvsMF by (iii), such that
\vvπ⊂\vv\leavevmode and pforc\vv\leavevmodeφ.
Note that still pwforc\vv\leavevmode¬φ by
Lemma 2.3.
Extend \vv\leavevmode once again, getting a contradiction
with (i).
∎
Corollary 3.3**.**
Let n≥2, \vvπ∈\vvsMF, p∈MT(\vvπ),
φ be a formula in LΣn1.
Then pforc\vvπφ and pforc\vvπφ−
cannot hold together.
Proof**.**
If n=1 then apply Lemma 3.2(i).
If n≥2 then the result immediately follows
by definition (3∘ in Section 2).
∎
Corollary 3.4** (in L).**
Assume that \vvπ∈\vvsMF, p∈MT(\vvπ),
φ is a formula in L(Σ+Π)11,
N⊨ZFL– is a TM containing \vvπ and
φ, and pwforc\vvπφ.
Then pMT(\vvπ)-forces φ[G]
over N in the usual sense.
This looks like the case \vvρ=\vvπ in
Lemma 3.1, but forc is weakened to
wforc, and φ∈M
(automatic in Lemma 3.1) is added, in the premise.
Proof**.**
Otherwise there is a multitree q∈MT(\vvπ),
q⩽p, that MT(\vvπ)-forces ¬φ[G]
over N.
On the other hand, by Lemma 3.2(iii),
there is a multisequence \vv\leavevmode∈\vvsMF such that
\vvπ⊂M(\vvπ)\vv\leavevmode
and pforc\vv\leavevmodeφ, hence, qforc\vv\leavevmodeφ by
Lemma 2.3.
However we have qforc\vv\leavevmode¬φ by
definition
(1∘a in Section 2 with ϑ=dom\vvπ),
which contradicts to Lemma 3.2(i).
∎
4 Tail invariance
If \vvπ=⟨πα⟩α<λ∈\vvsMF and
γ<λ=dom\vvπ then let the
γ-tail\vvπ↾≥γ be the restriction
\vvπ↾[γ,λ) to the ordinal semiinterval
[γ,λ)={α:\linebreak[0]γ≤α<λ}.
Then the multiforcing MT(\vvπ↾≥γ)=⋃γ≤α<λcw\vvπ(α)
is open dense in MT(\vvπ)
by Corollary 1.2(v)(a).
Therefore it can be expected that if
\vv\leavevmode is another multisequence of the same length
λ=dom\vv\leavevmode, and \vv\leavevmode↾≥γ=\vvπ↾≥γ,
then the relation
forc\vvπ coincides with forc\vv\leavevmode.
And indeed this turns out to be the case (almost).
Theorem 4.1**.**
Assume that \vvπ,\vv\leavevmode are multisequences in \vvsMF,
γ<λ=dom\vvπ=dom\vv\leavevmode,
\vv\leavevmode↾≥γ=\vvπ↾≥γ,
p∈MT, and φ is an L-formula.
Then
(i)
if φ∈L(Σ+Π)11 then
pwforc\vvπφ iff pwforc\vv\leavevmodeφ;
2. (ii)
if n≥2, \vvπ,\vv\leavevmode∈\vvsMF[\vv\nmiΠ↾↾<n−2], and
φ∈LΠn1∪LΣn+11,
then pforc\vvπφ iff
pforc\vv\leavevmodeφ.
Proof**.**
(i)
Suppose to the contrary that pwforc\vvπφ,
but pwforc\vv\leavevmodeφ fails,
so there is a multisequence \vv\leavevmode′∈\vvsMF and p′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊂\vv\leavevmode′,
p′⩽p, and p′forc\vv\leavevmode′¬φ.
Let λ′=dom\vv\leavevmode′.
By Corollary 1.2(v)(a),
there is a multitree r∈MT(\vv\leavevmode′↾≥γ), r⩽p′.
Then still r⩽p and rforc\vv\leavevmode′¬φ,
by Lemma 2.3.
Define a multisequence \vvπ′ so that
dom\vvπ′=λ′=dom\vv\leavevmode′, \vvπ⊆\vvπ′,
and \vvπ′↾≥λ=\vv\leavevmode′↾≥λ.
Then r∈MT(\vvπ′), and rwforc\vvπ′φ
by Lemma 2.3.
Consider any CTM N⊨ZFL– containing φ,
\vvπ′, \vv\leavevmode′.
Then, by Corollary 3.1, one and the same
multitree rMT(\vvπ′)-forces φ[G] but
MT(\vv\leavevmode′)-forces ¬φ[G] over N.
But this contradicts to the fact that the forcing
notions MT(\vvπ′), MT(\vv\leavevmode′) contain one and
the same dense set
MT(\vvπ′↾≥λ)=MT(\vv\leavevmode′↾≥λ).
(ii)
Consider first the LΠ21 case.
Assume that φ(x) is a LΣ11 formula,
pforc\vvπ∀xφ(x), but
to the contrary pforc\vv\leavevmode∀xφ(x) fails.
Thus there is a multisequence \vv\leavevmode′∈\vvsMF and a multitree p′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊆\vv\leavevmode′, p′⩽p, and
p′forc\vv\leavevmode′∃xφ−(x).
By definition there is a small real name c
such that p′forc\vv\leavevmode′φ−(c).
There is a multitree r∈MT(\vv\leavevmode′↾≥γ), r⩽p′.
Then still r⩽p and rforc\vv\leavevmode′φ−(c).
As above there is a multisequence \vvπ′ such that
dom\vvπ′=λ′=dom\vv\leavevmode′, \vvπ⊆\vvπ′,
and \vvπ′↾≥λ=\vv\leavevmode′↾≥λ.
Then r∈MT(\vvπ′) and rwforc\vvπ′φ−(c)
by the inductive hypothesis.
By Lemma 3.2, there is a multisequence \vvσ
such that \vvπ′⊆\vvσ and
rwforc\vvσφ−(c),
hence, rwforc\vvσ∃xφ−(x).
But this contradicts to
pforc\vvπ∀xφ(x), since r⩽p.
To carry out the step LΠn1→LΣn+11, n≥2,
let φ(x) be a formula in LΠn1.
Assume that pforc\vvπ∃xφ(x).
By definition (see 2∘ in Section 2),
there is a small real name c such that
pforc\vvπφ(c).
Then we have pforc\vv\leavevmodeφ(c)
by the inductive assumption, thus
pforc\vv\leavevmode∃xψ(x).
To carry out the step LΣn1→LΠn1, n≥3,
assume that φ is a LΠn1 formula,
pforc\vvπφ, but
to the contrary pforc\vv\leavevmodeφ fails.
Then by 3∘ of Section 2,
as \vv\leavevmode∈\vvsMF[\vv\nmiΠ↾↾<n−2], there is a multisequence \vv\leavevmode′∈\vvsMF[\vv\nmiΠ↾↾<n−2] and a multitree p′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊆\vv\leavevmode′, p′⩽p, and
p′forc\vv\leavevmode′φ−.
By Corollary 1.2(v)(a),
there is a multitree r∈MT(\vv\leavevmode′↾≥γ), r⩽p′.
Then still r⩽p and rforc\vv\leavevmode′φ−.
As above in the proof of (i),
there is a multisequence \vvπ′ such that
dom\vvπ′=λ′=dom\vv\leavevmode′, \vvπ⊆\vvπ′,
and \vvπ′↾≥λ=\vv\leavevmode′↾≥λ.
We claim that \vvπ′∈\vvsMF[\vv\nmiΠ↾↾<n−2].
Indeed if α<dom\vvπ then
\vvπ′(α)=\vvπ(α) (as \vvπ⊆\vvπ′),
hence
\vvπ′(α)↾↾<m−2=\vvπ(α)↾↾<m−2=\nmiΠα↾↾<m−2
(as \vvπ belongs to \vvsMF[\vv\nmiΠ↾↾<n−2]).
If dom\vvπ≤α<dom\vvπ′ then
\vvπ′(α)=\vv\leavevmode′(α)
(as \vvπ′↾≥λ=\vv\leavevmode′↾≥λ),
hence
\vvπ′(α)↾↾<m−2=\vv\leavevmode′(α)↾↾<m−2=\nmiΠα↾↾<m−2
(as \vv\leavevmode′ belongs to \vvsMF[\vv\nmiΠ↾↾<n−2]).
Thus \vvπ′(α)↾↾<m−2=\nmiΠα↾↾<m−2
for all α, meaning that
\vvπ′↾↾<m−2⊂\vv\nmiΠ↾↾<m−2
and \vvπ′∈\vvsMF[\vv\nmiΠ↾↾<n−2].
To conclude,
\vvπ′∈\vvsMF[\vv\nmiΠ↾↾<n−2],
\vvπ⊆\vvπ′, r∈MT(\vvπ′↾≥γ),
r⩽p, and also rforc\vvπ′φ−
by the inductive hypothesis.
But this contradicts to the assumption
pforc\vvπφ.
∎
5 Permutations
Still arguing in L,
we let PERM be the set of all
bijections h:ω1×ω⟶ontoω1×ω, such that
the kernel∣h∣={⟨ξ,k⟩:\linebreak[0]h(ξ,k)=⟨ξ,k⟩}
is at most countable.
Elements of PERM will be called permutations.
If m<ω then let PERMm consist of those
permutations h∈PERM satisfying
∣h∣⊆ω1×(ω1∖m).
In other words, if h∈PERMm and ξ<ω1, k<m,
then h(ξ,k)=⟨ξ,k⟩.
Let h∈PERM.
We extend the action of h as follows.
•
if p is a multitree then hp is
a multitree,
∣hp∣=h”p={h(ξ,k):\linebreak[0]⟨ξ,k⟩∈∣p∣},
and (hp)(h(ξ,k))=p(ξ,k)
whenever ⟨ξ,k⟩∈∣p∣,
in other words, hp coincides with the
superposition p∘(h−1);
•
if π∈MT is a multiforcing then
h⋅π=π∘(h−1) is
a multiforcing,
∣h⋅π∣=h”π
and (h⋅π)(h(ξ,k))=π(ξ,k)
whenever ⟨ξ,k⟩∈∣π∣;
•
if c⊆MT×(ω×ω) is a real name,
then put
hc={⟨hp,n,i⟩:\linebreak[0]⟨p,n,i⟩∈c},
thus easily hc is a real name as well;
•
if \vvπ=⟨πα⟩α<κ is a multisequence, then
h\vvπ=⟨h⋅πα⟩α<κ,
still a multisequence.
•
if φ:=φ(c1,…,cn) is a L-formula
(with all names explicitly indicated), then
hφ is φ(hc1,…,hcn).
Many notions and relations defined
above are clearly PERM-invariant, e. g.,
p∈MT(π) iff hp∈MT(h⋅π),
π⊏\leavevmode iff h⋅π⊏h⋅\leavevmode,
et cetera.
The invariance persists even with respect to
the relation forc, at least to some extent.
Theorem 5.1**.**
*Assume that \vvπ∈\vvsMF, p∈MT(\vvπ),
φ
is an L-formula, and h∈PERM.
Then
*
(i)
if φ belongs to L(Σ+Π)11 and
pforc\vvπφ, then
(hp)wforch\vvπ(hφ);
2. (ii)
if n≥2, h∈PERMn−2, and
φ belongs to LΠn1∪LΣn+11,
then pforc\vvπφ iff
(hp)forch\vvπ(hφ).
Proof**.**
Let \vv\leavevmode=h\vvπ, q=hp, ψ:=hφ.
(i)
Suppose to the contrary that pwforc\vvπφ,
but qwforc\vv\leavevmodeψ fails,
so that there is a multisequence \vv\leavevmode′∈\vvsMF and q′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊂\vv\leavevmode′,
q′⩽q, and q′forc\vv\leavevmode′¬ψ.
The multisequence \vvπ′=h−1\vv\leavevmode′ then satisfies
\vvπ⊂\vvπ′, and the multitree p′=h−1q′
belongs to MT(\vvπ′) and p′⩽p, hence
we have p′wforc\vvπ′φ by Lemma 2.3.
Now let M⊨ZFL– be an arbitrary CTM containing
\vvπ′,\vv\leavevmode′,φ,ψ,h↾∣h∣.
Then, by Corollary 3.4,
p′MT(\vvπ′)-forces φ[G], but
q′MT(\vv\leavevmode′)-forces ψ[G],
over M.
However the sets MT(\vvπ′), MT(\vv\leavevmode′)
belong to the same model M,
where they are order-isomorphic
via the isomorphism induced by h↾∣h∣.
Therefore, and since q=hp and ψ=hφ,
it cannot happen that both
pMT(\vvπ′)-forces φ[G] and
qMT(\vv\leavevmode′)-forces ¬ψ[G].
But this contradicts to the above.
(ii)
Consider first the LΠ21 case.
Assume that φ(x) is a LΣ11 formula,
ψ(x):=hφ(x),
pforc\vvπ∀xφ(x), but
to the contrary qforc\vv\leavevmode∀xψ(x) fails.
Thus there is a multisequence \vv\leavevmode′∈\vvsMF and a multitree q′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊂\vv\leavevmode′, q′⩽q, and
q′forc\vv\leavevmode′∃xψ−(x).
By definition there is a small real name d
such that q′forc\vv\leavevmode′ψ−(d).
The multisequence \vvπ′=h−1\vv\leavevmode′ then satisfies
\vvπ⊂\vv\leavevmode, the multitree p′=h−1q′
belongs to MT(\vvπ′) and p′⩽p,
c=h−1d
is a small real name,
and we have p′wforc\vvπ′φ−(c)
by (i).
Then by Lemma 3.2 there is a longer multisequence \vvσ∈\vvsMF satisfying \vvπ′⊂\vvσ and
p′forc\vvσφ−(c), that is, we have
p′forc\vvσ∃xφ−(x).
But by definition (3∘ in Section 2)
this contradicts to the assumption
pforc\vvπ∀xφ(x).
To carry out the step LΠn1→LΣn+11, n≥2,
let φ(x) be a formula in LΠn1,
ψ(x):=hφ(x), and h∈PERMn−2.
Assume that pforc\vvπ∃xφ(x).
By definition (see 2∘ in Section 2),
there is a small real name c such that
pforc\vvπφ(c).
Then we have qforc\vv\leavevmodeψ(d)
by inductive assumption, where
d=hc is a small real name itself.
Thus
qforc\vv\leavevmode∃xψ(x).
To carry out the step LΣn1→LΠn1, n≥3, let
φ be a formula in LΠn1, and h∈PERMn−2.
Let pforc\vvπφ,
in particular \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2],
but, to the contrary,
qforc\vv\leavevmodeψ fails,
where q=hp, \vv\leavevmode=h\vvπ,
and ψ is hφ, as above.
Then in our assumptions,
\vv\leavevmode↾↾<m−2=\vvπ↾↾<m−2, hence
\vv\leavevmode∈\vvsMF[\vv\nmiΠ↾↾<n−2] as well.
Therefore by definition
(3∘ in Section 2)
there is a multisequence \vv\leavevmode′∈\vvsMF[\vv\nmiΠ↾↾<n−2] and q′∈MT(\vv\leavevmode′)
such that \vv\leavevmode⊆\vv\leavevmode′,
q′⩽q, and q′forc\vv\leavevmode′ψ−.
Now let p′=h−1q′ and \vvπ′=h−1\vv\leavevmode′,
so that p′⩽p, \vvπ⊆\vvπ′, and,
that is most important, \vvπ′ belongs to \vvsMF[\vv\nmiΠ↾↾<n−2]
since so does \vv\leavevmode′ and h−1∈PERMn−2.
Moreover we have p′forc\vvπ′φ−
by inductive assumption.
We conclude that pforc\vvπφ fails, which is a
contradiction.
∎
6 Forcing with subsequences of the key multisequence
We argue in L.
The key multisequence \vv\nmiΠ=⟨\nmiΠα⟩α<ω1∈\vvsMFω1, satisfying
(i), (ii), (iii) of
Theorem 4.1, was fixed by
4.4, and
P=MT(\vv\nmiΠ) is our forcing notion.
If γ<ω1 then the subsequence \vv\nmiΠ↾γ
belongs to \vvsMF[\vv\nmiΠ↾↾<m], ∀m.
Definition 6.1**.**
We write
pforcαφ instead of pforc\vv\nmiΠ↾αφ,
for the sake of brevity.
Let pforcφ mean: pforcαφ for some α<ω1.
∎
Lemma 6.2** (in L).**
Assume that p∈P, α<ω1, and
pforcαφ.
Then:
(i)
if α≤β<ω1, q∈P<β=MT(\vv\nmiΠ↾β),
and q⩽p,
then qforcβφ;
2. (ii)
if q∈P, q⩽p, then qforcβφ
for some β;α≤β<ω1;
3. (iii)
if q∈P
and qforcφ− then p,q
are somewhere almost disjoint*;***
4. (iv)
therefore, 1st, if p,q∈P, q⩽p,
and pforcφ then qforcφ, and 2nd,
pforcφ, pforcφ− cannot hold together.
Proof**.**
To prove (i) apply Lemma 2.3.
To prove (ii) let β satisfy α<β<ω1
and q∈MT(\vv\nmiΠ↾β), and apply (i).
Finally to prove (iii) note that p,q
have to be incompatible in P, as otherwise
(i) leads to contradiction, but the
incompatibility in P implies being somewhere a. d. by Corollary 4.1.
∎
Now we are going to prove that the auxiliary relation
forc essentially
coincides with the usual P-forcing relation
over L.
Lemma 6.3**.**
If n<ω, φ is a closed formula as in
2.2, and p∈P, then
pP-forces φ[G] over L
in the usual sense if and only if pforcφ.
Proof**.**
Let ∥− denote the usual P-forcing relation
over L.
Part 1: φ is a formula in L(Σ+Π)11.
If pforcφ then pforc\vv\nmiΠ↾γφ
for some γ<ω1, and then p∥−φ[G]
by Lemma 3.1 with \vv\leavevmode=\vv\nmiΠ and N=L.
Suppose now that p∥−φ[G].
There is an ordinal γ0<ω1 such that
p∈Pγ0=MT(\vv\nmiΠ↾γ0) and φ
belongs to M(\vv\nmiΠ↾γ0).
The set U of all multitrees \vvπ∈\vvsMF such that
γ0<dom\vvπ and there is an ordinal ϑ,
γ0<ϑ<dom\vvπ, such that
\vvπ↾ϑ⊂M(\vvπ↾ϑ)\vvπ, is
dense in \vvπ by Corollary 1.2(ii),
and is Δ1HC.
Therefore by Corollary 4.5 there is an
ordinal γ<ω1 such that
\vvπ=\vv\nmiΠ↾γ∈U.
Let this be witnessed by an ordinal ϑ,
so that γ0<ϑ<γ=dom\vvπ and
\vvπ↾ϑ⊂M(\vvπ↾ϑ)\vvπ.
We claim that pMT(\vvπ↾ϑ)-forces
φ[G] over M(\vvπ↾ϑ) in the
usual sense — then
by definition pforc\vvπφ, and we are done.
To prove the claim, suppose otherwise.
Then there is a multitree q∈MT(\vv\nmiΠ↾ϑ),
q⩽p, which MT(\vvπ↾ϑ)-forces
¬φ[G] over M(\vvπ↾ϑ).
Then by definition we have qforc\vvπ¬φ,
hence qforc¬φ, which implies
q∥−¬φ[G] (see above),
with a contradiction to p∥−φ[G].
Part 2: the step LΠn1→LΣn+11 (n≥1).
Consider a LΠn1 formula φ(x).
Assume pforc∃xφ(x).
By definition there is a small real name c such that
pforcφ(c).
By inductive hypothesis, p∥−φ(c)[G], that is,
p∥−∃xφ(x)[G].
Conversely, assume that p∥−∃xφ(x)[G].
As P is CCC, there is a small real name c (in L)
such that p∥−φ(c)[G].
We have pforcφ(c) by the inductive hypothesis,
hence pforc∃xφ(x).
Part 3: the step LΣn1→LΠn1 (n≥2).
Consider a closed LΣn1 formula φ.
Assume that pforcφ−.
By Lemma 6.2(iv), there is no multitree q∈P, q⩽p, with qforcφ.
This implies p∥−φ− by
the inductive hypothesis.
Conversely, suppose that p∥−φ−.
There is an ordinal γ0<ω1 such that
p∈Pγ0=MT(\vv\nmiΠ↾γ0) and φ
belongs to M(\vv\nmiΠ↾γ0).
Consider the set U of all
multisequences
of the form \vvπ↾↾≥n−2, where \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2],
dom\vvπ>γ0, and
there is a multitree q∈MT(\vvπ) satisfying
q⩽p (q is stronger) and
qforc\vvπφ.
It follows from Lemma 1.2 and Lemma 2.4
that U belongs to Σn−1HC
(with φ and p0 as parameters).
Therefore by 4.4(ii)
there is an ordinal γ<ω1 such that
the subsequence \vv\nmiΠ↾γ(n−2)-decides U.
Case 1: (\vv\nmiΠ↾γ)↾↾≥n−2∈U.
Let this be witnessed by a multisequence \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2]
and a multitree q∈MT(\vvπ), so that in particular
(\vv\nmiΠ↾γ)↾↾≥n−2=\vvπ↾↾≥n−2 and
dom\vvπ=γ>γ0.
Then by definition (Definition 1.1)
we also have \vvπ↾↾<n−2=(\vv\nmiΠ↾γ)↾↾<n−2,
so that overall \vvπ=\vv\nmiΠ↾γ.
Thus q∈MT(\vv\nmiΠ↾γ), q⩽p, and
qforc\vv\nmiΠ↾γφ, that is,
q∥−φ[G] by the inductive hypothesis,
contrary to the choice of p.
Therefore Case 1 cannot happen, and we have:
Case 2: negative decision,
no multisequence in U extends (\vv\nmiΠ↾γ)↾↾≥n−2.
We can assume that γ>γ0.
(Otherwise replace γ by γ0+1.)
We claim that pforcγφ−.
Indeed otherwise by 3∘
there is a multisequence \vvπ∈\vvsMF[\vv\nmiΠ↾↾<n−2]
and a multitree q∈MT(\vvπ), such that
\vv\nmiΠ↾γ⊆\vvπ,
q⩽p, and qforc\vv\leavevmodeφ.
But then \vvπ and q witness that
\vvσ=\vvπ↾↾≥n−2 belongs to U.
On the other hand, \vvσ obviously
extends \vv\nmiΠ↾γ↾↾≥n−2, since
\vv\nmiΠ↾γ⊆\vvπ,
contrary to the Case 2 assumption.
Thus indeed pforcφ−, as required.
∎
The next lemma provides a useful strengthening.
Lemma 6.4**.**
If Φ is a Δ1HC collection of
closed Πn+21 formulas, p0∈P,
and p0P-forces φ[G]
over L for each φ∈Φ,
then there is an ordinal γ<ω1
such that if φ∈Φ then
p0forc\vv\nmiΠ↾γφ.
(Same γ for all φ.)
Proof**.**
Let U consist of all multisequences of the form \vvπ↾↾≥m,
where \vvπ∈\vvsMF[\vv\nmiΠ↾↾<m],
and there is a formula φ∈Φ
and p∈MT(\vvπ) such that p⩽p0 and
pforc\vvπφ−.
It follows from Lemma 1.2 and 2.4
that U is a Σm+1HC set, so by
4.4(ii)
there is an ordinal γ<ω1 such that
\vv\nmiΠ↾γm-decides U.
Case 1: (\vv\nmiΠ↾γ)↾↾≥m∈U,
that is, the multisequence \vvπ=\vv\nmiΠ↾γ satisfies the
condition that there exist φ∈Φ
and a multitree p∈\vvπ such that p⩽p0 and
pforc\vvπφ−,
and hence pP-forces
φ−[G] over L by Lemma 6.3,
contrary to the choice of p0.
Therefore Case 1 cannot happen, and we have
Case 2: no multisequence in
U extends (\vv\nmiΠ↾γ)↾↾≥m.
We can assume that γ>γ0.
(Otherwise replace γ by γ0+1.)
We claim that γ is as required.
Indeed otherwise
p0forc\vv\nmiΠ↾γφfails for a formula φ∈Φ,
thus (3∘ in Section 2),
there is a multisequence \vvπ∈\vvsMF[\vv\nmiΠ↾↾<m] and p∈MT(\vvπ)
such that \vv\nmiΠ↾γ⊆\vvπ,
p⩽p0,
and pforc\vvπφ−.
It follows that \vvπ↾↾≥m∈U.
In addition, \vvπ↾↾≥m extends
(\vv\nmiΠ↾γ)↾↾≥m
by construction.
But this contradicts to the Case 2 assumption.
∎
VI The model
In this conclusive section we gather the results
obtained above towards the proof of Theorem 1.1.
We begin with the analysis of definability of key
generic reals in P-generic extensions
of L, which will lead to (I) and (II)
of Theorem 1.1.
Then we proceed to (III) (elementary equivalence)
and (IV) (the non-wellorderability).
1 Key generic extension and subextensions
Recall that the key multisequence \vv\nmiΠ=⟨\nmiΠα⟩α<ω1
of small multiforcings \nmiΠα is defined in L by 4.4,
\nmiΠ=⋃α<ω1cw is a multiforcing, ∣\nmiΠ∣=ω1×ω
in L, and P=MT(\vv\nmiΠ)=MT(\nmiΠ)∈L is our key
forcing notion, equal to the finite-support product
∏ξ<ω1,k<ω\nmiΠ(ξ,k) of perfect-tree
forcings \nmiΠ(ξ,k) in L.
See Section 5, where some properties of P are
established, including CCC and definability of the
factors \nmiΠ(ξ,k).
From now on, we’ll typically
argue in L and in P-generic extensions
of L, so by Lemma 5.6 it will always be true that
ω1L=ω1.
This allows us to still think that ∣\nmiΠ∣=ω1×ω
(rather than ω1L×ω).
Recall that \nmiΠ∈L and P=MT(\nmiΠ) is a forcing
notion in L.
Definition 1.1**.**
Let a set G⊆P be generic over the
constructible set universe L.
If ⟨ξ,k⟩∈ω1×ω
then following Remark 4.3, we
let xξk=xξk[G]∈2ω be the only real in
⋂T∈G(ξ,k)[T].
Thus P adds an array
X=⟨xξk⟩⟨ξ,k⟩∈ω1×ω of reals,
where each real
xξk=xξk[G]∈∈2ω∩L[G]
is a \nmiΠ(ξ,k)-generic real over L,
and L[G]=L[X].
∎
Let G⊆P be a set (filter) P-generic over L.
If m<ω then following the notation in
Section 2 we define
[TABLE]
so that the set G↾↾<m is P↾↾<m-generic
over L, where accordingly
[TABLE]
Each subextension L[G↾↾<m]⊆L[G] coincides
with L[⟨xξk[G]⟩ξ<ω1∧k<m].
Our goal will be to demonstrate that the model
L[X]=L[G], along with the system of submodels
L[⟨xξk[G]⟩ξ<ω1∧k<m],
proves Theorem 1.1.
2 Definability of generic reals
Recall that the factors \nmiΠ(ξ,k) of the forcing
notion \nmiΠ are defined by
\nmiΠ(ξ,k)=⋃α(ξ,k)≤α<ω1\nmiΠα(ξ,k),
where α(ξ,k)<ω1, the sets \nmiΠα(ξ,k) are
countable sets of perfect trees, whose definability in
L is determined by Corollary 5.3.
Theorem 2.1**.**
Assume that a set G⊆P is
P-generic over L,
ξ<ω1, k<ω, and x∈L[G]∩ωω.
The following are equivalent:
(1)
x=xξk[G];**
2. (2)
x* is \nmiΠ(ξ,k)-generic over L;*
3. (3)
x∈⋂α(ξ,k)≤α<ω1⋃T∈\nmiΠα(ξ,k)[T].
Proof**.**
\refxik1⟹\refxik2 is a routine (see Remark 4.3).
To check \refxik2⟹\refxik3 recall that each set
\nmiΠα(ξ,k) is pre-dense in \nmiΠ(ξ,k) by
Lemma 1.2(v).
It remains to establish \refxik3⟹\refxik1.
Suppose towards the contrary that a real x∈L[G]∩2ω
satisfies (3) but x=xξk[G].
By Theorem 6.2(i) there is a
true \nmiΠ-real name c=⟨Cni⟩n,i<ω,
non-principal over \nmiΠ at ξ,k
and such that x=c[G].
Being non-principal means that the next set
is open dense in P=MT(\nmiΠ):
[TABLE]
And as P=MT(\nmiΠ) is a CCC forcing by Lemma 5.6,
we can assume that the name c is small,
that is, each set Cni⊆P is countable.
Then there is an ordinal γ0<ω1 such that
Cni⊆P<γ0 for all n,i.
Then c is a true
\nmiΠ<γ0-real name.
Moreover we can assume by Corollary 5.7
that Dξk\nmiΠ(c)∩P<γ0 is
pre-dense in P.
Now consider the set W of all multisequences
\vvπ=⟨πα⟩α<dom(\vvπ)∈\vvsMF
such that dom(\vvπ)>γ0 and
−
either (I) \vv\nmiΠ↾γ0⊂\vvπ;
−
or (II) \vv\nmiΠ↾γ0⊂\vvπ and c
is not non-principal over
π=⋃cw\vvπ at ξ,k;
−
or (III) \vv\nmiΠ↾γ0⊂\vvπ,
dom(\vvπ)=δ+1 is
a successor, and
⋃α<δcwπα⊏ξkcπδ.
We assert that W is dense in \vvsMF:
any multisequence \vvπ∈\vvsMF can be extended to some
\vv\leavevmode∈W.
Indeed first extend \vvπ by Corollary 1.2
so that is has a length
dom(\vvπ)=δ>γ0.
If now \vv\nmiΠ↾γ0⊂\vvπ then immediately
\vvπ∈W via (I), so we assume that
\vv\nmiΠ↾γ0⊂\vvπ.
We can also assume that c
is non-principal over π=⋃cw\vvπ at ξ,k
by similar reasons related to (II).
The multisequence \vvπ can
be extended, by Corollary 1.2, by an extra term
πδ, so that the extended multisequence \vvπ+
satisfies \vvπ⊂{c}\vvπ+, that is,
π⊏⊏{c}πδ.
By definition (Definition 7.1) and the
nonprincipality of c, we get
π⊏ξkcπδ.
It follows that \vvπ+∈W via (III).
Since W is Σ1HC, by Definition 4.4(ii)
there is an ordinal γ<ω1 such that the multisequence \vv\nmiΠ↾γ0-decides W.
However the negative decision is impossible by the
density (see the proof of Lemma 5.2).
We conclude that \vv\nmiΠ↾γ∈W; hence, γ>γ0.
Option (I) for \vvπ=\vv\nmiΠ↾γ clearly fails, and
(II) fails either because the set
Dξk\nmiΠ(c)∩P<γ0 is
pre-dense in P and γ>γ0.
Therefore \vv\nmiΠ↾γ belongs to W via (III),
that is, γ=δ+1 and
\nmiΠ<δ=⋃α<δcw\nmiΠα⊏ξkc\nmiΠδ.
Then
\nmiΠ<δ⊏ξkc\nmiΠ≥δ=⋃δ≤α<ω1cw\nmiΠδ
by Lemma 4.3(iii).
Now we make use of Theorem 6.2(ii) with
π=\nmiΠ<δ and \leavevmode=\nmiΠ≥δ; note that
π∪cw\leavevmode=\nmiΠ.
It follows that
x=c[G]∈/⋃Q∈\nmiΠ≥δ(ξ,k)[Q],
which clearly contradicts to the assumption (3).
∎
Corollary 2.2**.**
Assume that k<ω and G⊆P is P-generic
over L.
Then
[TABLE]
is a set of definability class Πk+2HC in L[G]
and in any transitive model M⊨ZFC satisfying
L⊆M⊆L[G] and {xξk[G]:\linebreak[0]ξ<ω1}⊆M.
Proof**.**
By the theorem, it is true in L[G]
that ⟨ξ,x⟩∈Wk iff
[TABLE]
which can be re-written as
[TABLE]
Here the equality μ=α(ξ,k) (with a fixed k)
is Δk+2HC by Corollary 5.3, and so is
the equality X=\nmiΠα(ξ,k) by
Corollary 5.3.
It follows that the whole relation is Πk+2HC,
since the quantifier ∃T∈X is bounded.
∎
The next corollary is the first cornerstone in the proof
of Theorem 1.1.
Assume that m<ω and a set G⊆P is
P-generic over L.
Then ωω∩L[G↾↾<m] is a Σm+31
set in L[G],
and it holds in L[G↾↾<m] that there is
a Δm+31 wellordering of ωω of length ω1.
Proof**.**
If γ<ω1 then let
Xγn=⟨xξk[G]⟩ξ<γ∧k<n;
thus X=Xγn is a Πn+1HC relation
in L[G] (with γ,n,X as arguments)
by Corollary 2.2.
It follows that
[TABLE]
is a set in Σn+2HC, hence, a Σm+31
set in L[G].
To define a required wellordering, if
x∈ωω∩L[G↾↾<m] then let γ(x) be
the least γ<ω1 such that x∈L[Xγn],
and let ν(x)<ω1 be the index of x in the
canonical wellordering of ωω in L[Xγn].
Now we wellorder ωω∩L[G↾↾<m] according to
the lexicographical ordering of triples
⟨max{γ(x),ν(x)},γ(x),ν(x)⟩.
∎
3 Elementary equivalence
Here we prove the following elementary equivalence
theorem for key generic extensions.
Compare to (III) of Theorem 1.1.
Theorem 3.1**.**
Assume that m<ω and a set G⊆P is
P-generic over L.
Then L[G↾↾<m] is an elementary submodel of
L[G] w. r. t. all Σm+21 formulas.
Proof**.**
Suppose that this is not the case.
Then there is a Πm+11 formula φ(r,x) with
r∈ωω∩L[G↾↾<m] as the only parameter,
and a real x0∈ωω∩L[G]
such that φ(r,x0) is true in L[G]
but there is no x∈ωω∩L[G↾↾<m]
such that φ(r,x) is true in L[G].
By a version of Proposition 6.1(ii),
we have r=c0[G], where c0 is a small
true (P↾↾<m)-real name.
(See Section 1 on notation.)
And there is a small true P-real name c such that
x0=c[G].
By Lemma 6.3, there is a multitree p0∈G
such that
(1)
p0P-forces
φ(c0[G],c[G])∧¬∃x∈L[G↾↾<m]φ(c0[G],x)
over L;
2. (2)
p0forcφ(c0,c), that is,
p0forc\vv\nmiΠ↾γ0φ(c0,c),
where γ0<ω1 —
and we can assume that p0∈MT(\vv\nmiΠ↾γ0)
as well.
As c,c0 are small names, there is an
ordinal δ<ω1 satisfying
(3)
∣c0∣⊆δ×m, ∣c∣⊆δ×ω,
and ∣p0∣⊆δ×ω,
and we can enlarge γ0, if necessary,
using the equality ∣\vv\nmiΠ∣=ω1×ω
of Lemma 5.2,
to make sure that
(4)
δ×ω⊆∣\vv\nmiΠ↾γ0∣,
that is, if η<δ and k<ω then
⟨η,k⟩∈∣\nmiΠα′∣ for some
α′=α′(η,k)<γ0.
We are starting from here towards a contradiction.
Let U consist of all multisequences of the form \vvπ↾↾≥m,
where
(A)
\vvπ∈\vvsMF[\vv\nmiΠ↾↾<m],
\vv\nmiΠ↾γ0⊂\vvπ,
and hence p0∈MT(\vvπ) by (2);
and
there is an ordinal ζ<ω1 and
a transformation h∈PERMm−1 such that
(B)
h=h−1, ∣h∣=D∪R,
and h maps D onto R and R onto D,
where D=δ×[m,ω),
R={⟨ξ,m−1⟩:\linebreak[0]ν0≤ξ<ν1}, and
δ<ν0<ν1<ω1;
2. (C)
γ0≤ζ<dom\vvπ and
(h\vvπ)↾≥ζ=\vvπ↾≥ζ,
or equivalently h(\vvπ(α))=\vvπ(α) whenever
ζ≤α<dom\vvπ.
It follows from Lemma 1.2 that U is
a Σm+1HC set
(with \vv\nmiΠ↾γ0, δ as parameters).
Therefore by 4.4(ii)
there is an ordinal γ<ω1 such that
\vv\nmiΠ↾γm-decides U.
Case 1: (\vv\nmiΠ↾γ)↾↾≥m∈U.
Basically this means that there is a transformation
h∈PERMm−1 such that
(A), (B),
(C)
hold for h and \vvπ=\vv\nmiΠ↾γ, via
ordinals δ<ν0<ν1 and γ0<ζ<γ as in
(B),
(C).
Now, by Lemma 2.3 and (2), we have
p0forc\vv\nmiΠ↾γφ(c0,c).
We further get
hp0forch\vv\nmiΠ↾γφ(hc0,hc)
by Theorem 5.1
because φ is a LΠn+11
formula and h belongs to PERMm−1.
However hc0=c0 since ∣c0∣∩∣h∣=∅
by (B).
Thus
p0′forc\vv\nmiΠ↾γφ(c0,c′)
holds by Theorem 4.1 and (C),
where c′=hc, p0′=hp0.
Note that the common part ∣p0∣∩∣p0′∣
of the domains of p0,p0′ does not intersect
∣h∣ by (B) since ∣p0∣⊆δ×ω
by (3).
It follows that p0,p0′ are compatible, basically
p=p0∪p0′ is a multitree in MT(\vv\nmiΠ↾γ).
Thus p⩽p0′ and still
pforc\vv\nmiΠ↾γφ(c0,c′).
It follows by Lemma 6.3 that
(5)
pP-forces
φ(c0[G],c′[G])
over L.
However ∣c′∣⊆ω1×m by construction
because ∣c∣⊆δ×ω by (3),
and hence c′[G]∈L[G↾↾<m] is forced.
Thus pP-forces
∃x∈L[G↾↾<m]φ(c0[G],x)
over L by (5), contrary to (1).
The contradiction ends Case 1.
Case 2: negative decision, no multisequence in
U extends (\vv\nmiΠ↾γ)↾↾≥m.
We can assume that γ>γ0.
(Otherwise replace γ by γ0+1.)
Let ν0 be the lest ordinal, bigger than δ
and satisfying ∣\vv\nmiΠ↾γ∣⊆ν0×ω.
Let ν1=ν0+ω.
Then countable sets D=δ×[m,∞) and R
as in (B) are
defined and D∩R=∅, so we can fix a
transformation h∈PERMm−1 satisfying (B).
Note that D⊆δ×ω⊆∣\vv\nmiΠ↾γ∣ by
(4) but R∩∣\vv\nmiΠ↾γ∣=∅ by
the choice of ν0.
Pick λ<ω1 such that λ>γ>γ0.
Then the multisequence \vv\leavevmode=\vv\nmiΠ↾λ clearly satisfies
(A), (B)
and extends \vv\nmiΠ↾γ.
Our plan is now to slightly modify \vv\leavevmode
in order to fulfill (C) as well, with ζ=γ.
Such a minor modification consists in the replacement
of the R-part of \vv\leavevmode above γ
by the h-copy of its D-part.
To present this in detail, recall that
\vv\leavevmode=\vv\nmiΠ↾λ=⟨\nmiΠα⟩α<λ, where
each \nmiΠα is a small multiforcing, whose domain
dα=∣\nmiΠα∣⊆ω1×ω is countable.
If α<γ then put πα=\nmiΠα.
Suppose that γ≤α<λ.
Then D⊆∣\nmiΠα∣ by (4).
Define a modified multiforcing πα such that
(a)
∣πα∣=dα∪R — note that
D⊆dα⊆∣πα∣ in this case because
D⊆∣\vv\nmiΠ↾γ∣ by (4)
(as γ0≤γ), and hence
D⊆dα=∣\nmiΠα∣ (as α≥γ),
2. (b)
if ⟨ξ,k⟩∈dα∖R then
πα(ξ,k)=\nmiΠα(ξ,k),
3. (c)
if ⟨ξ,k⟩∈D, so
h(ξ,k)=⟨η,m−1⟩∈R, then
πα(η,m−1)=\nmiΠα(ξ,k).
We claim that \vvπ=⟨πα⟩α<λ is a
multisequence, that is, if α<β<λ then
πα⊏πβ.
This amounts to the folowing: if
⟨η,k⟩∈∣πα∣ then
πα(η,k)⊏πβ(η,k).
Note that πα(η,k)=\nmiΠα(η,k) in case
⟨η,k⟩∈/R.
Thus it remains to check that
πα(η,m−1)⊏πβ(η,m−1) whenever
α<β<λ,
⟨η,m−1⟩=h(ξ,k)∈R∩∣πα∣, and
⟨ξ,k⟩∈D.
If now α<γ then R∩∣πα∣=∅
by the choice of ν0, so it remains to consider
the case when γ≤α.
Then the pairs ⟨ξ,k⟩, ⟨η,m−1⟩ belong to
∣πα∣ by construction, and we have
πα(η,m−1)=\nmiΠα(ξ,k) and
πβ(η,m−1)=\nmiΠβ(ξ,k).
Therefore πα(ξ,m)⊏πβ(ξ,m)
since \vv\nmiΠ is a multisequence, and we are done.
Now we claim that the multisequence \vvπ=⟨πα⟩α<λ
satisfies (A), (B),
(C).
Indeed as the difference between each
πα and the corresponding \nmiΠα
is fully located in the domain
R={⟨ξ,m−1⟩:\linebreak[0]ν0≤ξ<ν1},
we have \vvπ↾↾<m−1=\vv\leavevmode↾↾<m−1,
therefore \vvπ∈\vvsMF[\vv\nmiΠ↾↾<m].
We also note that \vvπ↾γ=\vv\leavevmode↾γ by
construction, hence \vv\nmiΠ↾γ=\vv\leavevmode↾γ⊂\vvπ.
This implies (A).
We also have (B)
by construction.
We finally claim that (C) is satisfied with
ζ=γ, that is, if γ≤α<λ then
h⋅πα=πα.
Indeed we have D∪R⊆∣πα∣, see
(a).
Now the invariance of πα under h holds
by (b), (c).
It follows that \vvπ↾↾≥m∈U.
In addition, \vvπ↾↾≥m extends
(\vv\nmiΠ↾γ)↾↾≥m, since
\vv\nmiΠ↾γ⊂\vvπ.
But this contradicts the Case 2 assumption.
To conclude, either case leads to a contradiction,
proving the theorem.
∎
4 Non-wellorderability
We finally prove that the reals are not wellorderable by
a (lightface) analytically definable relation in
P-generic extensions, that is, (IV) of
Theorem 1.1.
Theorem 4.1**.**
Assume that m<ω and a set G⊆P is
P-generic over L.
Then it is true in L[G] that the reals
are not wellorderable by an analytically definable
relation.
Proof**.**
Suppose to the contrary that, in L[G], a Σm+21
relation ≪ strictly wellorders ωω, m≥1.
Let ψ(x,y) be a parameter-free Σm+21 formula,
which defines ≪, so that x≪y iff ψ(x,y)
in L[G].
Note that ≪ is essentially a Δm+21 relation,
since x≪y⟺y≪x∧x=y.
Of all nonconstructible reals xξm[G], ξ<ω1,
there is a ≪-least one.
We suppose that x0m[G] is such.
(If it is some xξ0m[G], ξ0=0,
then the arguments suitably change in obvious way.)
That is, x0m[G]≪xξm[G]
whenever ξ>0.
Accordingly there is a multitree p0∈G that
P-forces, over L, that
(1)
≪ (that is, the relation defined by ψ)
is a wellordering of ωω, and
(2)
∀ξ>0(x0m[G]≪xξm[G]).
Therefore, if ξ>0 then p0P-forces
{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m}[{\underline{G}}]\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m}[{\underline{G}}])
over L.
(We make use of the real names {\overset{\text{\hskip 2.15277pt{}_{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi k} introduced
by 1.6, 1.7.)
By Lemma 6.3, we can assume that
p0forc(1)∧(2), so that in fact we have
p0forc\vv\nmiΠ↾γ0(1)∧(2),
for some γ0<ω1.
Then p0∈MT(\vv\nmiΠ↾γ0)=MT(\nmiΠ<γ0),
where \nmiΠ<γ0=⋃ξ<γ0cw\nmiΠξ is
a small multiforcing.
Let δ<ω1 be the least ordinal satisfying
∣\nmiΠ<γ0∣⊆δ×ω.
It follows then that ∣p0∣⊆δ×ω.
By Lemma 6.4, there is an ordinal
γ1, γ0<γ1<ω1, such that
if ξ<ω1 then
{\boldsymbol{p}}_{0}\mathop{\hskip 1.72218pt{\tt forc}_{\vv{\nmi\Pi}{\hskip 0.60275pt{\restriction}\hskip 0.60275pt}\gamma_{1}}\hskip 1.72218pt}({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m})^{-}.
We can enlarge γ1, if necessary, using Lemma 5.2,
to make sure that ⟨0,m⟩∈∣\vv\nmiΠ↾γ1∣,
that is, ⟨0,m⟩∈∣\nmiΠα′∣ for some
α′<γ1.
If ξ<ω1 then let hξ∈PERMm be the
permutation of ⟨0,m⟩ and ⟨ξ,m⟩, such that
∣hξ∣={⟨0,m⟩,⟨ξ,m⟩},
hξ(0,m)=⟨ξ,m⟩,
hξ(ξ,m)=⟨0,m⟩,
hξ(η,n)=⟨η,n⟩ for any pair ⟨η,n⟩
different from both ⟨0,m⟩ and ⟨ξ,m⟩.
The remainder of the proof is very similar to the proof
of Theorem 3.1.
Let U consist of all multisequences of the form \vvπ↾↾≥m,
where
(A)
\vvπ∈\vvsMF[\vv\nmiΠ↾↾<m],
\vv\nmiΠ↾γ1⊂\vvπ,
and hence p0∈MT(\vvπ) by (2);
and there exist ordinals ξ,ζ<ω1 such that
(B)
δ<ξ<dom\vvπ;
2. (C)
γ1≤ζ<dom\vvπ and
(hξ\vvπ)↾≥ζ=\vvπ↾≥ζ,
or equivalently hξ⋅(\vvπ(α))=\vvπ(α) whenever
ζ≤α<dom\vvπ.
It follows from Lemma 1.2 that U is
a Σm+1HC set
(with \vv\nmiΠ↾γ1 as a parameter).
Therefore by 4.4(ii)
there is an ordinal γ<ω1 such that
\vv\nmiΠ↾γm-decides U.
Case 1: (\vv\nmiΠ↾γ)↾↾≥m∈U.
Basically this means that γ>γ1
and there are ordinals ξ<ω1 and ζ<γ
such that (A), (B), (C)
hold for ξ and the multisequence \vvπ=\vv\nmiΠ↾γ.
By Lemma 2.3 and the choice of γ1,
{\boldsymbol{p}}_{0}\mathop{\hskip 1.72218pt{\tt forc}_{\vv{\nmi\Pi}{\hskip 0.60275pt{\restriction}\hskip 0.60275pt}\gamma}\hskip 1.72218pt}({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m})^{-}
holds.
This implies
\boldsymbol{h}_{\xi}{\boldsymbol{p}}_{0}\mathop{\hskip 1.72218pt{\tt forc}_{\boldsymbol{h}_{\xi}\vv{\nmi\Pi}{\hskip 0.60275pt{\restriction}\hskip 0.60275pt}\gamma}\hskip 1.72218pt}({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m})^{-}
by Theorem 5.1 because
({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m})^{-} is a LΠm+21
formula and hξ belongs to PERMm.
We conclude that
{\boldsymbol{p}}_{0}^{\prime}\mathop{\hskip 1.72218pt{\tt forc}_{\vv{\nmi\Pi}{\hskip 0.60275pt{\restriction}\hskip 0.60275pt}\gamma}\hskip 1.72218pt}({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m})^{-}
by (C) and Theorem 4.1,
where p0′=hξp0.
Note that ⟨ξ,m⟩∈/∣p0∣ by (B).
It follows by the definition of hξ
that p0,p0′ are compatible, basically
p=p0∪p0′ is a multitree in MT(\vv\nmiΠ↾γ)
and p⩽p0, p⩽p0′.
Thus both
{\boldsymbol{p}}\mathop{\hskip 1.72218pt{\tt forc}_{\vv{\nmi\Pi}{\hskip 0.60275pt{\restriction}\hskip 0.60275pt}\gamma}\hskip 1.72218pt}({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m})^{-} and
{\boldsymbol{p}}\mathop{\hskip 1.72218pt{\tt forc}_{\vv{\nmi\Pi}{\hskip 0.60275pt{\restriction}\hskip 0.60275pt}\gamma}\hskip 1.72218pt}({\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{\xi m}\ll{\overset{\text{\hskip 2.15277pt{}{\text{\Large\bf.}}}}{\boldsymbol{x}}}_{0m})^{-}
hold,
contrary to Lemma 6.2(iv).
The contradiction ends Case 1.
Case 2: negative decision, no multisequence in
U extends (\vv\nmiΠ↾γ)↾↾≥m.
We can assume that γ>γ1
(otherwise replace γ by γ1+1).
Note that
\vv\nmiΠ↾γ=⟨\nmiΠα⟩α<γ, where
each \nmiΠα is a small multiforcing, whose domain
dα=∣\nmiΠα∣⊆ω1×ω is countable.
Therefore the set
d=∣\vv\nmiΠ↾γ∣=⋃α<γdα is
still countable.
Pick an ordinal ξ, δ<ξ<ω1,
such that ⟨ξ,m⟩∈/d.
Finally pick an ordinal λ, γ<λ<ω1.
Then \vv\leavevmode=\vv\nmiΠ↾λ (as \vvπ) and ξ
clearly satisfy (A) and (B),
and \vv\leavevmode extends \vv\nmiΠ↾γ.
Let’s somewhat modify \vv\leavevmode
in order to fulfill (C) as well.
As above,
\vv\leavevmode=\vv\nmiΠ↾λ=⟨\nmiΠα⟩α<λ,
each \nmiΠα is a small multiforcing, and its domain
dα=∣\nmiΠα∣⊆ω1×ω is countable.
If α<γ then put πα=\nmiΠα.
Suppose that γ≤α<λ.
Then α≥γ1, and hence
⟨0,m⟩∈∣\nmiΠα∣ by the choice of γ1.
Define a modified multiforcing πα such that
∣πα∣=dα∪{⟨ξ,m⟩},
if ⟨η,k⟩∈dα∖{⟨ξ,m⟩}
then πα(η,k)=\nmiΠα(η,k), and finally
πα(ξ,m)=\nmiΠα(0,m).
We claim that \vvπ=⟨πα⟩α<λ is a
multisequence, that is, if α<β<λ then
πα⊏πβ.
This amounts to the folowing: if
⟨η,k⟩∈∣πα∣ then
πα(η,k)⊏πβ(η,k).
Note that πα(η,k)=\nmiΠα(η,k) whenever
⟨η,k⟩=⟨ξ,m⟩.
Thus it remains to check that
πα(ξ,m)⊏πβ(ξ,m) given
α<β<λ such that ⟨ξ,m⟩∈∣πα∣.
If α<γ then ∣πα∣=∣\nmiΠα∣=dα
by construction, and hence ⟨ξ,m⟩∈/dα by
the choice of ξ.
It remains to consider the case γ≤α<λ.
Then ⟨0,m⟩∈dα (see above), hence the
pairs ⟨0,m⟩, ⟨ξ,m⟩ belong to
∣πα∣ by construction,
and then obviously belong to ∣πβ∣ as α<β.
Now πα(ξ,m)=\nmiΠα(0,m) and
πβ(ξ,m)=\nmiΠβ(0,m), and we have
πα(ξ,m)⊏πβ(ξ,m) since \vv\nmiΠ
is a multisequence.
Now we claim that the multisequence \vvπ=⟨πα⟩α<λ
satisfies (A), (B), (C) with ζ=γ.
If α<λ then the difference between
\nmiΠα and πα
is located in the one-element domain
{⟨ξ,m⟩}, therefore
πα↾↾<m=\nmiΠα↾↾<m.
It follows that
\vvπ↾↾<m=(\vv\nmiΠ↾λ)↾↾<m, hence
\vvπ∈\vvsMF[\vv\nmiΠ↾↾<m].
We further have
\vvπ↾γ=\vv\nmiΠ↾γ by construction.
Thus \vv\nmiΠ↾γ⊂\vvπ, hence
\vv\nmiΠ↾γ1⊂\vvπ, and we have (A).
We also have (B) and (C)
(with ζ=γ) by construction.
Thus \vvπ↾↾≥m∈U.
In addition, \vvπ↾↾≥m extends
(\vv\nmiΠ↾γ)↾↾≥m, since even more
\vv\nmiΠ↾γ⊂\vvπ by construction.
But this contradicts to the Case 2 assumption.
To conclude, either case leads to a contradiction,
proving the theorem.
∎
We consider a P-generic extension L[G] of
L and present it in the form L[G]=L[X]
as in Section 1, where
X=⟨xξk⟩⟨ξ,k⟩∈ω1×ω, and each
xξk=xξk[G] is a real in 2ω∩L[G].
We also consider the subextensions
L[G↾↾<m]=L[⟨xξk⟩ξ<ω1∧k<m]
of L[G]=L[X].
Then (I) and (II) of Theorem 1.1 hold by
Corollary 2.3,
(III) holds by Theorem 3.1, and finally
(IV) holds by Theorem 4.1.
∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1[1] Uri Abraham. A minimal model for ¬ C H : : 𝐶 𝐻 absent \neg\>CH: iteration of Jensen’s reals. Trans. Am. Math. Soc. , 281:657–674, 1984.
2[2] Uri Abraham. Minimal model of “ ℵ 1 L subscript superscript ℵ 𝐿 1 \aleph^{L}_{1} is countable” and definable reals. Adv. Math. , 55:75–89, 1985.
3[3] Joan Bagaria and Vladimir Kanovei. On coding uncountable sets by reals. Math. Log. Q. , 56(4):409–424, 2010.
4[4] Ali Enayat. On the Leibniz-Mycielski axiom in set theory. Fundam. Math. , 181(3):215–231, 2004.
5[5] J. Hadamard, R. Baire, H. Lebesgue, and E. Borel. Cinq lettres sur la théorie des ensembles. Bull. Soc. Math. Fr. , 33:261–273, 1905.
6[6] Leo Harrington. The constructible reals can be anything. Preprint dated May 1974 with several addenda dated up to October 1975: (A) Models where Separation principles fail, May 74; (B) Separation without Reduction, April 75; (C) The constructible reals can be (almost) anything, Part II, May 75.
7[7] Kai Hauser and Ralf-Dieter Schindler. Projective uniformization revisited. Ann. Pure Appl. Logic , 103(1-3):109–153, 2000.
8[8] Thomas Jech. Set theory. Springer-Verlag, Berlin-Heidelberg-New York, The third millennium revised and expanded edition, 2003.