Definable E0 classes at arbitrary projective levels
Vladimir Kanovei
IITP RAS and MIIT,
[email protected] —
contact author.
Partial support of grant RFBR 17-01-00705 acknowledged.
Vassily Lyubetsky
IITP RAS,
[email protected].
Partial support of grant RSF 14-50-00150 acknowledged.
Abstract
Using a modification of the invariant Jensen forcing
of [10],
we define a model of ZFC, in which, for a given n≥3,
there exists a lightface
Πn1-set of reals,
which is a E0-equivalence class, hence a
countable set, and which does
not contain any OD element, while
every non-empty countable Σn1-set of reals
is necessarily constructible, hence contains only
OD reals.
Contents
- 1 Introduction
- 2 Connections to the Vitali equivalence relation
- 3 Structure of the proof
- 4 Silver trees
- 5 Splitting Silver trees
- 6 ST-forcings
- 7 Continuous maps
- 8 Generic extensions of ST-forcings
- 9 Construction of extending ST-forcing
- 10 Validation of the extension property
- 11 The blocking sequence of ST-forcings
- 12 CCC and some other forcing properties
- 13 Generic model
- 14 Definability of the set of generic reals
- 15 Auxiliary forcing relation
- 16 Invariance
- 17 The final argument
- Index
1 Introduction
Problems related to definability of mathematical objects,
were one of focal points of the famous discussion on
mathematical foundations in the beginning of XIX C.
In particular, Baire, Borel, Hadamard, and Lebesgue,
participants of the exchange of letters published in
[4], in spite of essential disagreement between
them on questions related to mathematical foundations,
generally agreed that the proof of existence of
an element in a given set, and a direct definition
(or effective construction) of such an element
— are different mathematical results, of which
the second does not follow from the first.
In particular, Lebesgue in his contribution to
[4] pointed out the difficulties in the problem
of effective choice, that is, choice of definable element
in a definable non-empty set. 111 Ainsi je vois déjà une difficulté dans ceci
“dans un M′ déterminé
je puis choisir un m′ déterminé”, in the French
original.
Thus I already see a difficulty with the assertion that
“in a determinate M′ I can choose a determinate m′”,
in the translation.
Studies in modern set theory demonstrated that effective
effective choice is not always possible.
In particular, it is true in many well-known models
(including the very first Cohen models),
that the set X=R∖L of all
Goedel-nonconstructible reals is not empty, but
contains no definable elements.
One may note that if the set X is non-empty then it
has to be rather large, that is, surely of cardinality
c, if measurable then of full measure, etc..
Is there such an example among small, e. g. countable sets?
This problem was discussed at
Mathoverflow 222
A question about ordinal definable real numbers.
Mathoverflow, March 09, 2010.
http://mathoverflow.net/questions/17608.
and
Foundations of mathematics (FOM) 333 Ali Enayat. Ordinal definable numbers. FOM Jul 23, 2010.
http://cs.nyu.edu/pipermail/fom/2010-July/014944.html
.
The problem was solved in [9]
(to appear in [15]).
Namely, let L[⟨an⟩n<ω] be a
Jω-generic extension of L, where
Jω is the countable power
(with finite support)
of Jensen’s minimal forcing J [8] 444 See also 28A [7] on this forcing.
We acknowledge that the idea to use the countable
power Jω of Jensen’s forcing J to
define such a model belongs to
Ali Enayat [2]..
The key property of J is that it adds
a nonconstructible generic Δ31 real a∈2ω,
in fact {a} is a Π21 singleton.
Accordingly Jω adds a sequence ⟨an⟩n<ω
of J-generic reals real an∈2ω to L, and
as shown in [9, 15] there is no orher
J-generic reals in L[⟨an⟩n<ω] except
for the reals an.
Furthermore, since “being a J-generic real” is
a Π21 relation, it is true in L[⟨an⟩n<ω]
that A={an:\linebreak[0]n<ω} is a countable (infinite)
lightface Π21 set
without OD (ordinal-definable) elements.
Using an uncountable product of forcing notions
similar to Jω,
we defined in [11] a model in which
there is a “planar” Π21 set with countable
vertical cross-sections, which cannot be uniformized
by any real-ordinal definable (ROD)
set.
For a more detailed analysis of the problem,
note that the elements an of the set A, adjoined by
the forcing Jω, are connected to each other only by
the common property of their J-genericity.
Does there exist a similar countable set with a more
definite mathematical structure?
This question was answered in [10]
by a model in which there is
an equivalence class of the equivalence
relation E0 555 Recall that E0 is defined on the Cantor space 2ω
so that xE0y iff the set {n:\linebreak[0]x(n)=y(n)}
is finite.
E0-equivalence classes are countable sets in 2ω,
of course.
(a E0-class, for brevity),
which is a (countable) lightface Π21 set in 2ω,
and does not contain OD elements.
This model makes use of a forcing notion Jinv,
similar to Jensen’s forcing J, but different from
J.
In particular, it consists of Silver trees
(rather than perfect trees of general form, as J does)
and is invariant under finite transformations.
Thus it can be called
an invariant Jensen forcing.
Due to the invariance, Jinv adjoins a
E0-equivalence class of Jinv-generic reals
rather than a single real, and this class turns out to
be a Π21 set without OD elements.
A forcing similar to Jinv was also used in [3]
to define a model with a Π21 Groszek – Laver pair
of E0-classes.
Our main theorem extends this research line.
Theorem 1.1**.**
Let n≥3.
There is a generic extension L[a] of L,
by a real a∈2ω, such that the following is
true in {\mathbf{L}}[a]$$:
- (i)
a∈/OD* and a is minimal over L —
hence each OD real belongs
to L;*
2. (ii)
the E0-class [a]E0 is a
(countable)
lightface Πn1 set — which by (i)
does not contain OD elements*;***
3. (iii)
every countable Σn1 set belongs to L,
hence consists of OD elements.
Thus we have a model, in which, for a given n≥3,
there is a Πn1, hence, OD E0-class
(therefore, a countable set) in 2ω
containing only non-OD elements, and in the same time
every countable Σn1 set belongs to L,
hence consists of OD elements.
The abovementioned result of [10] corresponds to
n=2 in this theorem since countable Σ21 sets
belong to L and consist of OD elements.
2 Connections to the Vitali equivalence relation
The relation E0 is tightly connected with the
Vitali equivalence relation VIT=R/Q
on the true real line R. 666 VIT is defined on R so that
xVITy iff the set x−y
is rational.
In particular, there is a lightface Δ11
(in fact of a very low class Δn0)
injection ϑ:R→2ω which reduces
VIT to E0 in the sense that the equivalence
xVITy⟺ϑ(x)E0ϑ(y) holds for all
x,y∈R.
(See Mycielski and Osofsky [17] for an explicit
construction of ϑ, along with an inverse
reduction of E0 to VIT.)
It follows that Theorem 1.1 is true with
(ii) for [a]VIT
as well, since if C⊆2ω is a Πn1
E0-class not containing OD elements then the
preimage C′={x∈R:\linebreak[0]ϑ(x)∈C} is a Πn1
Vitali class not containing OD elements.
The interest to Vitali classes in this context is inspired
by the observation that they can be viewed as the most
elementary countable sets in R which do not allow
immediate effective choice of an element.
Indeed if a set X⊆R contains at least one
isolated, or even one-sided isolated point, then
one of such points can be chosen effectively.
However any non-empty set X⊆R without
one-sided isolated points is just an everywhere dense
set
(not counting close segments of the complementary set).
Yet the Vitali classes, that is, shifts of the rationals
Q, are exactly the most simple and typical
countable dense sets in R.
Historically, the Vitali relation and its equivalence
classes have deep roots in descriptive set theory.
For instance Sierpinski [18, c. 147]
and Luzin [16, Section 64]
observed that the quotient set R/Q of all Vitali
classes has the property that () it cannot be mapped
into R by an injective Borel map.
On the other hand, as established in [14], in
models of ZF (without the axiom of choice)
the Hartogs number of the set R/Q
(the least cardinal which cannot be injectively mapped
into R/Q)
can be greater than the continuum.
The relations E0 and VIT play a key role in
modern studies of Borel equivalence relations,
being the least ones,
in the sense of the Borel reducibility [5],
among those satisfying ().
3 Structure of the proof
The proof of Theorem 1.1 is arganized as follows.
Basic notions, related to Silver trees in the set
2<ω of all finite dyadic strings,
are introduced in sections 4–7.
Every set P of Silver trees T, closed under
restriction to a given string s∈T,
and under the natural action s⋅T by s∈2<ω,
is considered as a forcing by Silver trees,
a ST-forcing, in brief.
Every ST-forcing adjoins a P-generic real a∈2ω.
Arguing in the constructible universe L, we
define a forcing notion to prove Theorem 1.1
in Section 11
in the form P=⋃α<ω1Pα.
The summands Pα are countable ST-forcings defined
by induction.
Any P-generic extension of L is a
model for Theorem 1.1.
The inductive construction of Pα involves two
key ideas.
The first idea, essentially by Jensen [8],
is to make every level Pα of the construction
generic in some sense over the union of lower
levels Pξ, ξ<α.
This is based on a construction developed in
sections 8 – 10, which includes
the technique of fusion of Silver trees.
A special aspect of this construction, elaborated
in [10],
guarantees that P
is invariant under the group of transformations
(2<ω with the componentwise addition mod 2),
which induces the equivalence relation E0.
This invariance implies that P
(unless Jensen’s original forcing) adjoins
a E0-class of generic reals rather than a single
such real as in [8].
And overall, the successive genericity of the
levels Pα implies that the three sets are
equal in any P-generic extension of L:
the E0-class [a]E0 of the principal generic
real a∈2ω,
the intersection
⋂α<ω1⋃T∈Pα,
and the set of all P-generic reals over L.
This equality, which leads to [a]E0 being
Πn1, is established in
sections 12 – 14.
The second idea goes back to old papers
[6, 13].
In L, let STF be the set of all countable
sequences P=⟨Pξ⟩ξ<α
(α<ω1)
compatible with the first genericity idea.
Then a whole sequence ⟨Pα⟩α<ω1
can be interpreted as a maximal branch in STF.
It happens that if this branch is generic, in
some sense precisely defined in Section 11
((ii) of Theorem 11.4),
with respect to all Σn−11 subsets of STF,
then the ensuing forcing notion
P=⋃α<ω1Pα
inherits some basic forcing properties of the whole
Silver forcing, up to a certain level
of projective hierarchy.
This includes, in particular, the invariance of the
forcing relation with respect to some natural
transformations of Silver trees, leading eventually
to the proof of (iii) of Theorem 1.1
in sections 15 – 17.
But before that the actual construction of
P=⋃α<ω1Pα
involving both mentioned ideas is given
in Section 11.
4 Silver trees
Let 2<ω be the set of all dyadic strings
(finite sequences)
of numbers 0,1 —
including the empty string Λ.
If t∈2<ω and i=0,1, then
t⌢i is the extension of t by i as the rightmost
term.
If s,t∈2<ω then s⊆t means that the string t
extends s, while
s⊂t means a proper extension.
The length of a string s is denoted by lh(s),
and we let
2n={s∈2<ω:\linebreak[0]lh(s)=n} (strings of length n).
As usual, 2ω is the set of
all functions f:ω→2={0,1},
— the Cantor space.
Any string s∈2<ω acts on 2ω so that
(s⋅x)(k)=x(k)+s(k)(mod2) whenever k<lh(s), and
(s⋅x)(k)=x(k) otherwise.
If X⊆2ω and s∈2<ω then let
s⋅X={s⋅x:\linebreak[0]x∈X}.
Similarly, if s∈2m, t∈2n, m≤n, then
define a string s⋅t∈2n by
(s⋅t)(k)=t(k)+s(k)(mod2) whenever k<m, and
(s⋅t)(k)=t(k) whenever m≤k<n.
If m>n, then let s⋅t=(s↾n)⋅t.
In both cases, lh(s⋅t)=lh(t).
If T⊆2<ω then let s⋅T={s⋅t:\linebreak[0]t∈T}.
Definition 4.1**.**
A set T⊆2<ω is a Silver tree,
in symbol T∈ST, whenever there exists an infinite
sequence of strings uk=uk(T)∈2<ω such that
T consists of all strings of the form
s=u0⌢i0⌢u1⌢i1⌢u2⌢i2⌢⋯⌢un⌢in,
and their substrings (including Λ),
where n<ω and ik=0,1.
In this case we let stem(T)=u0
(the stem of T),
and define a closed set [T]⊆2ω
of all branches of T, i. e. all
sequences
a=u0⌢i0⌢u1⌢i1⌢u2⌢i2⌢⋯∈2ω,
where ik=0,1, ∀k.
Let
[TABLE]
in particular, spl0(T)=lh(u0),
so that
spl(T)={spln(T):\linebreak[0]n<ω}⊆ω is the set of all
splitting levels of T∈ST;
spl(T) is infinite.
If u∈T∈ST, then
define the restricted tree
T↾u={t∈T:\linebreak[0]u⊆t∨t⊆u};
T↾u∈ST.
∎
Example 4.2**.**
If s∈2<ω then the tree
B[s]={t∈2<ω:\linebreak[0]s⊆t∨t⊂s}
belongs to ST, stem(B[s])=u0(B[s])=s,
spln(B[s])=lh(s)+n, and if k≥1 then
uk(B[s])=Λ.
In particular B[Λ]=2<ω.
∎
The corresponding sets
[T[s]]={x∈ωω:\linebreak[0]s⊂x} are clopen in 2ω.
Lemma 4.3**.**
Let T∈ST.
Then
- (i)
if a set X⊆2ω is open and X∩[T]=∅,
then there is a string s∈T such that
T↾s⊆X;
2. (ii)
if h∈spl(T) and u,v∈2h∩T then
T↾v=(u⋅v)⋅T↾u and (u⋅v)⋅T=T.
Proof**.**
(i)
If a∈X∩[T] then {a}=⋂nT↾a↾n,
and hence
T↾a↾n⊆X for some n by the compactness.
Let s=a↾n.
∎
5 Splitting Silver trees
The simple splitting of a tree T∈ST consists
of the subtrees
[TABLE]
Then we have T(→i)∈ST, and
u0(T(→i))=u0(T)⌢⟨i⟩⌢u1(T),
and then
uk(T(→i))=uk+1(T) whenever k≥1, and
spl(T(→i))=spl(T)∖{spl0(T)}.
The splitting can be iterated.
Namely if
s∈2n then define
[TABLE]
Separately let T(→Λ)=T, for the empty string Λ.
Lemma 5.1**.**
Let T∈ST, n<ω, and h=spln(T).
Then
- (i)
if s∈2n then T(→s)∈ST,
lh(stem(T(→s)))=h,
and there is a string
u[s]∈2h∩T such that T(→s)=T↾u[s];
2. (ii)
conversely if u∈2h∩T,
then there is a string s[u]∈2n such that
T↾u=T(→s[u]);
3. (iii)
therefore,
{T↾u:\linebreak[0]u∈T}={T(→s):\linebreak[0]s∈2<ω}.
Proof**.**
(i)
u[s]=u0(T)⌢⟨s(0)⟩⌢⋯⌢un−1(T)⌢⟨s(n−1)⟩⌢un(T).
(ii)
Define s=s[u]∈2n by s(k)=u(splk(T))
for all k<n.
(iii)
Let u∈T.
Then spln−1(T)<lh(u)≤spln(T) for some n.
Now, by Definition 4.1,
there exists a (unique) string
v∈2h∩T, where h=spln(T), such that
T↾u=T↾v.
It remains to refer to (ii).
∎
If T,S∈ST and n∈ω then define S⊆nT
(the tree S n-refines T),
whenever
S⊆T and splk(T)=splk(S) for all k<n.
In particular S⊆0T is equivalent to just S⊆T.
By definition if S⊆n+1T then S⊆nT
(and S⊆T).
Lemma 5.2**.**
If T∈ST, n<ω, s0∈2n, and
U∈ST, U⊆T(→s0), then
there is a unique tree T′∈ST such that
T′⊆nT and T′(→s0)=U.
Proof**.**
Let h=spln(T).
Pick a string u0=u[s0]∈2h by
Lemma 5.1(i).
Following Lemma 4.3(ii),
define T′ so that T′∩2h=T∩2h, and if
u∈T∩2h then T′↾u=(u⋅u0)⋅U.
In particular T′↾u0=U.
∎
Lemma 5.3**.**
Let
⋯⊆5T4⊆4T3⊆3T2⊆2T1⊆1T0
be an infinite decreasing sequence of trees ST.
Then
- (i)
T=⋂nTn∈ST;**
2. (ii)
if n<ω and s∈2n+1 then
T(→s)=T∩Tn(→s)=⋂m≥nTm(→s).
Proof**.**
Note that
spl(T)={spln(Tn):\linebreak[0]n<ω}; both claims
easily follow.
∎
The next application of this lemma
and Lemma 5.2 is well known:
Corollary 5.4**.**
Let T∈ST.
If a set X⊆[T] has the Baire property inside [T],
but is not meager inside [T],
then there is a tree S∈ST such that
[S]⊆X.
If f:[T]→2ω is a continuous map then there exists
a tree S∈ST such that S⊆T and f↾[S]
is a bijection or a constant.∎
6 ST-forcings
Definition 6.1**.**
Any set P⊆ST satisfying
- (A)
if u∈T∈P then T↾u∈P, and
2. (B)
if T∈P and σ∈2<ω then σ⋅T∈P,
is called a forcing by Silver trees,
ST-forcing in brief.
∎
Remark 6.2**.**
Any ST-forcing P can be considered as a forcing notion
ordered so that if T⊆T′, then T is a stronger
condition.
The forcing P adjoins a real x∈2ω.
More exactly if a set G⊆P is
P-generic over a given model or set universe
M (and P∈M is assumed)
then the intersection ⋂T∈G[T] contains a
unique real a=a[G]∈2ω, and this real satisfies
M[G]=M[a[G]] and G={T∈P:\linebreak[0]a[G]∈[T]}.
Reals a[G] of this kind are called
P-generic.
∎
Example 6.3**.**
The following sets are ST-forcings:
the set
Pcoh={T[s]:\linebreak[0]s∈2<ω}
of all trees in 4.2 —
the Cohen forcing,
and the set ST of all Silver trees
— the Silver forcing itself.
∎
Lemma 6.4**.**
If ∅=Q⊆ST then the following set
is a ST-forcing:
[TABLE]
Proof**.**
To prove 6.1(A),
let T∈Q and v∈S=σ⋅(T↾u).
Then w=σ⋅v∈T↾u and v=σ⋅w.
It follows that S↾v=σ⋅(T↾u↾w),
where T↾u↾w=T↾u or =T↾w, whenever
accordingly w⊆u or u⊂w.
The second equality of the lemma
follows from Lemma 5.1(iii).
∎
Definition 6.5** (collages).**
If P⊆ST, T∈ST, n<ω, and all split
trees T(→s), s∈2n, belong to P then
T is an n-collage over P.
The set of all n-collages over P is
Colgn(P).
Then
P=Colg0(P)⊆Colgn(P)⊆Colgn+1(P).
∎
Lemma 6.6**.**
Let P⊆ST be a ST-forcing, and n<ω.
Then:
- (i)
if T∈P and s∈2<ω then
T(→s)∈P;
2. (ii)
if T∈ST and s0∈2n
then T(→s0)∈P is equivalent to
T∈Colgn(P);**
3. (iii)
if U∈Colgn(P), s0∈2n, S∈P, and
S⊆U(→s0) then there is a tree
V∈Colgn(P) such that V⊆nU and
V(→s0)=S;
4. (iv)
if U∈Colgn(P) and
D⊆P is open dense in P then there is
a tree V∈Colgn(P) such that V⊆nU
and V(→s)∈D
for all s∈2n.
A set D⊆P is dense in P
if for any S∈P there is a tree T∈D,
T⊆S, and open dense, if in addition
S∈D holds whenever S∈P, T∈D, S⊆T.
Proof**.**
To prove (i) make use of 6.1(A)
and Lemma 5.1(i).
(ii)
If T∈Colgn(P) then by definition T(→s0)∈P.
To prove the converse let h=spln(T) and let a string
u[s]∈2h∩T satisfy
T(→s)=T↾u[s] for all s∈2n
by lemma 5.1(i).
If T(→s0)∈P and s∈2n then
T(→s)=T↾u[s]=(u[s]⋅u[s0])⋅T↾u[s0]=(u[s]⋅u[s0])⋅T(→s0)
by Lemma 4.3(ii).
Therefore T(→s)∈P
by 6.1(B).
And finally T∈Colgn(P).
(iii)
By Lemma 5.2, there is a tree V∈ST,
satisfying V⊆nU and V(→s0)=S.
However V∈Colgn(P) by (ii).
To prove (iv)
apply (iii) 2n times (for all s∈2n).
∎
7 Continuous maps
Let P be a fixed ST-forcing in this section.
Regularity.
We study the behaviour of continuous maps on sets
of the form [T], T∈P.
The next definition highlights the case when a given
continuous f:2ω→2ω is forced to be not equal
to a map of the form x↦σ⋅x, σ∈2<ω.
Definition 7.1**.**
Let T∈P.
A continuous f:2ω→2ω is
regular on T inside P,
if there is no tree T′∈P and string σ∈2<ω
such that T′⊆T and σ⋅f(x)=x
(equivalently, f(x)=σ⋅x)
for all x∈[T′].
∎
Lemma 7.2**.**
Let S,T∈P, f:2ω→2ω
be continuous,
and σ∈2<ω.
Then:
- (i)
there are trees S′,T′∈P such that
S′⊆S, T′⊆T,
[T′]∩(σ⋅f”[S′])=∅;
2. (ii)
if τ∈2<ω, T=τ⋅S, and f
is regular on S inside P,
then there exist trees S′,T′∈P such that
S′⊆S, T′⊆T,
T′=τ⋅S′, and
[T′]∩(σ⋅f”[S′])=∅.
Proof**.**
(i)
Let x0∈[S] and let y0∈[T] be different
from σ⋅f(x0).
As f is continuius, there is m≥lh(σ),
such that
σ⋅(f(x)↾m)=y0↾m whenever
x∈[S] and x↾m=x0↾m.
By 6.1(A),
there are trees S′,T′∈P such that
S′⊆S, T′⊆T,
x↾m=x0↾m for all x∈[S′], and
y↾m=y0↾m for all y∈[T′].
(ii)
Assume that lh(σ)=lh(τ)
(otherwise the shorter string can be extended by zeros).
The set X={x∈[S]:\linebreak[0]σ⋅f(x)=τ⋅x}
is open in [S] and non-empty, by the regularity.
Let x0∈X.
There is a number m≥lh(σ)=lh(τ) satisfying
τ⋅(x0↾m)=σ⋅(f(x0)↾m).
By 6.1(A) there is
a tree S′∈P satisfying x0∈[S′] and
x↾m=x0↾m, f(x)↾m=f(x0)↾m
for all x∈[S′].
Put T′=τ⋅S′.
∎
Coding continuous maps.
If f:2ω→2ω is continuous, k<ω and i=0,1
then the set Dki(f)={x∈2ω:\linebreak[0]f(x)(k)=i},
and
Dk0(f)∩Dk1(f)=∅,
Dk0(f)∪Dk1(f)=2ω.
Let Cki(f)
be the set of all ⊆-minimal strings s∈2<ω
such that B[s]⊆Dki(f).
Then Ck0(f),Ck1(f)⊆2<ω are finite
disjoint irreducible antichains 777 An antichain A⊆2<ω
is irreducible, if it does not contain a
pair of the form s⌢0,s⌢1.
in 2<ω, and
Dki(f)=⋃s∈Cki(f)B[s],
while the union Ck0(f)∪Ck1(f) is a
maximal antichain in 2<ω.
Let code(f)=⟨Cki(f)⟩k<ω,i=0,1
— the code of f.
The other way around, if
c=⟨Cki⟩k<ω,i=0,1 is a family
of finite irreducible antichains Cki⊆2<ω,
and if k<ω then
Ck0∩Ck1=∅ while
Ck0∪Ck1 is a maximal antichain in 2<ω,
then c is called a code of continuous function.
In this case, the related continuous function
f:2ω→2ω is denoted by fc, that is,
fc(x)(k)=i whenever
x∈⋃s∈CkiB[s].
Let CCF denote the set of all
codes of continuous functions.
8 Generic extensions of ST-forcings
The forcing notion to prove Theorem 1.1
will be defined in the form of an ω1-union
of its countable parts — levels.
The next definition presents requirements which
will govern the interactions between the levels.
Definition 8.1**.**
Let M be any set and P be a ST-forcing.
We say that another ST-forcing Q
is an M-extension of P,
in symbol P⊏MQ, if the following holds:
- (A)
Q is dense in Q∪P;
2. (B)
if a set D∈M, D⊆P is pre-dense in P
and U∈Q then U⊆fin⋃D, that is,
there is a finite set D′⊆D such that
U⊆⋃D′;
3. (C)
if T0∈P,
f:2ω→2ω is a continuous map with a code in
M, regular on T0 inside P, and U,V∈Q,
U⊆T0,
then [V]∩(f”[U])=∅.∎
Speaking of (C), it claims essentially that
if the regularity holds then
T0 forces, in the sense of
Q∪P, that f(a[G]) does not belong
to ⋃V∈Q[V].
If M=∅ then we write P⊏Q
instead of P⊏∅Q;
in this case (B) and (C)
are trivial.
Generally, we’ll consider, in the role of M,
transitive models of the theory ZFC′
which includes all ZFC axioms except for the Power
Set axiom, but an axiom is adjoined, which claims
the existence of P(ω).
(Then the existence of ω1 and sets like 2ω
and ST
easily follows.)
Lemma 8.2**.**
Let M⊨ZFC′ be a transitive model,
P∈M and Q be
ST-forcings satisfying P⊏MQ, and
U∈Q.
Then
- (i)
if T∈P then [U]∩[T]
is clopen in [U];
2. (ii)
if D∈M, D⊆P is pre-dense in P
then D remains pre-dense in Q∪P;
3. (iii)
if T,T′∈P
are incompatible in P then T,T′
are incompatible in Q∪P, too, and moreover
if U∈Q then [T]∩[T′]∩[U]=∅;
4. (iv)
if R⊆U is a Silver tree
then the set
R=Q∪{σ⋅(R(→t)):\linebreak[0]t,σ∈2<ω}
is a ST-forcing, and still
P⊏MR.
Proof**.**
(i)
The set
D(T)={S∈P:\linebreak[0]S⊆T∨[S]∩[T]=∅}
belongs to M and is open dense in P by
6.1(A).
Then by 8.1(B) there is a finite
set D′⊆D(T) such that U⊆⋃D′.
But then we have
[U]∖[T]=⋃S∈D′′([S]∩[W]),
where D′′={S∈D′:\linebreak[0][S]∩[T]=∅}.
Thus [U]∖[T] is a closed set.
(ii)
Let U∈Q.
Then by 8.1(B) there is a finite
set D′⊆D such that U⊆⋃D′.
There is a tree T∈D′ such that [T]∩[U]
has a non-empty open interior in [U].
By Lemma 4.3(i),
there is s∈U such that
[U′]⊆[T]∩[U], where U′=U↾s,
thus U′⊆U∩T.
Finally U′∈Q, as Q is a ST-forcing.
(iii)
By the incompatibility,
if S∈P then S⊆T or S⊆T′,
and hence there is a tree S′∈P,
S′⊆S, satisfying [S′]∩[T]∩[T′]=∅.
Therefore the set
D={S∈P:\linebreak[0][S]∩[T]∩[T′]=∅}
is dense in P and belongs to M.
Now if U∈Q then U⊆fin⋃D by
8.1(B), thus immediately
[U]∩[T]∩[T′]=∅.
(iv)
R is a ST-forcing by Lemma 6.4, so we have
to prove P⊏MR.
We skip a routine verification of
8.1(A),(B)
and focus on (C).
Let T0, f be as in (C).
Consider trees
R′=σ⋅(R(→t))∈R, R′⊆T0, and
V∈Q; we have to prove that
[V]∩(f”[R′])=∅.
The problem is that while
R′⊆σ⋅R⊆U′=σ⋅U,
it may not be true that U′⊆T0.
But, now we claim that
there is a finite set of trees
{U1,…,Un}⊆Q such that
R′⊆U1∪…∪Un⊆T0.
If this is established then
[V]∩(f”[Ui])=∅ for all i since
P⊏MQ, and we are done.
To prove the claim consider the dense set
D(T0)∈M as in the proof of (i) above.
Then U′⊆fin⋃D, hence there is a finite
set D′⊆D(T0) satisfying U′⊆⋃D′.
As by construction R′⊆U′∩T0,
we conclude that R′⊆⋃D′′,
where D′′={S∈D′:\linebreak[0]S⊆T0}.
Now if S∈D′′ then [S]∩[U′] is clopen
in [U′],
therefore [S]∩[U′]=⋃v∈W(S)U′↾v,
where W(S)⊆U′ is a suitable finite set.
We put
{U1,…,Un}=⋃S∈D′′{U′↾v:\linebreak[0]v∈W(S)}.
∎
Theorem 8.3**.**
Let M⊨ZFC′ be a countable transitive model
and P∈M be a ST-forcing.
Then there exists a countable ST-forcing Q
satisfying P⊏MQ.
The proof of this theorem is presented below.
Section 9 contains the definition of
the ST-forcing Q, while the proof of its
properties follows in Section 10.
9 Construction of extending ST-forcing
The next definition formalizes a construction of
countably many Silver trees by means of
Lemma 5.3.
Definition 9.1**.**
A system is any indexed set
φ=⟨⟨νmφ,τmφ⟩⟩m∈∣φ∣,
where ∣φ∣⊆ω is finite,
and if m∈∣φ∣ then
νmφ∈ω,
τmφ=⟨Tmφ(0),Tmφ(1),…,Tmφ(νmφ)⟩,
each Tmφ(n) is a Silver tree,
and Tmφ(n+1)⊆n+1Tmφ(n)
whenever n<νmφ.
In this case, if n≤νmφ and s∈2n
then let Tmφ(s)=Tmφ(n)(→s).
If P is a ST-forcing then Sys(P)
is the set of all system φ such that
Tmφ(n)∈Colgn(P) for all
m∈∣φ∣ and n≤νmφ.
Then every tree Tmφ(s)
belongs to P.
∎
A system φ extends a system ψ,
in symbol ψ≼φ,
if ∣ψ∣⊆∣φ∣, and
for any index m∈∣ψ∣, first,
νmφ≥νmψ, and second,
τmφ extends τmψ in the sense that
simply Tmφ(n)=Tmψ(n) for all
n≤νmψ.
Lemma 9.2**.**
Let P be a ST-forcing and
φ∈Sys(P).
If m∈∣φ∣ and n=νmφ then the
extension φ′ of the system φ by
νmφ′=n+1 and
Tmφ′(n+1)=Tmφ(n) belongs to
Sys(P) and φ≼φ′.
If m∈/∣φ∣ and T∈P then the
extension φ′ of the system φ by
∣φ′∣=∣φ∣∪{m},
νmφ′=0 and
Tmφ′(0)=T,
belongs to Sys(P) and φ≼φ′.∎
Now, according to the formulation of Theorem 8.3,
we assume that
M⊨ZFC′ is a countable transitive model
and P∈M is a (countable) ST-forcing.
Definition 9.3**.**
(i)
We fix a ≼-increasing sequence
Φ=⟨φ(j)⟩j<ω
of systems
φ(j)∈Sys(P),
generic over M in the sense that it
intersects every set
D∈M,\linebreak[0]D⊆Sys(P) dense in Sys(P).
The density here means that for any system ψ∈Sys(P)
there is a system φ∈D such that ψ⊆φ.
The goal of this definition is to define another
ST-forcing Q from Φ, see item (iv) below.
(ii)
If m,n<ω then the set
Dmn={φ∈Sys(P):\linebreak[0]νmφ≥n}
is dense by Lemma 9.2 and belongs to M,
hence it intersects Φ.
Therefore if m<ω then there exists an infinite
sequence
[TABLE]
of trees TmΦ(n)∈Colgn(P) such that
for each j, if
m∈∣φ(j)∣ and n≤νmφ(j),
then Tmφ(j)(n)=TmΦ(n).
If n<ω and s∈2n then let
TmΦ(s)=TmΦ(n)(→s);
then TmΦ(s)∈P because
TmΦ(n)∈Colgn(P).
(iii)
In this case, by Lemma 5.3, every set
[TABLE]
belongs to ST,
the same is true for all subtrees UmΦ(→s),
and we have
[TABLE]
by Lemma 5.3,
and it is clear that UmΦ=UmΦ(→Λ).
In addition if strings s,t∈2<ω
satisfy s⊆t then
TmΦ(s)⊆TmΦ(t) and UmΦ(→s)⊆UmΦ(→t),
but if s,t are ⊆-incomparable then
[UmΦ(→s)]∩[UmΦ(→t)]=[TmΦ(s)]∩[TmΦ(t)]=∅.
(iv)
Finally the set
Q={σ⋅UmΦ(→s):\linebreak[0]m<ω∧σ,s∈2<ω}
is a countable ST-forcing by Lemma 6.4.
∎
10 Validation of the extension property
Here we prove that P⊏MQ
in the context of Definition 9.3.
We check all requirements of Definition 8.1.
8.1**(A)****.**
If T∈P then
the set Δ(T) of all
systems φ∈Sys(P)∩M
such that Tmφ(0)=T for some m,
belongs to M and is dense in Sys(P) by
Lemma 9.2.
Therefore φ(J)∈Δ(T) for some J,
by the choice of Φ.
Then TmΦ(0)=T for some m<ω.
But UmΦ(→Λ)=UmΦ⊆TmΦ(0) and
UmΦ∈Q.
8.1**(B)****.**
Let U=σ⋅UmΦ(→s)∈Q,
where m<ω and s,σ∈2<ω.
We have to check U⊆fin⋃D.
We can assume, as above, that σ=Λ,
that is, U=UmΦ(→s).
(Otherwise substitute σ⋅D for D.)
We can also assume that s=Λ,
that is, U=UmΦ, as
UmΦ(→s)⊆UmΦ.
Thus let U=UmΦ.
The set Δ∈M of all systems
φ∈Sys(P) such that
m∈∣φ∣ and for every string t∈2n,
where n=νmφ, there is a tree St∈D with
Tmφ(t)⊆St,
is dense in Sys(P) by lemma 6.6(iv)
due to the pre-density of D itself.
Therefore there is an index j such that
φ(j)∈Δ.
Let this be witnessed by trees
St∈D,\linebreak[0]t∈2n,
where n=νmφ(j),
so that Tmφ(j)(t)⊆St, ∀t,
and hence Tmφ(j)(n)⊆finD.
Then
U=UmΦ⊆TmΦ(n)=Tmφ(j)(n)⊆fin⋃D.
8.1**(C)****.**
Let T0∈P, f, and U,V∈Q be as in
8.1(C).
Then U=τ⋅UKΦ(→s0), where
s0,τ∈2<ω and K<ω.
We can wlog assume that τ=Λ,
that is, U=UKΦ(→s0), since the general case is
reducible to this case by the substitution
of τ⋅T0 for T0 and
the function f′(x)=f(τ⋅x) for f.
Thus let U=UKΦ(→s0).
Similarly, generally speaking
V=ρ⋅ULΦ(→t0), where t0,ρ∈2<ω
and L<ω.
But this is reducible to the case ρ=Λ
by the substitution of
f′(x)=ρ⋅f(x) for f.
Thus let V=ULΦ(→t0).
Finally, since ULΦ(→t0)⊆ULΦ, we can
assume that even V=ULΦ.
Now consider the set Δ∈M of all systems
φ∈Sys(P) such that there is
a number m<ω satisfying the following:
- (I)
K,L∈∣φ∣, νKφ=νLφ=m,
and lh(s0)≤m;
2. (II)
if s∈2m then TKφ(s)⊆T0 or
[TKφ(s)]∩[T0]=∅;
3. (III)
if s∈2m and TKφ(s)⊆T0 then
TLφ(m)∩(f”[TKφ(s)])=∅.
Lemma 10.1**.**
The set Δ is dense in Sys(P).
Proof**.**
Let ψ∈Sys(P);
we have to define a system φ∈Δ satisfying
ψ≼φ.
By lemma 9.2, we can assume that K,L∈∣ψ∣
and
νKψ=νLψ=m−1 for some m≥lh(s0).
Now we define a first preliminary version of
φ, by νKφ=νLψ=m and
TKφ(m)=TKψ(m−1), TLφ(m)=TLψ(m−1),
and keeping the other elements of φ equal to
those of the system ψ, so that ψ≼φ.
The trees S=TKφ(m) and T=TLφ(m)
belong to Colgm(P).
The set D(T0) of all trees W∈P,
such that W⊆T0 or [W]∩[T0]=∅,
is open dense in P by 6.1(A).
Therefore by Lemma 6.6(iv)
there is a tree S′∈Colgm(P) satisfying
S′⊆mS and if s∈2m then S′(→s)∈D(T0).
We modify φ by putting TKφ(m)=S′
instead of S.
It is clear that the new system still satisfies
ψ≼φ, and in addition (II)
holds by construction.
Further modification of φ towards (III)
depends on whether K=L.
Case 1: K=L.
If s,t∈2m then by Lemma 7.2(i)
there exist trees C,D∈P such that
C⊆S(→s), D⊆T(→t), and
[D]∩(f”[C])=∅.
Applying Lemma 6.6(iii), we get trees
S′,T′∈Colgm(P) satisfying
S′⊆mS, T′⊆mT, C=S′(→s), D=T′(→t),
so that [T′(→t)]∩(f”[S′(→s)])=∅.
Iterate this construction by exhaustion of
all pairs s,t∈2m.
We get trees S∗,T∗∈Colgm(P)
such that S∗⊆mS, T∗⊆mT, and
[T∗(→t)]∩(f”[S∗(→s)])=∅
for all s,t∈2m, that is
[T∗]∩(f”[S∗])=∅.
Nodify φ by
TKφ(m)=S∗ instead of S and
TLφ(m)=T∗ instead of T.
Now (III) holds for the modified φ.
Case 2: K=L, and then
S=T=TKφ(m)=TLφ(m).
It suffices to show that if s,t∈2n
(strings of length n) and S(→s)⊆T0,
then there is a tree S′∈Colgn(P) such that
S′⊆mS and
[S′(→t)]∩(f”[S′(→s)])=∅.
Then the iteration by exhaustion of all
those pairs of strings s,t yields a tree
S∗∈Colgm(P) such that
S∗⊆mS and
[T∗(→t)]∩(f”[S∗(→s)])=∅
for all s,t∈2m with S(→s)⊆T0, that is,
[S∗]∩(f”[S∗(→s)])=∅
whenevew s∈2m satisfies
S(→s)⊆T0.
To achieve (III), it remains
to modify the system φ by
TKφ(m)=S∗ instead of S.
Thus let us carry out the construction of S′
for a pair of strings
s,t∈2n with S(→s)⊆T0.
It follows that f
is regular on S(→s) inside P.
By Lemma 5.1(i), we have
S(→s)=S↾u and S(→t)=S↾v,
where u,v∈T are strings of length
h=lh(u)=lh(v), and
S(→s)=τ⋅(S(→t)),
where τ=u⋅v, by
Lemma 4.3(ii).
Lemma 7.2(ii) yields a pair of
trees U,V∈P satisfying
U⊆S(→s), V⊆S(→t), V=τ⋅U, and
[V]∩(f”[U])=∅.
Now, twice reducing the tree S by means of
Lemma 6.6(iii), we get a tree
S′∈Colgn(P) such that S′⊆mS and
S′(→s)=U, S′(→t)=V, so that
[S′(→t)]∩(f”[S′(→s)])=∅,
as required.
□ (Lemma)
Now return to the verification of 8.1(C).
By the lemma, at least one
system φ(j) belongs to Δ, that is, conditions
(I), (II), (III)
are satisfied for φ=φ(j).
The tree V=ULΦ satisfies
V⊆T=TLφ(j)(m).
Moreover, the tree
U=UKΦ(→s0) satisfies
U⊆S=⋃s∈ΣTKφ(j)(s),
where Σ={s∈2m:\linebreak[0]S(→s)⊆T0},
by (I), (II).
However [T]∩(f”[S])=∅
by (III),
thus [V]∩(f”[U])=∅,
as required.
□ (Theorem 8.3)
11 The blocking sequence of ST-forcings
We argue in the constructible universe L
in this section.
The forcing to prove Theorem 1.1
will be defined as the union of a ω1-sequence
of countable ST-forcings, increasing in the sense of
a relation ⊏
(Definition 8.1).
We here introduce the notational system to be used
in this construction.
Let STF be the set of all countable ST-forcings.
If P=⟨Pξ⟩ξ<ω1
is a transfinite sequence of countable ST-forcings,
of length domP=λ<ω1,
then let ⋃P=⋃ξ<λPξ,
and let M(P) be the least transitive model
of ZFC− of the form Lϑ, containing P,
in which λ and ⋃P are countable.
Definition 11.1**.**
If α∈Ord then let STFα
be the set of all λ-sequences
P=⟨Pξ⟩ξ<α
of forcings Pξ∈STF,
satisfying the following:
- (∗)
if γ<domP then
⋃(P↾γ)⊏M(P↾γ)Pγ.
Let STF=⋃α<ω1STFα.
∎
The set STF∪STFω1 is ordered by the
extension relations ⊂ and ⊆.
Lemma 11.2**.**
Assume that κ<λ<ω1,
and P=⟨Pξ⟩ξ<κ∈STF.
Then:
- (i)
the union P=⋃P is a countable
ST-forcing*;***
2. (ii)
there is a sequence Q∈STF
such that dom(Q)=λ and
P⊂Q.
Proof**.**
To prove (ii) apply Theorem 8.3 by induction
on λ.
∎
Definition 11.3** (key definition).**
A sequence P∈STF
blocks a set W⊆STF if either
P∈W (the positive block case)
or there is no sequence
Q∈W satisfying P⊆Q
(the negative block case).
∎
Approaching the next
blocking sequence theorem,
we recall that HC is the set of all
hereditarily countable sets, so that
HC=Lω1 in L.
See [1, Part B, Chap. 5, Section 4]
on definability classes ΣnX,ΠnX,ΔnX
for any set X,
and especially on ΣnHC,ΠnHC,ΔnHC for
X=HC in [12, Sections 8, 9] or elsewhere.
Theorem 11.4** (blocking sequence theorem, in L).**
If n≥3 then there is a sequence
P=⟨Pξ⟩ξ<ω1∈STFω1
satisfying the following two conditions:
- (i)
P,
as the set of pairs ⟨ξ,Pξ⟩,
belongs to the definability class Δn−1HC;
2. (ii)
(genericity of P w. r. t. Σn−2HC(HC) sets)*
if W⊆STF is a Σn−2HC(HC) set
(that is parameters from HC are admitted),
*then there is an ordinal γ<ω1 such that
the restricted sequence
P↾γ=⟨Pξ⟩ξ<γ∈STF
blocks W.
Proof**.**
Let ⩽L be the canonical Δ1 wellordering of L;
thus its restriction to HC=Lω1 is Δ1HC.
As n≥3, there exists a universal Σn−2HC set
U⊆ω1×HC.
That is, U is Σn−2HC
(parameter-free Σn−2 definable in HC),
and for every set X⊆HC of class Σn−2HC(HC)
(definable in HC by a Σn−2 formula with arbitrary
parameters in HC)
there is an ordinal α<ω1 such that X=Uα,
where Uα={x:\linebreak[0]⟨α,x⟩∈U}).
The choice of ω1 as the domain of parameters is
validated by the assumption V=L, which implies the
existence of a Δ1HC surjection ω1⟶ontoHC.
Coming back to Definition 11.3, note that for any
sequence P∈STF and any set W⊆STF
there is a sequence Q∈STF which satisfies
P⊂Q and blocks W.
This allows us to define Qα∈STF by induction
on α<ω1 so that Q0=∅,
Qλ=⋃α<λQα, and each
Qα+1 is equal to the ⩽L-least
sequence Q∈STF which satisfies
Qα⊂Q and blocks Uα.
Then P=⋃α<ω1Qα∈STFω1.
Condition (ii) holds by construction, while
(i) follows by a routine verification,
based on the fact that STF∈Δ1HC.
∎
Definition 11.5** (in L).**
We fix a natural number n≥3, for which
Theorem 1.1 is to be established.
We also fix a sequence
P=⟨Pξ⟩ξ<ω1∈STFω1,
given by Theorem 11.4 for this n.
If α<ω1 then let Mα=M(P↾α)
and P<α=⋃ξ<αPξ.
Let
P=⋃ξ<ω1Pξ.
∎
12 CCC and some other forcing properties
The ST-forcing P defined by 11.5
will be the forcing notion for the proof
of Theorem 1.1.
Here we establish some forcing properties of
P, including CCC.
We continue to argue in the conditions and
notation of Definition 11.5.
Lemma 12.1**.**
P* and all sets Pξ,
P<α are ST-forcings.
In addition:*
- (i)
if α<ω1 then P<γ⊏MγPγ;
2. (ii)
*if α<ω1 and the set
D∈Mα,\linebreak[0]D⊆P<α
is pre-dense in P<α then it is
pre-dense in P, too**;***
3. (iii)
every set Pα is pre-dense in P;
4. (iv)
if Q⊆ST belongs to
Σn−2HC(HC) and
Q−={T∈ST:\linebreak[0]¬∃S∈Q(S⊆T)}
then P∩(Q∪Q−) is dense in P;**
5. (v)
if c∈CCF is a code of continuous function
and
[TABLE]
then the set P∩CBc is dense in P;**
6. (vi)
let D={T∈ST:\linebreak[0]spl(T) is co-infinite}
(see Definition 4.1 on spl(T)),
then
the set P∩D is dense in P.
Proof**.**
(i)
holds by (∗) ‣ 11.1 of Definition 11.1.
(ii)
We use induction on γ,\linebreak[0]α≤γ<ω1,
to check that if D is pre-dense in P<γ
then it remains pre-dense in
P<γ∪Pγ=P<γ+1 by (i)
and 8.1(B).
Limit steps, including the final step to P
(γ=ω1) are routine.
(iii)
Pα is dense in
P<α+1=P<α∪Pα
by 8.1(A).
It remains to refer to (ii).
(iv)
Let T0∈P, that is,
T0∈P<α0, α0<ω1.
The set W of all sequences P∈STF,
such that P↾α0⊆P and
∃T∈Q∩(⋃P)(T⊆T0),
belongs to Σn−2HC(HC)
along with Q.
Therefore there is an ordinal α<ω1 such that
P↾α blocks W.
We have two cases.
Case 1:
P↾α∈W.
Then the related tree T⊆T0 belongs to
Q∩P.
Case 2:
there is no sequence in W which extends
P↾α.
Let γ=max{α,α0}.
Then P<γ⊏MγPγ by (i).
As α0<γ, there is a tree T∈Pγ,
T⊆T0.
We claim that T∈Q−, which completes the
proof in Case 2.
Suppose to the contrary that T∈/Q−,
thus there is a tree S∈Q, S⊆T.
The set
R=Pγ∪{σ⋅(S(→t)):\linebreak[0]t,σ∈2<ω}
is a countable ST-forcing and
P<γ⊏MγR by Lemma 8.2(iv).
It follows that the sequence R defined by
domR=γ+1,
R↾γ=P↾γ, and R(γ)=R,
belongs to STF, and even R∈W since
S∈Q∩R.
Yet P↾α⊏MγR by construction,
which contradicts to the Case 2 hypothesis.
(v)
A routine estimation gives CBc∈Σ1HC({c}).
The set CBc is dense in ST
by Corollary 5.4,
thus (CBc)− is empty.
Now the result follows from (iv).
(vi)
Similarly to (v), D∈Σ1HC
and D is dense in ST.
∎
Corollary 12.2**.**
If α<ω1 and trees T,T′∈P<α
are incompatible in P<α then T,T′
are incompatible in P, too.
Proof**.**
Prove by induction on γ that if α<γ≤ω1
then T,T′ are incompatible in P<γ, using
Lemma 12.1(i),
and Lemma 8.2(iii) on limit steps.
∎
To prove CCC we’ll need the following lemma.
Lemma 12.3** (in L).**
If X⊆HC=Lω1 then the set OX
of all ordinals α<ω1 such that the model
⟨Lα;X∩Lα⟩
is an elementary submodel of ⟨Lω1;X⟩
and X∩Lα∈Mα, is unbounded in ω1.
Generally if Xn⊆HC for all n
then the set O of all ordinals
α<ω1 such that
⟨Lα;⟨Xn∩Lα⟩n<ω⟩ is
an elementary submodel of
⟨Lω1;⟨Xn⟩n<ω⟩
and ⟨Xn∩Lα⟩n<ω∈Mα,
is unbounded in ω1.
Proof**.**
Let α0<ω1.
There is a countable elementary submodel M
of ⟨Lω2;∈⟩
which contains α0,\linebreak[0]ω1,\linebreak[0]X
and is such that the set M∩Lω1 is transitive.
Consider the Mostowski collapse ϕ:M⟶ontoLλ.
Let α=ϕ(ω1).
Then α0<α<λ<ω1 and ϕ(X)=X∩Lα
by the choice of M.
We conclude that ⟨Lα;X∩Lα⟩ is
an elementary submodel of ⟨Lω1;X⟩.
And α is uncountable in Lλ, hence
Lλ⊆Mα.
It follows that X∩Lα∈Mα, as
X∩Lα∈Lλ by construction.
The more general claim is proved similarly.
∎
Corollary 12.4** (in L).**
P* is a CCC forcing, therefore
P-generic extensions preserve cardinals.*
Proof**.**
Consider any maximal antichain A⊆P.
By Lemma 12.3 there is an orrdinal α
such that ⟨Lα;P′,A′⟩ is
an elementary submodel of ⟨Lω1;P,A⟩,
where P′=P∩Lα and A′=A∩P<α,
and in addition P′,A′∈Mα.
By the elementarity, we have
P′=P<α and A′=A∩P<α∈Mα,
and A′ is a maximal antichain, hence a pre-dense
set, in P<α.
But then A′ is a pre-dense set, hence,
a maximal antichain, in the whole set P
by Lemma 12.1(ii).
Thus A=A′ is countable.
∎
13 Generic model
This section presents some properties of
P-generic extensions L[G] of L
obtained by adjoining a P-generic
set G⊆P to L.
Recall that the forcing notion P∈L
was introduced by Definition 11.5, along with
some related notation.
The next lemma involves the coding system for
continuous maps introduced in Section 7.
If G⊆P is generic over L
and c∈CCF∩L,
then define c[G]=fc(a[G])∈2ω∩L[G];
the definition of a[G] see 6.2.
Lemma 13.1** (continuous reading of names).**
If a set G⊆P is generic over L
and x∈2ω∩L[G] then
there exists a code c∈CCF∩L
such that x=c[G].
Proof**.**
One of basic forcing lemmas
(Lemma 2.5 in [1, Chap. 4])
claims that there is a P-name t∈L for x,
satisfying x=t[G]
(the G-valuation of t),
and it can be assumed that P forces that t
is valuated as a real in 2ω.
Then the sets
Fni={T∈P:\linebreak[0]T forces t(n)=i}
(n<ω and i=0,1)
satisfy the following:
- (1)
the indexed set ⟨Fni⟩n<ω∧i=0,1
belongs to L;
2. (2)
if n<ω, S∈Fn0, T∈Fn1, then S,T
are incompatible in P;
3. (3)
if n<ω then the set Fn=Fn0∪Fn1
is open dense in P.
We argue in L.
Pick a maximal antichain An⊆Fn in each Fn.
Then all sets An are maximal antichains in P
by (3), and all An are countable by
Corollary 12.4.
Therefore there is an ordinal α<ω1L such that
the set ⋃nAn⊆P<α
and the sequence ⟨An⟩n<ω belong to Mα.
Note that G∩Pα=∅ by
Lemma 12.1(iii); let U∈G∩Pα.
As P<α⊏MαPα
by Lemma 12.1(i),
we have U⊆fin⋃An for all n, there exists
a finite set
An′⊆An such that U⊆⋃An′.
Let Ani′=An′∩Fni and
Xni=[U]∩⋃T∈Ani′[T], i=0,1.
We claim that Xn0∩Xn1=∅.
Indeed otherwise there exist trees Ti∈Fni
such that Z=[U]∩[T0]∩[T1] is non-empty.
By Lemma 8.2(i), Z is clopen in [U].
Therefore there is a tree U′∈Pα such that
[U′]⊆Z, hence, T0 and T1
are compatible in P,
which contradicts (2) by construction.
Thus indeed Xn0∩Xn1=∅.
As clearly Xn0∪Xn1=[U], we can define
a continuous g:[U]→2ω such that
g(x)(n)=i iff x∈Xni.
The map g can be extended to a continuous
f:2ω→2ω, that is f(x)(n)=i whenever
x∈Xni — for all n<ω and i=0,1.
We have f=fc, where c∈CCF∩L.
We argue in L[G].
We skip a routine verification of x=c[G].
∎
Lemma 13.2**.**
If G⊆P is generic over L then a[G]
is not
OD in L[G].
Proof**.**
Assume to the contrary that
ϑ(x) is a formula with ordinal parameters,
and a tree T∈G P-forces that
a[G] is the only real x∈2ω
satisfying ϑ(x).
Let s=stem(T) and n=lh(s).
Then T contains both s⌢0 and s⌢1.
Then either s⌢0⊂a[G] or s⌢1⊂a[G].
Let say s⌢0⊂a[G].
Let σ=0n⌢1, so that the strings
s⌢0, s⌢1, σ belong to 2n+1,
s⌢1=σ⋅s⌢0, and σ⋅T=T
by Lemma 4.3(ii).
As P is invariant under the action of σ,
the set G′=σ⋅G={σ⋅S:\linebreak[0]S∈G}
is P-generic over L, and T=σ⋅T∈G′.
We conctude that it is true in L[G′]=L[G] that
a[G′]=σ⋅a[G] is still the unique real in
2ω satisfying ϑ(a[G′]).
But a[G′]=a[G]!
∎
14 Definability of the set of generic reals
We continue to argue in the context of
Definition 11.5.
The goal of this section is to study the definability
of the set of all P-generic reals x∈2ω
in P-generic extensions of L.
Lemma 14.1**.**
In an transitive model of ZF extending L,
it is true that a real x∈2ω is
P-generic over L iff
x belongs to the set GENP=⋂α<ω1L⋃T∈Pα[T].
Proof**.**
All sets Pα are pre-dense in
P by Lemma 12.1(iii).
Therefore all P-generic reals belong
to GENP.
On the other hand, any maximal antichain
A∈L,\linebreak[0]A⊆P is countable in L
by Corollary 12.4,
and hence A⊆P<α and A∈Mα
for some index α<ω1L.
But then every tree T∈Pα satisfies
T⊆fin⋃A by Lemma 8.2(ii).
We conclude that
⋃T∈Pα[T]⊆⋃S∈A[S].
∎
According to the next lemma, P-generic
extensions do not contain
P-generic reals,
except the real a[G] itself and reals connected
to a[G] in terms of the equivalence relation E0
(see Footnote 5).
We observe that the E0-class
[TABLE]
of any real x∈2ω is a countable set.
Lemma 14.2**.**
Let G⊆P be a P-generic set
over L.
Then it is true in L[G] that GENP=[a[G]]E0.
Proof**.**
The real a[G] is P-generic,
hence a[G]∈GENP by Lemma 14.1.
Yet every set Pα is a ST-forcing,
that is by definition it is closed under the action
s⋅T of any string s∈2<ω.
This implies [a[G]]E0⊆GENP.
To prove in the other direction, assume to the
contrary that x∈L[G]∩2ω,
x∈GENP∖[a[G]]E0.
By Lemma 13.1,
there is a code c∈L∩CCF such that
x=c[G].
By the contrary assumption there is a tree T0∈G
which forces
c[G]∈GENP∖[a[G]]E0.
Fix an ordinal α<ω1L such that c∈Mα.
We claim that (in L)
the function f=fc
is regular on T0 inside P<α.
Indeed otherwise there exist
σ∈2<ω and T∈P<α such that T⊆T0
and σ⋅f(x)=x for all x∈T.
Then T forces σ⋅c[G]=a[G],
that is, forces c[G]∈[a[G]]E0,
contrary to the choice of T0.
The regularity is established.
Recall that P<α⊏MαPα by
Lemma 12.1(i).
Therefore by 8.1(A),
there is a tree U∈Pα, U⊆T0.
And by 8.1(C) if V∈Pα
then [V]∩(f”[U])=∅.
Thus if V∈Pα then U forces
c[G]∈/[V], hence forces
c[G]∈/GENP,
which contradicts to the choice of T0.
∎
Corollary 14.3**.**
Let G⊆P be a P-generic set
over L.
Then the E0-class [a[G]]E0 is a
Πn1 set in L[G].
Proof**.**
A routine verification of GENP∈Πn1 in L[G]
using the property 11.4(i) of the sequence
P is left to the reader.
∎
15 Auxiliary forcing relation
Here we introduce a key tool for the proof of
claim (i) of Theorem 1.1.
This is a forcing-like relation forc.
It is not explicitly connected with the forcing notion
P
(but rather connected with the full
Silver forcing ST),
however it will be compatible with P for
formulas of certain quantifier complexity
(Lemma 17.1).
The crucial advantage of forc will be its invariance
under two certain groups of transformations
(Lemma 16.1),
a property that cannot be expected for P.
This will be the key argument in the proof
of Theorem 17.2 below.
We argue in L.
We consider a language L containing
variables i,j,k,… of type 0 with the domain ω
and variables x,y,z,… of type 1 with the domain 2ω.
Terms are variables of type 0 and
expressions like x(k).
Atomic formulas are those of the form R(t1,…,tn),
where R⊆ωn is any n-ary relation
on ω in L.
A formula is arithmetic if it does not contain
variables of type 1.
Formulas of the form
[TABLE]
where Ψ is arithmetic, are of types
LΣn1, resp., LΠn1.
In addition we allow codes
c∈CCF to substitute free variables of type 1.
The semantics is as follows.
Let φ:=φ(c1,…,ck) be an L-formula,
with all codes in CCF explicitly indicated, and
let x∈2ω.
By φ[x] we denote the formula
φ(fc1(x),…,fck(x)),
where all fci(x) are reals in 2ω, of course.
Arithmetic formulas and those in LΣn1∪LΠn1,
n≥1, will be called normal.
If φ is a formula in LΣn1 or LΠn1 then
φ− is the result of canonical transformation of
¬φ to LΠn1, resp., LΣn1 form.
For arithmetic formulas, let φ−:=¬φ.
Definition 15.1** (in L).**
We define a relation Tforcφ between trees T∈ST
and closed normal L-formulas:
- (I)
if φ is a closed L-formula, arithmetic or
in LΣ11∪LΠ11,
then Tforcφ iff φ[x] holds for all
x∈[T];
2. (II)
if φ:=∃xψ(x) is a closed
LΣn+11 formula, n≥1
(ψ being of type LΠn1),
then Tforcφ iff there is a code c∈CCF
such that Tforcψ(c);
3. (III)
if φ is a closed LΠn1 formula, n≥2,
then Tforcφ iff there is no tree S∈ST
such that S⊆T and Sforcψ−.
Let Forc(φ)={T∈ST:\linebreak[0]Tforcφ} and
Des(φ)=Forc(φ)∪Forc(φ−).
∎
Lemma 15.2** (in L).**
If m≥2 and φ is a closed formula in
LΣm1, resp., LΠm1, then the set
Forc(φ) belongs to Σm−1HC(HC),
resp., Πm−1HC(HC).
Proof**.**
For LΠ11 formulas, Definition 15.1(I)
implies Forc(φ)∈Π11,
thus Forc(φ) belongs to Δ1HC(HC).
Then argue by
induction on Definition 15.1(II),(III).
∎
Recall that a number n≥3 is fixed by
Definition 11.5.
Lemma 15.3** (in L).**
Let φ be a closed normal L-formula.
Then the set Des(φ) is dense in ST.
If φ is of type LΣm1,
m<n, then
Des(φ)∩P is dense in P.
Proof**.**
It suffices to establish the density of Des(φ)
for formulas φ as in (I).
If φ is such then the set
X(φ)={x∈T:\linebreak[0]φ[x]}
belongs to Σ11∪Π11, that is, it has the Baire
property inside [T].
Therefore at least one of the two complimentary sets
X(φ), X(φ−) is not meager in [T].
It remains to apply Corollary 5.4.
The second claim follows from the first one by lemmas
15.2 and 12.1(iv).
∎
16 Invariance
It happens that the relation forc is invariant under
two rather natural groups of transformations of ST.
Here we prove the invariance.
We still argue in L.
First group.
Let h⊆ω.
If x∈2ω then a real h⋅x∈2ω is defined
by (h⋅x)(j)=1−x(j) for j∈h, but
(h⋅x)(j)=x(j) for j∈/h.
If X⊆2ω then let h⋅X={h⋅x:\linebreak[0]x∈X}.
Accordingly, if s∈2<ω and n=lh(s) then a string
h⋅s∈2<ω is defined by
dom(h⋅s)=n=doms and if j<n then
(h⋅x)(j)=1−x(j) for j∈h, but
(h⋅x)(j)=x(j) for j∈/h.
If T⊆2<ω then let h⋅T={h⋅s:\linebreak[0]s∈T}.
Then obviously T∈ST iff h⋅T∈ST.
If f:2ω→2ω then a function h⋅f:2ω→2ω
is defined by (h⋅f)(x)=f(h⋅x),
equivalently, (h⋅f)(h⋅x)=f(x).
If f is continuous, then f=fc, where
c∈CCF, and there is a canonical definition of
a code h⋅c∈CCF such that
h⋅(fc)=fh⋅c.
Finally if φ:=φ(c1,…,ck) is a
L-formula then let hφ be the formula
φ(h⋅c1,…,h⋅ck).
Then
(hφ)[h⋅x] coincides with φ[x].
Second group.
Let IB be the set of all idempotent
bijections b:ω⟶ontoω, that is, we require
that b(j)=b−1(j), ∀j.
If x∈2ω then define b⋅x∈2ω by
(b⋅x)(j)=x(b(j)), ∀j.
Let b⋅X={b⋅x:\linebreak[0]x∈X}, for X⊆2ω.
If T∈ST then put
b⋅T={x↾m:\linebreak[0]x∈(b⋅[T])∧m<ω}.
Clearly T∈ST iff b⋅T∈ST.
If f:2ω→2ω then a function b⋅f:2ω→2ω
is defined similarly to the above
by (b⋅f)(x)=f(b⋅x),
equivalently, (b⋅f)(b⋅x)=f(x).
If f is continuous, then f=fc, where
c∈CCF, and still there is a canonical definition
of a code b⋅c∈CCF such that
b⋅(fc)=fb⋅c.
And finally if φ:=φ(c1,…,ck) is a
L-formula then let bφ be the formula
φ(b⋅c1,…,b⋅ck).
Then
(bφ)[b⋅x] coincides with φ[x].
Lemma 16.1** (in L).**
Let T∈ST and
φ be a closed normal L-formula.
Then
- (i)
if h⊆ω then
Tforcφ iff (h⋅T)forchφ;**
2. (ii)
if b∈IB then
Tforcφ iff (b⋅T)forcbφ.
Proof**.**
(i)
If φ is of type 15.1(I) then it
suffices to note that, first,
[h⋅T]={h⋅x:\linebreak[0]x∈[T]},
and second, if x∈[T] then φ[x] coincides with
(hφ)[h⋅x].
A routine induction based on
Definition 15.1(II),(III)
is left to the reader.
∎
Corollary 16.2**.**
Let
φ be a closed normal L-formula, such
that if a code c occurs in φ then
fc is a constant.
Assume that S,T∈ST and the splitting sets
spl(S), spl(T) (see Section 4)
are both co-infinite.
Then Sforcφ iff Tforcφ.
Proof**.**
Assume that Sforcφ.
As both spl(S) and spl(T) are co-infinite
(and they are infinite anyway), there is a bijection
b∈IB such that b”(spl(S))=spl(T).
Then the tree S′=b⋅S satisfies
spl(S′)=spl(T),
and still S′forcφ by Lemma 16.1(ii),
as all
occurring codes define constant functions, and hence
bφ and φ essentially coincide.
Now, as spl(S′)=spl(T),
there is a set h⊆ω∖spl(S′)=ω∖spl(T)
such that T=h⋅S′.
Then Tforcφ by Lemma 16.1(i) and the
constantness of the codes involved, as above.
∎
17 The final argument
Recall that n≥3 is fixed by Definition 11.5.
The last part of the proof of Theorem 1.1
will be Lemma 17.2.
Note the key ingredient of the proof:
we surprisingly approximate the
forcing P, definitely non-invariant under
the transformations considered in Section 16,
by the invariant relation forc, using
the next lemma.
Lemma 17.1**.**
Assume that 1≤n<n, φ∈L is a
closed formula in LΠn1∪LΣn+11, and a set
G⊆P is generic over L.
Then the sentence φ[a[G]] is true in L[G]
if and only if ∃T∈G(Tforcφ).
Proof**.**
Base of induction:
φ is arithmetic or belongs to LΣ11∪LΠ11,
as in 15.1(I).
If T∈G and Tforcφ, then φ[a[G]]
holds by the Shoenfield absoluteness theorem, as
a[G]∈[T].
The inverse holds by Lemma 15.3.
Step LΠn1⟹LΣn+11.
Let φ be ∃xψ(x) where ψ
is of type LΠn1.
Assume that T∈G and Tforcφ.
Then by Definition 15.1(II)
there is a code c∈CCF∩L such that
Tforcψ(c).
By the inductive hypothesis,
the formula ψ(c)[a[G]], that is,
ψ[G](fc(a[G])), is true in L[G].
But then φ[a[G]] is obviously true as well.
Conversely assume that φ[a[G]] is true.
Then there is a real y∈L[G]∩2ω such that
ψ[G](y) is true.
By Lemma 13.1,
y=fc(a[G]) for a code c∈CCF∩L.
But then ψ(c)[a[G]] is true in L[G].
By the inductive hypothesis, there is a tree T∈G
satisfying Tforcψ(c).
Then Tforcφ as well.
Step LΣn1⟹LΠn1.
Let φ be a LΠn1 formula, n≥2.
By Lemma 15.3, there is a tree T∈G
such that either Tforcφ or Tforcφ−.
If Tforcφ− then φ−[a[G]] is true by
the inductive hypothesis, hence φ[a[G]] is false.
Now assume that Tforcφ.
We have to prove that φ[a[G]] is true.
Suppose otherwise.
Then φ−[a[G]] is true.
By the inductive hypothesis, there is a tree
S∈G such that Sforcφ−.
But the trees S,T belong to the same generic set
G, hence they are compatible, which leads to a
contradiction with the assumption Tforcφ,
according to Definition 15.1(III).
∎
Lemma 17.2**.**
If a set
G⊆P is P-generic over L,
then it is true in L[G], that every countable
Σn1 set X⊆2ω satisfies Y∈L.
Proof**.**
We work in the context of Definition 11.5.
The first part of the proof is to show that Y⊆L.
Suppose to the contrary that it holds in L[G]
that Y⊆2ω is a countable Σn1 set,
but Y⊆L.
We have Y={y∈2ω:\linebreak[0]φ(y)} where
φ(y):=∃zψ(y,z)
is a Σn1 formula, that is, LΣn1 formula
without codes in CCF.
There is a tree T0∈G which P-forces that
“{y∈2ω:\linebreak[0]φ(y)} is a countable set and
∃y(φ(y)∧y∈/L)”.
Our goal is to derive a contradiction.
By Lemma 13.1,
there exist codes c,d∈CCF∩L such that the real
y0=c[G]=fc(a[G]) belongs to Y, so that
y0∈/L and
φ(c)[a[G]] holds, that is, ∃zψ(c,z)[a[G]],
and finally d witnesses the existence quantifier, so that
the sentence ψ(c,d)[a[G]] holds in L[G].
By Lemma 17.1 as ψ is a LΠn−11 formula,
there is a tree T1∈G satisfying
T1forcψ(c,d).
We can wlog assume that T1⊆T0 and that,
in L, the map fc is either a constant or a
bijection on [T1], by Lemma 12.1(v).
Case 1: fc↾[T1] is a constant, that is,
there exists a real y1∈2ω∩L such that
fc(x)=y1 for all x∈[T1].
But then y1=fc(a[G])=y0, however y0∈/L
while y1∈L, which is a contradiction.
Case 2: fc↾[T1] is a bijection.
As T1 is a Silver tree, the set
H=spl(T1)⊆ω of all its splitting levels
is infinite (Definition 4.1).
Let h∈L, h⊆H.
Then h⋅T1=T1, and we have
T1forcψ(h⋅c,h⋅d)
By Lemma 16.1.
Therefore the formula ψ(h⋅c,h⋅d)[a[G]]
is true in L[G] by Lemma 17.1.
But this formula coincides with
ψ(fh⋅c(a[G]),fh⋅d(a[D])),
hence we have
φ(fh⋅c(a[G])) in L[G].
This implies
fh⋅c(a[G])∈Y, or equivalently,
fc(h⋅a[G])∈Y.
However if sets h,h′∈L, h∪h′⊆H,
satisfy h=h′ then h⋅a[G]=h′⋅a[G],
and hence fc(h⋅a[G])=fc(h′⋅a[G]),
as fc is a bijection on [T1]
(and a[G]∈[T1]).
Thus picking different sets h∈L∩P(H) we get
uncountably many different elements of the set Y in
L[G], which contradicts to the choice of Y.
The proof of Y⊆L is accomplished.
To prove Y∈L, a stronger statement, it suffices
now to show that if y0∈2ω∩L then
y0∈Y iff ∃T∈ST(Tforcφ(c0)), where
c0∈CCF∩L is the code of the constant
function fc0(x)=y0, ∀x∈2ω.
If y0∈Y then the formula φ(y0), equal
to φ(c0)[x] for any x, is true in L[G]
by the choice of φ.
It follows by Lemma 17.1 that there is a tree
T∈G satisfying Tforcφ(c0), as required.
Now suppose that T∈ST
(not necessarily ∈P!)
and Tforcφ(c0).
As the set
D={T∈ST:\linebreak[0]spl(T) is co-infinite}
(see Lemma 12.1(vi))
is open dense in ST,
we can assume that spl(T) is co-infinite.
On the other hand, it follows from
Lemma 12.1(vi) that there is a
tree S∈G∩D,
so that spl(S) is co-infinite as well.
Now we have Sforcφ(c0) by Corollary 16.2,
and then φ(c0)[a[G]] is true in L[G]
by Lemma 17.1, that is, φ(y0) holds
in L[G], and y0∈Y, as required.
∎
Proof** **(Theorem 1.1, the main theorem).
We assert that any P-generic extension
L[G]=L[a[G]]
satisfies conditions (i), (ii), (iii)
of the theorem.
That a[G]∈/OD in (i) follows
by Lemma 13.2.
The minimality follows from Lemma 12.1(v)
by Lemma 13.1 (continuous reading of names).
We further have (ii) by Corollary 14.3,
and we have (iii) by Lemma 17.2.
∎
Index
-
action
-
b⋅c §16
-
bφ §16
-
h⋅c §16
-
h⋅s §16
-
h⋅T §16
-
h⋅X §16
-
h⋅x §16
-
hφ §16
-
s⋅T §4
-
s⋅t §4
-
s⋅X §4
-
s⋅x §4
-
blocks Definition 11.3
-
negatively Definition 11.3
-
positively Definition 11.3
-
code, code(f) §7
-
collage Definition 6.5
-
definability classes
-
ΣnHC,ΠnHC,ΔnHC §11
-
ΣnHC(HC),ΠnHC(HC) item (ii)
-
equivalence relation
-
[x]E0, E0-class §14
-
E0 §1
-
Vitali, VIT §2
-
forcing
-
by Silver trees Definition 6.1
-
Cohen forcing, Pcoh Example 6.3
-
extension, ⊏ §8
-
Jensen’s forcing, J §1
-
invariant, Jinv §1
-
M-extension, ⊏M Definition 8.1
-
Silver forcing, ST Example 6.3
-
ST-forcing Definition 6.1
-
STF §11
-
P Definition 11.5
-
formula
-
arithmetic §15
-
language L §15
-
LΣn1, LΠn1 §15
-
normal §15
-
φ− §15
-
φ[x] §15
-
function
-
code, code(f) §7
-
regular Definition 7.1
-
generic real
-
a[G] Remark 6.2
-
hereditarily countable
-
HC §11
-
map
-
regular Definition 7.1
-
M-extension, ⊏M Definition 8.1
-
model
-
Mα Definition 11.5
-
M(P) §11
-
number n≥3 Definition 11.5
-
regular Definition 7.1
-
splitting §5
-
T(→i) §5
-
T(→s) §5
-
stem, stem(T) Definition 4.1
-
string §4
-
2<ω, dyadic strings §4
-
2n, strings of length n §4
-
extension, ⊆, ⊂ §4
-
length §4
-
uk(T) Definition 4.1
-
Λ, the empty string §4
-
support
-
∣φ∣ Definition 9.1
-
system Definition 9.1
-
∣φ∣ Definition 9.1
-
extension, ψ≼φ §9
-
Sys(P) Definition 9.1
-
Tξmφ(n) Definition 9.1
-
Tξmφ(s) Definition 9.1
-
νξmφ Definition 9.1
-
τξmφ Definition 9.1
-
theory
-
ZFC′ §8
-
tree
-
branch Definition 4.1
-
restricted T↾u Definition 4.1
-
Silver, ST Definition 4.1
-
stem, stem(T) Definition 4.1
-
B[s] Example 4.2
-
TξmΦ(n) Definition 9.3
-
Tξmφ(n) Definition 9.1
-
TξmΦ(s) Definition 9.3
-
Tξmφ(s) Definition 9.1
-
UξmΦ Definition 9.3
-
2<ω §4
-
a[G], generic real Remark 6.2
-
B[s] Example 4.2
-
code(f) §7
-
Colgn(P) Definition 6.5
-
E0 §1
-
φ− §15
-
∣φ∣ Definition 9.1
-
φ[x] §15
-
HC §11
-
J §1
-
Jinv §1
-
Λ, the empty string §4
-
lh(s), length §4
-
LΠn1 §15
-
LΣn1 §15
-
Mα Definition 11.5
-
M(P) §11
-
Sys(P) Definition 9.1
-
n≥3 Definition 11.5
-
νξmφ Definition 9.1
-
Pcoh Example 6.3
-
P Definition 11.5
-
s[u] Proof
-
ΣnHC,ΠnHC,ΔnHC §11
-
ΣnHC(HC),ΠnHC(HC) item (ii)
-
spln(T) Definition 4.1
-
spl(T) Definition 4.1
-
⊆fin item (B)
-
⊏ Definition 8.1
-
⊏M Definition 8.1
-
S⊆nT §5
-
stem(T) Definition 4.1
-
STF §11
-
s⊆t §4
-
s⊂t §4
-
⊆n §5
-
T(→i) §5
-
T(→s) §5
-
τξmφ Definition 9.1
-
TξmΦ(n) Definition 9.3
-
Tξmφ(n) Definition 9.1
-
TξmΦ(s) Definition 9.3
-
Tξmφ(s) Definition 9.1
-
[T] Definition 4.1
-
T↾u Definition 4.1
-
t⌢i §4
-
u[s] Proof
-
UξmΦ Definition 9.3
-
VIT §2
-
[x]E0 §14
-
ZFC′ §8