# Forcing the $\bf{\Sigma^{1}_{3}}$-Separation Property

Stefan Hoffelner111 WWU Münster. Research funded by thr Deutsche
Forschungsgemsinschaft (DFG German Research Foundation) under Germanys
Excellence Strategy EXC 2044 390685587, Mathematics Münster: Dynamics-
Geometry-Structure. The author was additionally partially supported by FWF-
GACR grant no. 17-33849L, Filters, ultrafilters and connections with forcing.
He thanks S. D. Friedman for several discussions on a related topic. He thanks
A. Lietz for discussions and several improvements, and F. Schlutzenberg, R.
Schindler and L. Wu for more discussions.

(26.12.2019)

###### Abstract

We generically construct a model in which the $\bf{\Sigma^{1}_{3}}$-separation
property is true, i.e. every pair of disjoint $\bf{\Sigma^{1}_{3}}$-sets can
be separated by a $\bf{\Delta^{1}_{3}}$-definable set. This answers an old
question from A. Mathias. We also construct a model in which the (lightface)
$\Sigma^{1}_{3}$-separation property is true.

##  1 Introduction

The separation property is a very old concept, introduced implicitly by Lusin
and Sierpinski in their proof of Suslin’s celebrated result on the equivalence
of Borel and boldface $\Delta^{1}_{1}$-definable sets. Given two disjoint sets
of reals $A_{1}$ and $A_{2}$, we say that a set $C$ separates $A_{1}$ and
$A_{2}$ iff $A_{1}\subset C$ and $A_{2}\subset C^{c}$. The problem becomes
interesting when considered through the lens of definability.

######  Definition 1.1.

We say that an adequate pointclass $\Gamma$ has the separation property iff
every pair $A_{1}$ and $A_{2}$ of disjoint elements $\Gamma$ has a separating
set $C\in\Gamma\cap\check{\Gamma}$, where $\check{\Gamma}$ denotes the dual
pointclass of $\Gamma$ .

It is a classical result that the pre-wellordering property for $\Gamma$
implies the reduction property for $\Gamma$, i.e. given two sets $A_{1}$ and
$A_{2}$ of $\Gamma$ there are disjoint sets $B_{1}\subset A_{1}$ and
$B_{2}\subset A_{2}$ both in $\Gamma$ such that $A_{1}\cup A_{2}=B_{1}\cup
B_{2}$. Again a well-known classical result then shows that for a $\Gamma$
with the reduction property, the dual $\check{\Gamma}$ has the separation
property (see e.g. [12], 4B 11). Consequentially, $\bf{\Sigma^{1}_{1}}$ and
$\bf{\Pi^{1}_{2}}$-sets have the separation property due to M. Kondo’s theorem
that $\bf{\Pi^{1}_{1}}$, hence also $\bf{\Sigma^{1}_{2}}$-sets are scaled,
thus have the pre-wellordering property. This is as much as $\mathsf{ZFC}$ can
prove about the separation property. In Gödel’s constructible universe $L$ the
$\bf{\Sigma^{1}_{3}}$-reduction property holds, so
$\bf{\Pi^{1}_{3}}$-separation holds. On the other hand, by the Y. Moschovakis
(see [13]), $\bf{\Delta^{1}_{2}}$-determinacy implies the
$\bf{\Pi^{1}_{3}}$-uniformization property, so
$\bf{\Sigma^{1}_{3}}$-separation holds. Recall here that
$\bf{\Delta^{1}_{2}}$-determinacy implies an inner model with a Woodin
cardinal. It is an old problem of A. Mathias whether one can get a model of
the $\bf{\Sigma^{1}_{3}}$-separation property from just assuming the
consistency of $\mathsf{ZFC}$, (see [11], Problem 3029). One can find in the
literature references to a major paper of L. Harrington in which the problem
is solved. This paper however, and its proofs never materialized (see [7] for
more details). We add that our proof seems to use different ideas than the
ones which Harrington relied on. After there was almost no progress made on
these questions since the mid 70’ies, problems related to the forcability of
certain implication of $\mathsf{PD}$ received more attention again, mostly due
to the efforts of V. Kanovei, who embarked on a detailed study of certain
related problems (see [6] and [7]) and resurrected old results by L.
Harrington. Goal of this paper is to show that the
$\bf{\Sigma^{1}_{3}}$-separation property has no large cardinal strength,
which answers Mathias question.

######  Theorem.

Starting with $L$ as the ground model, one can produce a set-generic extension
$L[G]$ which satisfies $\mathsf{CH}$ and in which the
$\bf{\Sigma^{1}_{3}}$-separation property holds.

The proof method also allows to tackle the $\Sigma^{1}_{3}$-separation
property:

######  Theorem.

Starting with $L$ as the ground model, one can produce a set-generic extension
$L[G]$ which satisfies $\mathsf{CH}$ and in which the
${\Sigma^{1}_{3}}$-separation property holds.

##  2 Preliminaries

###  2.1 The forcings which are used

The forcings which we will use in the construction are all well-known. We
nevertheless briefly introduce them and their main properties.

######  Definition 2.1.

For a stationary $S\subset\omega_{1}$ the club-shooting forcing with finite
conditions for $S$, denoted by $\mathbb{P}_{S}$ consists of conditions $p$
which are finite partial functions from $\omega_{1}$ to $S$ and for which
there exists a normal function $f:\omega_{1}\rightarrow\omega_{1}$ such that
$p\subset f$. $\mathbb{P}_{S}$ is ordered by end-extension.

The club shooting forcing $\mathbb{P}_{S}$ is the paradigmatic example for an
$S$-_proper forcing_ , where we say that $\mathbb{P}$ is $S$-proper if and
only if for every condition $p\in\mathbb{P}_{S}$, every sufficiently large
$\theta$ and every countable $M\prec H(\theta)$ such that $M\cap\omega_{1}\in
S$ and $p,\mathbb{P}_{S}\in M$, there is a $q<p$ which is
$(M,\mathbb{P}_{S})$-generic.

######  Lemma 2.2.

The club-shooting forcing $\mathbb{P}_{S}$ generically adds a club through the
stationary set $S\subset\omega_{1}$, while being $S$-proper and hence
$\omega_{1}$-preserving. Moreover stationary subsets $T$ of $S$ remain
stationary in the generic extension.

We will choose a family of $S_{\beta}$’s so that we can shoot an arbitrary
pattern of clubs through its elements such that this pattern can be read off
from the stationarity of the $S_{\beta}$’s in the generic extension. For that
it is crucial to recall that $S$-proper posets can be iterated with countable
support and always yield an $S$-proper forcing again. This is proved exactly
as in the well-known case for plain proper forcings (see [3], 3.19. for a
proof).

######  Fact 2.3.

Let $(\mathbb{P}_{\alpha},\dot{\mathbb{Q}}_{\alpha})$ be a countable support
iteration, assume also that at every stage $\alpha$,
$\Vdash_{\alpha}\dot{\mathbb{Q}}_{\alpha}$ is $S$-proper. The the iteration is
an $S$-proper notion of forcing again.

The following coding method has been used several times already (see [1]).

######  Lemma 2.4.

Let $r\in 2^{\omega_{1}}$ be arbitrary, and let $\mathbb{P}$ be a countable
support iteration $(\mathbb{P}_{\alpha},\dot{\mathbb{Q}}_{\alpha})$ of length
$\omega_{1}$, inductively defined via
$\dot{\mathbb{Q}}_{\alpha}:=\mathbb{P}_{\omega_{1}\backslash
S_{2\cdot\alpha}}$ if $r(\alpha)=1$ and
$\dot{\mathbb{Q}}_{\alpha}:=\mathbb{P}_{\omega_{1}\backslash
S_{(2\cdot\alpha)+1}}$ if $r(\alpha)=0$. Then in the resulting generic
extension $V^{\mathbb{P}}$, we have that
$\forall\alpha<\omega_{1}:\,r(\alpha)=1$ if and only if $S_{2\cdot\alpha}$ is
nonstationary, and $r_{\alpha}=0$ iff $S_{(2\cdot\alpha)+1}$ is nonstationary.

###### Proof.

Assume first that $r(\alpha)=1$ in $V^{\mathbb{P}}$. Then by definition of the
iteration we must have shot a club through the complement of $S_{\alpha}$,
thus it is nonstationary in $V^{\mathbb{P}}$.

On the other hand, if $S_{2\cdot\alpha}$ is nonstationary in $V^{\mathbb{P}}$,
then as for $\beta\neq 2\cdot\alpha$, every forcing of the form
$\mathbb{P}_{S_{\beta}}$ is $S_{2\cdot\alpha}$-proper, we can iterate with
countable support and preserve $S_{2\cdot\alpha}$-properness, thus the
stationarity of $S_{2\cdot\alpha}$. So if $S_{2\cdot\alpha}$ is nonstationary
in $V^{\mathbb{P}}$, we must have used $\mathbb{P}_{S_{2\cdot\alpha}}$ in the
iteration, so $r(\alpha)=1$.

∎

The second forcing we use is the almost disjoint coding forcing due to R.
Jensen and R. Solovay. We will identify subsets of $\omega$ with their
characteristic function and will use the word reals for elements of
$2^{\omega}$ and subsets of $\omega$ respectively. Let
$F=\\{f_{\alpha}\,\>\,\alpha<\aleph_{1}\\}$ be a family of almost disjoint
subsets of $\omega$, i.e. a family such that if $r,s\in F$ then $r\cap s$ is
finite. Let $X\subset\kappa$ for $\kappa\leq 2^{\aleph_{0}}$ be a set of
ordinals. Then there is a ccc forcing, the almost disjoint coding
$\mathbb{A}_{F}(X)$ which adds a new real $x$ which codes $X$ relative to the
family $F$ in the following way

$\alpha\in X\text{ if and only if }x\cap f_{\alpha}\text{ is finite.}$

######  Definition 2.5.

The almost disjoint coding $\mathbb{A}_{F}(X)$ relative to an almost disjoint
family $F$ consists of conditions $(r,R)\in\omega^{<\omega}\times F^{<\omega}$
and $(s,S)<(r,R)$ holds if and only if

  1. 1.

$r\subset s$ and $R\subset S$.

  2. 2.

If $\alpha\in X$ and $f_{\alpha}\in R$ then $r\cap f_{\alpha}=s\cap
f_{\alpha}$.

For the rest of this paper we let $F\in L$ be the definable almost disjoint
family of reals one obtains when recursively adding the $<_{L}$-least real to
the family which is almost disjoint from all the previously picked reals.
Whenever we use almost disjoint coding forcing, we assume that we code
relative to this fixed almost disjoint family $F$.

The last two forcings we briefly discuss are Jech’s forcing for adding a
Suslin tree with countable conditions and, given a Suslin tree $T$, the
associated forcing which adds a cofinal branch through $T$. Recall that a set
theoretic tree $(T,<)$ is a Suslin tree if it is a normal tree of height
$\omega_{1}$ and has no uncountable antichain. As a result, forcing with a
Suslin tree $S$, where conditions are just nodes in $S$, and which we always
denote with $S$ again, is a ccc forcing of size $\aleph_{1}$. Jech’s forcing
to generically add a Suslin tree is defined as follows.

######  Definition 2.6.

Let $\mathbb{P}_{J}$ be the forcing whose conditions are countable, normal
trees ordered by end-extension, i.e. $T_{1}<T_{2}$ if and only if
$\exists\alpha<\text{height}(T_{1})\,T_{2}=\\{t\upharpoonright\alpha\,:\,t\in
T_{1}\\}$

It is wellknown that $\mathbb{P}_{J}$ is $\sigma$-closed and adds a Suslin
tree. In fact more is true, the generically added tree $T$ has the additional
property that for any Suslin tree $S$ in the ground model $S\times T$ will be
a Suslin tree in $V[G]$. This can be used to obtain a robust coding method
(see also [4] for more applications)

######  Lemma 2.7.

Let $V$ be a universe and let $S\in V$ be a Suslin tree. If $\mathbb{P}_{J}$
is Jech’s forcing for adding a Suslin tree and if $T$ is the generic tree then

$V[T]\models T\times S\text{ is Suslin.}$

###### Proof.

Let $\dot{T}$ be the $\mathbb{P}_{J}$-name for the generic Suslin tree. We
claim that $\mathbb{P}_{J}\ast\dot{T}$ has a dense subset which is
$\sigma$-closed. As $\sigma$-closed forcings will always preserve ground model
Suslin trees, this is sufficient. To see why the claim is true consider the
following set:

$\\{(p,\check{q})\,:\,p\in\mathbb{P}_{J}\land
height(p)=\alpha+1\land\check{q}\text{ is a node of $p$ of level }\alpha\\}.$

It is easy to check that this set is dense and $\sigma$-closed in
$\mathbb{P}_{J}\ast\dot{T}$.

∎

A similar observation shows that a we can add an $\omega_{1}$-sequence of such
Suslin trees with a countably supported iteration.

######  Lemma 2.8.

Let $S$ be a Suslin tree in $V$ and let $\mathbb{P}$ be a countably supported
product of length $\omega_{1}$ of forcings $\mathbb{P}_{J}$. Then in the
generic extension $V[G]$ there is an $\omega_{1}$-sequence of Suslin trees
$\vec{T}=(T_{\alpha}\,:\,\alpha\in\omega_{1})$ such that for any finite
$e\subset\omega$ the tree $S\times\prod_{i\in e}T_{i}$ will be a Suslin tree
in $V[\vec{T}]$.

These sequences of Suslin trees will be used for coding in our proof and get a
name.

######  Definition 2.9.

Let $\vec{T}=(T_{\alpha}\,:\,\alpha<\kappa)$ be a sequence of Suslin trees. We
say that the sequence is an independent family of Suslin trees if for every
finite set $e=\\{e_{0},e_{1},...,e_{n}\\}\subset\kappa$ the product
$T_{e_{0}}\times T_{e_{1}}\times\cdot\cdot\cdot\times T_{e_{n}}$ is a Suslin
tree again.

##  3 A first step towards the proof of the boldface separation property

###  3.1 Rough idea of the proof

We proceed via proving first the following theorem which is the main step in
proving the result of the article.

######  Theorem 3.1.

There is a generic extension $L[G]$ of $L$ in which there is a countable
ordinal $\alpha_{0}$ such that every pair of disjoint (ligthface)
$\Sigma^{1}_{3}$-sets can be separated by a
$\Delta^{1}_{3}(\alpha_{0})$-formula.

The proof of the theorem will serve as an easier blueprint for the proof of
the main result.

For its proof, we will use the two easily definable $\omega_{1}$-sequences of
Suslin trees on $\omega_{1}$, $\vec{S}=\vec{S}^{1}\cup\vec{S}^{2}$ and branch
shooting forcings to create for every pair $(A_{m},A_{k})$ of disjoint
$\Sigma^{1}_{3}$-definable sets of reals a
$\Delta_{3}^{1}(\alpha_{0})$-definable separating set $D_{m,k}\supset A_{m}$.
Using a bookkeeping function we list all the reals $x$ and decide for every
such real whether we put it into $D_{m,k}$ or its complement $D_{m,k}^{c}$.
Elements of $D_{m,k}$ will be coded into $\omega$-blocks on the
$\vec{S}^{1}$-sequence whereas elements of the complement $D_{m,k}^{c}$ will
be coded into $\omega$-blocks on the $\vec{S}^{2}$-sequence. Using coding
arguments the sets $D_{m,k}$ and its complement will be
$\Sigma^{1}_{3}(\alpha_{0})$-definable. The fact that we have to decide at
every stage where to put the current real $x$ before the iteration is actually
finished seems to be somewhat daring as the evaluation of the $\Pi^{1}_{3}$
and $\Sigma^{1}_{3}$-sets vary as we generically enlarge our surrounding
universe along the iteration. Additionally one has to deal with possible
degenerated cases which stem from a certain amount of self referentiality in
the way we set up things. Indeed it could happen that forcing a real $x$ into
one side, $D_{m,k}$ say, could force simultaneously that $x$ will become a
member of $A_{k}$ in the generic extension, thus preventing $D_{m,k}$ to
actually separated $A_{m}$ and $A_{k}$. A careful case distinction will show
that this problem can be overcome though.

###  3.2 The ground model $W$ of the iteration

We have to first create a suitable ground model $W$ over which the actual
iteration will take place. $W$ will be a generic extension of $L$, satisfying
$\mathsf{CH}$ and, as stated already earlier, has the property that it
contains two $\omega_{1}$-sequence $\vec{S}=\vec{S^{1}}\cup\vec{S^{2}}$ of
independent Suslin trees.

To achieve this we start with Gödels constructible universe $L$ as our ground
model. Next we fix an appropriate sequence of stationary subsets of
$\omega_{1}$. Recall that $\diamondsuit$ holds in our ground model $L$, i.e.
there is a $\Sigma_{1}$-definable sequence
$(a_{\alpha}\,:\,\alpha<\omega_{1})$ of countable subsets of $\omega_{1}$ such
that any set $A\subset\omega_{1}$ is guessed stationarily often by the
$a_{\alpha}$’s, i.e. $\\{\alpha<\omega_{1}\,:\,a_{\alpha}=A\cap\alpha\\}$ is a
stationary subset of $\omega_{1}$. The $\diamondsuit$-sequence can be used to
produce an easily definable sequence of stationary subsets: we list the reals
in $L$ in an $\omega_{1}$ sequence $(r_{\alpha}\,:\,\alpha<\omega_{1})$ and
define for every $\beta<\omega_{1}$ a stationary set in the following way:

$R_{\beta}:=\\{\alpha<\omega_{1}\,:\,a_{\alpha}=r_{\beta}\\}.$

These stationary sets will be used to define our separating sets which will
witness the $\Sigma^{1}_{3}$-separation property. We definably split the
sequence

$\vec{R}=(R_{\beta}\,:\,\beta<\omega_{1})$

into two, we let

$\vec{R}^{1}:=Even(\vec{R})=(R^{1}_{\omega\cdot\alpha+2n}\,:\,\alpha<\omega_{1},n\in\omega)$

be the sequence of the even entries in $\vec{R}$ and

$\vec{R}^{2}:=Odd(\vec{R})=(R^{2}_{\omega\cdot\alpha+2n+1}\,:\,\alpha<\omega_{1},n\in\omega)$

be the sequence of the odd entries.

Frist we add $\aleph_{1}$-many $\aleph_{0}$-sized blocks of Suslin trees with
a countably supported product of Jech’s Forcing $\mathbb{C}(\omega_{1})$. We
let $\mathbb{R}_{0,\alpha}:=\prod_{n\in\omega}\mathbb{C}(\omega_{1})$, and let
$\mathbb{R}_{0}=\prod_{\alpha<\omega_{1}}\mathbb{R}_{0,\alpha}$. This is a
$\sigma$-closed, hence proper notion of forcing. We denote the generic filter
of $\mathbb{R}_{0}$ with
$\vec{S}=(S_{\omega\cdot\alpha+n}\,:\,\alpha<\omega_{1},n\in\omega)$ and note
that whenever $I\subset\omega_{1}$ is a set of indices then for every $j\notin
I$, the Suslin tree $S_{j}$ will remain a Suslin tree in the universe
$L[\vec{S}][g]$, where $g\subset\prod_{i\in I}S_{i}$ denotes the generic
filter for the forcing with the finitely supported product of the trees
$S_{i}$, $i\in I$ (see [4] for a proof of this fact). We fix a definable
bijection between $[\omega_{1}]^{\omega}$ and $\omega_{1}$ and identify the
trees in $(S_{\omega\cdot\alpha+n}\,:\,\alpha<\omega,n\in\omega)$ with their
images under this bijection, so the trees will always be subsets of
$\omega_{1}$ from now on. Further we partition the
$\omega\cdot\omega_{1}$-sequence of Suslin trees into the odd and even members
and let

$\vec{S^{1}}:=Even(\vec{S})$

and

$\vec{S^{2}}:=Odd(\vec{S})$

In a second step we code the even and the odd trees into the according
sequence of the even and odd definable $L$-stationary subsets $\vec{R^{1}}$
and $\vec{R^{2}}$ we produced earlier, using club shooting forcing. We will
just describe the method for one sequence
$(S_{\omega\cdot\alpha+n}\,:\,\alpha<\omega_{1},n\in\omega_{1})$, to not write
everything twice for the even and the odd sequence.

The forcing used in the second step will be denoted by $\mathbb{R}_{1}$. Fix
$\alpha<\omega_{1}$ and $n\in\omega$ and consider the Suslin tree
$S_{\omega\cdot\alpha+n}$. We let $\mathbb{R}_{1,\alpha,n}$ be the countable
support product which codes $S_{\omega\cdot\alpha+n}$ into the
$\omega\cdot\alpha+n$-th $\omega_{1}$-block of the
$\omega_{1}\cdot\omega_{1}$-sequence of the $R_{\beta}$’s. So

$\mathbb{R}_{1,\alpha,\beta}=\prod_{\gamma\in
S_{\omega\cdot\alpha+n}}\mathbb{P}_{R_{\omega_{1}\cdot(\omega\cdot\alpha+n)+2\cdot\gamma}}\times\prod_{\gamma\notin
S_{\omega\cdot\alpha+n}}\mathbb{P}_{\omega_{1}\backslash
R_{\omega_{1}\cdot(\omega\cdot\alpha+n)+2\cdot\gamma+1}}$

If we let $R$ be some stationary subset of $\omega_{1}$ which is disjoint from
all the $R_{\alpha}$’s, e.g.
$R=\\{\alpha<\omega_{1}\,:\,a_{\alpha}=\\{\omega\\}\\}$, then it is obvious
that for every $\alpha<\omega_{1}$ and every $n\in\omega$,
$\mathbb{R}_{1,\alpha,\beta}$ is an $R$-proper forcing which additionally is
$\omega$-distributive. Then we let $\mathbb{R}_{1}$ be the countably supported
iteration,

$\mathbb{R}_{1}:=\bigstar_{\alpha<\omega_{1},n\in\omega_{1}}\mathbb{R}_{1,\alpha,n}$

which is again $R$-proper and $\omega$-distributive. This way we can turn the
generically added sequence of Suslin trees $\vec{S}$ into a definable sequence
of Suslin trees. Now we apply this method to code up both, the even and the
odd sequence $\vec{S^{1}}$ and $\vec{S^{2}}$ into patterns of non-stationary
elements of $\vec{R^{1}}$ and $\vec{R^{2}}$.

Let $\mathbb{R}_{1}$ now be this coding forcing, so $\mathbb{R}_{1}$ consists
of two copies, one for $\vec{S^{1}}$ and one for $\vec{S^{2}}$, of the forcing
we denoted with $\mathbb{R}_{1}$ above. If $H$ denotes the generic filter for
$\mathbb{R}_{1}$ over $L[\vec{S}]$ then we obtain that in $L[\vec{S}][H]$,
every element $S_{i}\in\vec{S^{1}}$ is $\Sigma_{1}$-definable over
$H(\omega_{2})$ with parameter $\omega_{1}$ using the definable sequence of
the even $L$-stationary subsets
$\vec{R^{1}}=(R^{1}_{\alpha}\,:\,\alpha<\omega_{1})$.

  * $(\ast)$

$S\in\vec{S^{1}}$ if and only if there is an $\alpha<\omega_{1}$ and a
$n<\omega$ such that $\forall\gamma\in\omega_{1}(\gamma\in S$ iff
$R^{1}_{\omega_{1}\cdot(\omega\cdot\alpha+n)+2\gamma}$ is nonstationary and
$\gamma\notin S$ iff $R^{1}_{\omega_{1}\cdot(\omega\cdot\alpha+n)+2\gamma+1}$
is nonstationary).

Likewise elements of $\vec{S^{2}}$ do have a
$\Sigma_{1}(\omega_{1})$-definition using the elements of $\vec{R^{2}}$. Note
that this formula is indeed equivalent to a $\Sigma_{1}(\omega_{1})$ formula,
as already transitive, $\aleph_{1}$-sized models of $\mathsf{ZF}^{-}$ are
sufficient to witness the truth of the statement above.

The Suslin trees from $\vec{S}$ will be used later to code information via
destroying certain patterns of elements of $\vec{S}$. Thus it is crucial that
elements from $\vec{S}$ are preserved in the process of making them definable
using $\mathbb{R}_{1}$. This is indeed the case as is shown in [4], Lemma 35.

######  Lemma 3.2.

The forcing $\mathbb{R}_{1}$, defined above preserves Suslin trees.

In a third step we will add reals which will turn the
$\Sigma_{1}(\omega_{1})$-definition of $\vec{S^{1}}$ and $\vec{S^{2}}$ into
$\Sigma^{1}_{3}$-properties using David’s trick. We only argue again for
elements $S\in\vec{S^{1}}$. For elements of $\vec{S^{2}}$ the situation is
exactly the same. First we note that for every $\alpha<\omega_{1}$ and
$n\in\omega$, there is a set $X^{1}_{\alpha,n}\subset\omega_{1}$ which codes
all the clubs which are sufficient to witness the right hand side of $(\ast)$
above. Consequentially any transitive model $M$ of a sufficiently strong,
finite fragment of $\mathsf{ZFC}$ which contains $X^{1}_{\alpha,n}$ can
correctly compute the tree $S^{1}_{\omega\cdot\alpha+n}$.

We define $Y^{1}_{\alpha,n}\subset\omega_{1}$ such that the odd entries code
the $X^{1}_{\alpha,n}$ and the enumeration $(y_{\beta}\,:\,\beta<\omega_{1})$
of the even entries $E(Y^{1}_{\alpha,n})$ of $Y^{1}_{\alpha,n}$ satisfies:

  1. 1.

$E(Y^{1}_{\alpha,n})\cap\omega$ codes a well-ordering of type $y_{0}$.

  2. 2.

$E(Y^{1}_{\alpha,n})\cap[\omega,y_{0})=\emptyset$.

  3. 3.

For all $\beta$, $E(Y^{1}_{\alpha,n})\cap[y_{\beta},y_{\beta}+\omega)$ codes a
well-ordering of type $y_{\beta+1}$.

  4. 4.

For all $\beta$,
$E(Y^{1}_{\alpha,n})\cap[y_{\beta}+\omega,y_{\beta+1})=\emptyset$.

In the next step we use almost disjoint forcing $\mathbb{A}_{F}(Y_{\alpha,n})$
relative to the canonical almost disjoint family of $L$-reals $F$, i.e. the
family $F$ one obtains when inductively picking the $<_{L}$-least real which
is almost disjoint to all the reals picked before, to code the set
$Y^{1}_{\alpha,n}$ into one real $r_{\alpha,n}$. Membership in
$S^{1}_{\omega\cdot\alpha+n}$ is a then $\Pi^{1}_{2}(r_{\alpha,n})$-property.

######  Lemma 3.3.

Let $r_{\alpha,n}$ be as defined above. Then

$\displaystyle\forall\gamma<\omega_{1}(\gamma\in
S^{1}_{\omega\cdot\alpha+n}\Leftrightarrow\forall M($ $\displaystyle
M\models\mathsf{ZF}^{-}\land|M|=\aleph_{0}\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\land$
$\displaystyle r_{\alpha,n},\gamma\in M\rightarrow M\text{ thinks that its
version of }$ $\displaystyle
R^{1}_{\omega_{1}\cdot(\omega\cdot\alpha+n)+2\gamma}\text{ is
nonstationary})).$

Now as the third an last step in our preparatory forcing, collect all sets of
the form $X_{\alpha,n}^{i}$, $i\in 2,\alpha<\omega_{1},n\in\omega$, then form
for each such $X_{\alpha,n}^{i}$ the according $Y_{\alpha,n}^{i}$ and let the
forcing be the finitely supported product

$\mathbb{R}_{2}:=\prod_{\alpha,n,i}\mathbb{A}_{F}(Y_{\alpha,n}^{i}).$

This is again a ccc forcing and will turn every tree
$S_{\omega\cdot\alpha+n}^{i}$ into a $\Sigma^{1}_{3}$-definable Suslin tree.
Note here that the forcing $\mathbb{R}_{2}$ has the Knaster property as the
product preserves being Knaster, thus the Suslin trees in $\vec{S^{1}}$ and
$\vec{S^{2}}$ are not destroyed. Indeed if there would be an $S\in\vec{S^{1}}$
say such that $\mathbb{R}_{2}\Vdash$ “$S$ is not Suslin$"$, then
$\mathbb{R}_{2}\times S=S\times\mathbb{R}_{2}$ is not ccc, which is a
contradiction to $\mathbb{R}_{2}$ being Knaster.

Let us set $W:=L[\mathbb{R}_{0}\ast\mathbb{R}_{1}\ast\mathbb{R}_{2}]$ which
will serve as our ground model for a second iteration of length $\omega_{1}$.
Note that $W$ satisfies $\mathsf{CH}$. The forcing which we will use to form
the desired model of the $\bf{\Sigma^{1}_{3}}$-separation property will be an
iteration consisting only of two types of forcings, shooting branches through
elements of $\vec{S}=\vec{S^{1}}\cup\vec{S^{2}}$ and using almost disjoint
coding $\mathbb{A}(F)$ relative to $F$ to code up $\omega$-blocks of such
genrically added branches. If $S$ is a Suslin tree we will denote the forcing
with the tree again with $S$. It is convenient to give the type of iterations
we are about to use a name.

######  Definition 3.4.

An iteration
$\mathbb{P}=(\mathbb{P}_{\delta},\mathbb{P}(\delta))_{\delta<\gamma}$ with
finite support of length $\gamma<\omega_{1}$ consisting entirely of factors of
the form $\mathbb{A}_{F}(X)$, $X\subset\omega_{1}$ and $S$ for
$S\in\vec{S}^{1}\cup\vec{S}^{2}$ is called a legal forcing if every element of
$\vec{S}$ is used at most once and it additionally satisfies that the
iteration has the form that alternately $\omega$-blocks of elements of
$\vec{S^{1}}$ or $\vec{S^{2}}$ are destroyed and then almost disjoint reals
are added, which code the added branches.

The iteration we are about to define will be a legal one. Note that both, the
Suslin tree forcing as well as the almost disjoint coding forcing consist of
conditions which are always elements of $W$, which guarantees some
absoluteness for its definition is independent of the universe in which they
are considered.

We will use the trees in $\vec{S}$ to code up information. Hence we need some
result which guarantees us that whenever we destroy certain elements of
$\vec{S}$, we will not accidentally destroy other elements of $\vec{S}$, hence
ruining our coding. This is the purpose of the next lemma.

######  Lemma 3.5.

Let $\mathbb{P}$ be a legal forcing over $W$ and let $S\in\vec{S}$ be a Suslin
tree which does not show up as one of the factors of $\mathbb{P}$. Then $S$
remains Suslin in $W[\mathbb{P}]$. In particular every legal iteration has the
ccc.

###### Proof.

We use induction on the length of the iteration $\mathbb{P}$. For the
successor case, assume the lemma is true for $\alpha$ and assume first that
$\mathbb{P}=\mathbb{P}^{\prime}\ast S^{\prime}$ is a legal iteration of length
$\alpha+1$, where $S^{\prime}$ is some Suslin tree from $\vec{S}$ and
$\mathbb{P}^{\prime}$ is a legal iteration of length $\alpha$. The iteration
$\mathbb{P}^{\prime}\ast(S^{\prime}\ast S)$ can be written as
$\mathbb{P}^{\prime}\times(S^{\prime}\times S)$ and the second factor is by
the independence of $\vec{S}$ a Suslin tree which does not show up in
$\mathbb{P}^{\prime}$. By induction hypothesis $S^{\prime}\times S$ remains
Suslin in $W[\mathbb{P}^{\prime}]$, so $S$ is Suslin in
$W[\mathbb{P}^{\prime}\ast S^{\prime}]$.

If $\mathbb{P}=\mathbb{P}^{\prime}\ast\mathbb{A}_{F}(Y)$ for some
$Y\subset\omega_{1}$, then $\mathbb{P}\ast S$ can be written as
$\mathbb{P}^{\prime}\ast(\mathbb{A}_{F}(Y)\times S)=\mathbb{P}^{\prime}\ast
S\ast\mathbb{A}_{F}(Y)$. Now if $S$ would not be Suslin in $W[\mathbb{P}]$,
$\mathbb{P}\ast S$ is not ccc, however $S$ remains Suslin in
$W[\mathbb{P}^{\prime}]$ and as $\mathbb{A}_{F}(Y)$ is Knaster it will remain
Suslin in $W[\mathbb{P}^{\prime}\ast\mathbb{A}_{F}(Y)]$. So
$\mathbb{P}^{\prime}\ast\mathbb{A}_{F}(Y)\ast S=\mathbb{P}^{\prime}\ast
S\ast\mathbb{A}_{F}(Y)$ is a ccc forcing which is a contradiction.

The case where $\mathbb{P}$ is a legal iteration of length $\alpha\in Lim$ is
shown as follows. Suppose that $S$ is not Suslin in $W[\mathbb{P}]$, then
$\mathbb{P}\ast S$ is not ccc, but $\mathbb{P}\ast S=S\times\mathbb{P}$ and by
the independence of $\vec{S}$, every Suslin tree used in $\mathbb{P}$ is still
a Suslin tree in $W[S]$. So $\mathbb{P}$ is a legal iteration of length
$\alpha$ in $W[S]$ and hence ccc by assumption which is a contradiction. ∎

###  3.3 Definition of the iteration over $W$

For $n\in\omega$ let $\varphi_{n}(v_{0})=\exists v_{1}\psi_{n}(v_{0},v_{1})$
be the $n$-th formula in an enumeration of the $\Sigma^{1}_{3}$-formulas with
one free variables. Let $A_{n}$ denote the $\Sigma^{1}_{3}$-set corresponding
to $\varphi_{n}(v_{0})$. We force with an $\omega_{1}$-length finite support
iteration legal forcings which all have size $\aleph_{1}$, and use a
definable, surjective bookkeeping-function
$F:\omega_{1}\rightarrow\omega_{1}\times\omega_{1}\times\omega\times\omega$ to
determine the iteration. We demand that every $\alpha<\omega_{1}$ is always
strictly bigger than the first projection of $F(\alpha)$. We also assume that
every quadruple $(\beta,\gamma,m,k)$ in
$\omega_{1}\times\omega_{1}\times\omega\times\omega$ is hit unboundedly often
by $F$.

Our goal is to find for every pair $(n,m)$ which corresponds to two disjoint
$\Sigma^{1}_{3}$-sets $A_{n}$ and $A_{m}$ a
$\Delta^{1}_{3}(\alpha_{0})$-definable set $D_{n,m}$ such that $A_{n}\subset
D_{n,m}$ and $A_{m}\subset D_{n,m}^{c}$, where $\alpha_{0}$ is a countable
ordinal which will serve as a parameter. We will use our two definable
sequences $\vec{S}^{1}$ and $\vec{S}^{2}$ to achieve this.

Assume that we are at some stage $\alpha<\omega_{1}$ of our iteration, let
$\mathbb{P}_{\alpha}$ denote the partial order we have defined so far, let
$G_{\alpha}$ denote a generic filter for $\mathbb{P}_{\alpha}$. Our goal is to
define the next forcing $\dot{\mathbb{Q}}_{\alpha}$ which we shall use. As
will become clear after finishing the definition of the iteration, we can
assume that $\mathbb{P}_{\alpha}$ is a legal notion of forcing. We look at the
value $F(\alpha)$ and define the forcing $\dot{\mathbb{Q}}_{\alpha}$ according
to $F(\alpha)$ by cases as follows.

####  3.3.1 Case a

For the first case we assume that $F(\alpha)=(\beta,\gamma,m,k)$, where the
$\gamma$-th (in some wellorder of $W$) names of a real of
$W^{\mathbb{P}_{\beta}}$ is $\dot{x}$. We assume that

$W[G_{\alpha}]\models\varphi_{m}(\dot{x}^{G_{\alpha}})$

yet for every legal notion of forcing $\mathbb{P}$ and every choice for a
$\mathbb{P}$-generic filter $H$:

$L[G_{\alpha}\ast H]\models\lnot\varphi_{k}(\dot{x}^{G_{\alpha}}).$

In that case we code the triple $(x,m,k)$ into the first $\omega$-block of
$\vec{S}^{1}$ which is still Suslin in $W[G_{\alpha}]$. More precisely we let
$\beta_{\alpha}<\omega_{1}$ be least such that for every $n\in\omega$,
$S_{\omega\cdot\beta_{\alpha}+n}$ is Suslin. Then we let $w$ be some real
which codes $(x,m,k)$ and let
$\dot{\mathbb{Q}}_{\alpha}:=\dot{\mathbb{Q}}^{0}_{\alpha}\ast\dot{\mathbb{Q}}^{1}_{\alpha}\ast\dot{\mathbb{Q}}^{2}_{\alpha}$,
where $\dot{\mathbb{Q}}^{0}_{\alpha}$ is a finitely supported $\omega$-length
iteration of the factors $(S_{2n+i}\,:\,n\in\omega,i\in 2)$ of Suslin tree
forcings, where $S_{2n+i}$ for $i=0$ if $\dot{w}^{G_{\alpha}}(n)=0$, and
$S_{2n+i}$ for $i=1$ if $\dot{w}^{G_{\alpha}}(n)=1$. If we pause for a second,
let $G^{0}$ be an $W[G_{\alpha}]$-generic for $\dot{\mathbb{Q}}^{0}_{\alpha}$
then the just built generic extension $W[G_{\alpha}][G^{0}]$ can define the
real $w=\dot{w}^{G_{\alpha}}$:

  * $(\ast\ast)$

In $W[G_{\alpha}][G^{0}]$ it holds that $n\in w$ if and only if
$S_{\omega\cdot\beta_{\alpha}+2n}$ is Suslin, and $n\notin w$ if and only if
$S_{\omega\cdot\beta_{\alpha}+2n+1}$ is Suslin.

Indeed if $n\notin w$ then we shot a branch through
$S_{\omega\cdot\beta_{\alpha}+2n}$. If on the other hand
$S_{\omega\cdot\beta_{\alpha}+2n}$ is Suslin in $W[G_{\alpha}][G^{0}]$ then we
must have forced with $S_{\omega\cdot\beta_{\alpha}+2n+1}$ as we always use
either $S_{\omega\cdot\beta_{\alpha}+2n+1}$ or
$S_{\omega\cdot\beta_{\alpha}+2n}$ and every other factor preserves the
statement “$S_{\omega\cdot\beta_{\alpha}+2n}$ is Suslin$"$.

We note that we can apply David’s trick in this situation as well. We code the
$\omega$-many clubs necessary to correctly compute for every $n\in\omega$,
$S_{\omega\beta_{\alpha}+n}$ and the $\omega$-many branches through
$S_{\omega\cdot\beta_{\alpha}+2n+i}$ witnessing $(\ast\ast)$ into just one
subset $X_{\alpha}\subset\omega_{1}$. Then rewrite the information of
$X_{\alpha}$ as a subset $Y_{\alpha}\subset\omega_{1}$ such that it satisfies

  1. 1.

$E(Y_{\alpha})\cap\omega$ codes a well-ordering of type $y_{0}$.

  2. 2.

$E(Y_{\alpha})\cap[\omega,y_{0})=\emptyset$.

  3. 3.

For all $\beta$, $E(Y_{\alpha})\cap[y_{\beta},y_{\beta}+\omega)$ codes a well-
ordering of type $y_{\beta+1}$.

  4. 4.

For all $\beta$, $E(Y_{\alpha})\cap[y_{\beta}+\omega,y_{\beta+1})=\emptyset$.

We obtain

  * $({\ast}{\ast}{\ast})$

For any countable transitive model $M$ of $\mathsf{ZF}^{-}$ such that
$\omega_{1}^{M}=(\omega_{1}^{L})^{M}$ and $Y_{\alpha}\cap\omega_{1}^{M}\in M$,
$M$ can construct its version of the universe $L[Y_{\alpha}\cap\omega_{1}]$,
and the latter will see that there is an ordinal $\xi<\omega_{1}$ and an
$\omega$-block of Suslin trees $S_{\omega\cdot\xi+n}$, computed with the help
of the local $\diamondsuit$-sequence and the $\omega$-sequence of clubs of
$\omega_{1}^{M}$ coded into $Y_{\alpha}\cap\omega_{1}^{M}$, such that for any
$m\in\omega$, $S_{\omega\cdot\xi+2m}^{M}$ is Suslin iff $m\in w$ and
$S_{\omega\cdot\xi+2m+1}^{M}$ is Suslin iff $m\notin w$.

Thus we have a local version of the property $(\ast\ast)$.

In the next step we use almost disjoint forcing $\mathbb{A}_{F}(Y_{\alpha})$
relative to the $<_{L}$-least almost disjoint family of reals $F$ to code the
set $Y_{\alpha}$ into one real $r_{\alpha}$. This forcing is well-known, has
the ccc and its definition only depends on the subset of $\omega_{1}$ we code,
thus the almost disjoint coding forcing $\mathbb{A}_{F}(Z)$ will be
independent of the surrounding universe in which we define it, as long as it
has the right $\omega_{1}$ and contains the set $Z$.

We finally obtained a real $r_{\alpha}$ such that

  * $({\ast}{\ast}{\ast}{\ast})$

For any countable, transitive model $M$ of $\mathsf{ZF}^{-}$ such that
$\omega_{1}^{M}=(\omega_{1}^{L})^{M}$ and $r_{\alpha}\in M$, $M$ can construct
its version of $L[r]$ which in turn thinks that there is an ordinal
$\xi<\omega_{1}$ such that for any $m\in\omega$, $S_{\xi+2m}^{L}$ is Suslin
iff $m\in w$ and $S_{\xi+2m+1}^{L}$ is Suslin iff $m\notin w$.

We say in this situation that the real $w$, which codes $(x,m,k)$_is written
into $\vec{S}^{1}$_, or that $w$ _is coded into_ $\vec{S^{1}}$.

####  3.3.2 Case b

This is the symmetric case to case a, i.e. $F(\alpha)=(\beta,\gamma,n,m)$ and
$W[G_{\alpha}]\models\varphi_{k}(x)$ while there is no legal forcing
$\mathbb{P}$ and no filter $H$ such that $W[G_{\alpha}\ast
H]\models\varphi_{m}(x)$. In that case we code the triple $(x,m,k)$ into a
real $w$ and code $w$ into the first fresh $\omega$-block of elements of
$\vec{S}^{2}$.

####  3.3.3 Case c

In that case we assume that $F(\alpha)=(\beta,\gamma,m,k)$, $m<k$ and that

$W[G_{\alpha}]\models\varphi_{m}(x)$

where $\dot{x}$ is the $\gamma$-th $\mathbb{P}_{\beta}$-name for a real and
$x=\dot{x}^{G_{\alpha}}$. We also assume, contrary to case a, that there is a
legal forcing $\mathbb{P}$ and a generic filter $H$ for $\mathbb{P}$ such that

$W[G_{\alpha}\ast H]\models\varphi_{k}(x)$

In that situation we use $\mathbb{P}$ to obtain $W[G_{\alpha}\ast H]$ in which
$A_{m}$ and $A_{k}$ are no longer disjoint, and by upwards absoluteness of
$\Sigma^{1}_{3}$-statements we do not have to worry about the pair
$(A_{m},A_{k})$ ever again.

Note that the forcing $\mathbb{P}$ which introduces a witness such that
$A_{k}(x)$ holds can possibly introduce fake codes on $\vec{S}^{1}$ and
$\vec{S}^{2}$, i.e. patterns of branches through elements of $\vec{S}$ which
do not correspond to reals we actually intended to be coded. However the set
of Suslin trees of $\vec{S}^{1}$ and $\vec{S}^{2}$ which have been killed in
$W[G_{\alpha}\ast H]$ is still bounded in $\omega_{1}$ as forcing
$\varphi_{k}(x)$ means adding a real $z$ which serves as a witnesses for the
truth of the $\Sigma^{1}_{3}$ formula $\varphi_{k}$. Such a real $z$ can
always be introduced while killing only boundedly many elements of
$\vec{S}^{1}$ and $\vec{S}^{2}$.

####  3.3.4 Case d

This is the symmetric case to c, we assume that
$F(\alpha)=(\beta,\gamma,m,k)$, $m<k$ and $W[G_{\alpha}]\models\varphi_{k}(x)$
and there is a legal $\mathbb{P}$ and a $\mathbb{P}$-generic filter such that
$W[G_{\alpha}\ast H]\models\varphi_{m}(x)$. Then we use $\mathbb{P}$ and $H$
just as in case c, forcing $A_{m}$ and $A_{k}$ to have non-empty intersection.

####  3.3.5 Case e

What is left is the case where $F(\alpha)=(\beta,\gamma,m,k)$, $m<k$ and

$W[G_{\alpha}]\models\lnot\varphi_{m}(x)\land\lnot\varphi_{k}(x).$

Additionally we assume that there is a legal forcing $\mathbb{P}$ and a
generic filter $H$ such that
$W[G_{\alpha}][H]\models\varphi_{m}(x)\land\varphi_{k}(x)$. In that situation
we use $\mathbb{P}$ and $H$, and note again that $\mathbb{P}$ will only
destroy countably many elements of both $\vec{S}^{1}$ and $\vec{S}^{2}$.
Nevertheless we can safely ignore $(A_{m},A_{k})$ in all future models as they
ceased to be disjoint.

####  3.3.6 Case f

We still work under the assumption that $F(\alpha)=(\beta,\gamma,m,k)$, $m<k$
and assume that

$W[G_{\alpha}]\models\lnot\varphi_{m}(x)\land\lnot\varphi_{k}(x).$

In contrast to the last case we assume that there is no legal forcing
$\mathbb{Q}$ such that $\Vdash_{\mathbb{Q}}\varphi_{m}(x)\land\varphi_{k}(x)$.
We distinguish two subcases. First assume that there is a legal forcing
$\mathbb{Q}$ such that

$\Vdash_{\mathbb{Q}}\varphi_{m}(x).$

We fix the least such legal forcing $\mathbb{Q}$ (using some previously fixed
well-order) and note that, by definition of legal, $\mathbb{Q}$ will use a
well-defined, countable set $b_{\alpha}$ of elements of $\vec{S}$ for coding
reals into Suslin trees.

In that situation we will use the first $\omega$-block of $\vec{S^{1}}$ which
is not used by $\mathbb{P}_{\alpha}$ and $\mathbb{Q}$ and use it to code
$(x,m,k)$ with the usual method. This is the forcing
$\dot{\mathbb{Q}}_{\alpha}$ we use at stage $\alpha$. Note that we do not use
$\mathbb{Q}$ here, we just need it to define $\dot{\mathbb{Q}}_{\alpha+1}$
properly.

For the rest of our iteration we ensure that all the legal factors we are
about to use will never touch any of the Suslin trees in $b_{\alpha}$. This
also includes a slight change of definitions in the cases $c,d,$ and $e$ where
we demand from stage $\alpha$ on that legal also includes that no Suslin tree
of a $b_{\alpha}$ will be destroyed. Note that this can always be done as we
are free to chose the places in $\vec{S}$ where the coding should happen and
we always have $\omega_{1}$-many free Suslin trees we can use. This has the
following effect.

Claim: For any legal extension $\mathbb{P}$ of $\mathbb{P}_{\alpha+1}$, which
leaves all the Suslin trees in $b_{\alpha}$ untouched,

$\cancel{\Vdash}_{\mathbb{P}}\,x\in A_{k}.$

###### Proof.

Indeed if not, then $\mathbb{P}\ast\mathbb{Q}=\mathbb{Q}\times\mathbb{P}$ is a
legal forcing and as $\mathbb{P}\Vdash x\in A_{k}$ and $A_{k}$ is
$\Sigma^{1}_{3}$, $\mathbb{P}\times\mathbb{Q}\Vdash x\in A_{k}$. But on the
other hand our assumption was that $\mathbb{Q}\Vdash x\in A_{m}$, thus
$\mathbb{Q}\times\mathbb{P}$ would be a legal forcing which forces $x\in
A_{m}\land A_{k}$ which contradicts the assumption that no legal partial order
forces that $A_{m}\cap A_{k}$ is non-empty. ∎

In the second case, there is no legal forcing $\mathbb{Q}$ for which
$\Vdash_{\mathbb{Q}}\varphi_{m}(x)$ is true, but there is a legal $\mathbb{Q}$
for which $\Vdash_{\mathbb{Q}}\varphi_{k}(x)$ is true. We proceed to code $x$
into the $\vec{S^{2}}$-sequence with the usual coding. Note that by our
assumption, no further legal extension will ever satisfy that $x\in A_{m}$,
thus no unwanted situation can occur.

In the final subcase, there is no legal forcing which forces $x\in A_{m}\cup
A_{k}$, and we are free to choose where to code $x$.

To summarize, we obtain in all subcases a forcing $\mathbb{P}_{\alpha+1}$
which decides where (i.e. into $\vec{S^{1}}$ or $\vec{S^{2}}$) we should place
the triple $(x,m,k)$ and simultaneously ensures that no further legal forcing
which will not destroy a Suslin tree from a definable, countable list of
elements of $\vec{S}$ will lead to a pathological situation.

###  3.4 Discussion of the resulting W[G]

We let $G$ be a generic filter for the $\omega_{1}$-length iteration which we
just described using countable support. First we note that the iteration has
the ccc. Hence the iteration is preserves $\aleph_{1}$. Consequently there
will be no new reals added at stage $\omega_{1}$, so $\omega^{\omega}\cap
W[G]=\bigcup_{\alpha<\omega_{1}}\omega^{\omega}\cap W[G_{\alpha}]$, in
particular $\mathsf{CH}$ is true in $W[G]$.

A second useful observation we already took advantage of, is that for every
pair of stages $\alpha<\beta<\omega_{1}$, the quotient-forcing which we use to
pass from $\mathbb{P}_{\alpha}$ to $\mathbb{P}_{\beta}$ is a legal forcing at
stage $\alpha$. Now it is straightforward to check that every forcing we used
in the five cases is a legal forcing at their respective stage, and that a
countable length iteration of legal forcings (with finite support) will yield
a legal forcing in the end, as seen from the starting model of the iteration.

Our goal is now to define, given a pair of disjoint $\Sigma^{1}_{3}$-definable
sets $A_{m},A_{k}$ a $\Delta^{1}_{3}(\alpha_{0})$-definable separating set,
i.e. a set such that $A_{m}\subset D^{1}_{m,k}$ and $A_{k}\subset D_{m,k}^{2}$
and such that $D_{m,k}^{2}=D_{m,k}^{c}$. We want our set $D^{1}_{m,k}$ to
consist of the codes written into $\vec{S}^{1}$ which itself contain a code
for the pair $(m,k)$ and its converse $D_{m,k}^{2}$ to consist of all the
codes on the $\vec{S}^{2}$-side which contain a code for $(m,k)$. It is clear
however that there were stages in the definition of the iteration where we
left open the possibility for adding unwanted codes on $\vec{S}^{1}$ and
$\vec{S}^{2}$. Indeed in the definition of the cases c,d and e we will always
use a legal forcing $\mathbb{P}$ (possibly preserving some blocks of Suslin
trees which showed up in stages where case f applied) which could possibly add
a code for some unwanted triple $(x,m,k)$ on the $\vec{S}^{1}$-sequence, i.e.
a triple $(x,m,k)$ such that $A_{k}(x)$ eventually becomes true, thus
preventing $D_{m,k}$ from separating $A_{m}$ from $A_{k}$. Note however that
such a degenerate situation can only happen once for every pair
$(A_{m},A_{k})$. As we only have countably many such pairs and as our
iteration has length $\omega_{1}$ and as we visit every triple $(x,m,k)$
uncountably often with our bookkeeping function, there will be a stage
$\alpha_{0}<\omega_{1}$ such that from $\alpha_{0}$ on all the codes we have
written into $\vec{S}^{1}$ and $\vec{S}^{2}$ are intended ones, i.e. the codes
really define a separating set $D_{m,k}$ for $A_{m}$ and $A_{k}$.

We let:

$\displaystyle x\in D_{m,k}^{1}(\alpha_{0})\Leftrightarrow$
$\displaystyle\exists\alpha>\alpha_{0}(x\text{ can be read off from an }$
$\displaystyle\omega\text{-block of elements of }\vec{S}^{1}\text{ starting at
}\alpha_{0}.)$

and

$\displaystyle x\in D_{m,k}^{2}(\alpha_{0})\Leftrightarrow$
$\displaystyle\exists\alpha>\alpha_{0}(x\text{ can be read off from an }$
$\displaystyle\omega\text{-block of elements of }\vec{S}^{2}\text{ starting at
}\alpha_{0}.)$

If $m,k$ are Gödel codes for two disjoint $\Sigma^{1}_{3}$-sets then
$D_{m,k}^{1}(\alpha_{0})$ and $D_{m,k}^{2}(\alpha_{0})$ form a partition.

######  Lemma 3.6.

In $L[G]$ for every pair $m\neq k\in{\omega}$, $D^{1}_{m,k}(\alpha_{0})$ and
$D_{m,k}^{2}(\alpha_{0})$ union up to all the reals.

###### Proof.

Immediate from the definitions. ∎

######  Lemma 3.7.

In $W[G]$ for every pair $(m,k)$, if the $\Sigma^{1}_{3}$-sets $A_{m}$ and
$A_{k}$ are disjoint then $D^{1}_{m,k}(\alpha_{0})$ separates $A_{m}$ and
$A_{k}$.

###### Proof.

Assume that $A_{m}$ and $A_{k}$ are disjoint and let $x\in
L[G]\cap\omega^{\omega}$ be arbitrary. There is a least stage $\alpha$ with
$\alpha_{0}<\alpha<\omega_{1}$ such that $F(\alpha)=(\dot{x},m,k)$ where
$\dot{x}$ is a name for $x$. According to the definition of the iteration and
the assumption that $A_{m}\cap A_{k}=\emptyset$, we can rule out the cases
$c,d$, and $e$. Thus case $a,b$ and the subcases of $f$ are remaining and in
all of these cases we coded $x$ either into $\vec{S}^{1}$ or $\vec{S}^{2}$ and
made sure that no further coding would put $x$ into the opposite
$\vec{S}$-sequence. Thus for any $x\in W[G]$, $x\in D^{1}_{m,k}(\alpha_{0})$
or $D_{m,k}^{2}(\alpha_{0})$ and these two sets are disjoint. ∎

######  Lemma 3.8.

In $W[G]$, every set $D_{m,k}$ and $D_{m,k}^{c}$ are in fact
$\Sigma^{1}_{3}(\alpha_{0})$-definable. Thus $W[G]$ satisfies that every pair
of disjoint $\Sigma^{1}_{3}$-sets can be separated by a
$\Delta^{1}_{3}(\alpha_{0})$-set.

###### Proof.

We claim that for $m,k\in\omega\times\omega$ arbitrary, $D_{m,k}$ and
$D_{m,k}^{c}$ have the following definitions in $W[G]$:

$\displaystyle x\in D_{m,k}\Leftrightarrow$ $\displaystyle\exists r\forall
M(r,\alpha_{0}\in M\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\land M\text{
transitive }\rightarrow$ $\displaystyle M\models
L[r]\models\exists\alpha>\alpha_{0}(x\text{ can be read off from an }$
$\displaystyle\omega\text{-block of elements of }\vec{S}^{1}\text{ starting at
}\alpha.)$

and

$\displaystyle x\in D_{m,k}^{c}\Leftrightarrow$ $\displaystyle\exists r\forall
M(r,\alpha_{0}\in M\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\land M\text{
transitive }\rightarrow$ $\displaystyle M\models
L[r]\models\exists\alpha>\alpha_{0}(x\text{ can be read off from an }$
$\displaystyle\omega\text{-block of elements of }\vec{S}^{2}\text{ starting at
}\alpha.)$

Counting quantifiers yields that both formulas are of the form
$\exists\forall(\Sigma^{1}_{2}\rightarrow\Delta^{1}_{2})$ and hence
$\Sigma^{1}_{3}$.

We will only show the result for $D_{m,k}$. To show the direction from left to
right, note that if $x\in D_{m,k}$, then there was a stage $\alpha>\alpha_{0}$
in our iteration such that we coded $x$ into the $\vec{S}^{1}$-sequence. In
particular we added a real $r_{\alpha}$ for which property
$({\ast}{\ast}{\ast}{\ast})$ is true, hence $r_{\alpha}$ witnesses that the
right hand side is true in $W[G]$.

For the other direction assume that the right hand side is true. This in
particular means that the assertion is true for transitive models containing
$r$ of arbitrary size. Indeed if there would be a transitive $M$ which
contains $r$ and whose size is $\geq\aleph_{1}$, then there would be a
countable $M_{0}\prec M$ which contains $r$. The transitive collapse of
$M_{0}$ would form counterexample to the assertion of the right hand side,
which is a contradiction to our assumption.

But if the right hand side is true for models of arbitrary size, by reflection
it must be true for $W[G]$ itself, thus $x\in D_{m,k}$ and we are done.

∎

##  4 Boldface Separation

###  4.1 Preliminary Considerations

We turn our attention to boldface separation.

######  Theorem 4.1.

There is an $\omega_{1}$-preserving, generic extension of $L$ in which every
pair of disjoint $\bf{\Sigma^{1}_{3}}$-sets $A_{m}$ and $A_{k}$ can be
separated by a $\bf{\Delta^{1}_{3}}$-set.

Its proof will heavily rely on the proof of the last theorem, hence we try to
use the same notation as before. It is clear that if we want to iterate in
order to handle all $\bf{\Sigma^{1}_{3}}$-sets simultaneously, we have to be
more careful as the codings would start to interfere with each other causing
chaos. The main idea to keep control is to replace the notion of legal forcing
with a dynamic variant which keeps changing along the iteration.

To motivate the following we first consider a more fine-tuned approach to the
definition of the iteration of the proof of the last theorem. Let us assume we
start the iteration of last theorems proof, and assume that $(m,k)$ is the
first pair such that case f in the definition of the iteration applies. Recall
that in the discussion of case f, we showed that, given a pair $(A_{m},A_{k})$
of $\Sigma^{1}_{3}$-sets for which there does not exist a legal forcing
$\mathbb{Q}$ such that $\Vdash_{\mathbb{Q}}\exists
z(\varphi_{m}(z)\land\varphi_{k}(z))$ becomes true, we can assign for an
arbitrary real $x$ always a side $\vec{S}^{1}$ or $\vec{S}^{2}$ such that in
all future legal extensions, as long as they leave certain well-defined blocks
of elements of $\vec{S}$ untouched, there will never occur a _pathological
situation_ , i.e. from that stage on we never run into the problem of having
coded the triple $(x,m,k)$ into, say, $\vec{S^{1}}$, yet $\varphi_{k}(x)$
becomes true in some future extension of our iteration (or vice versa). Note
here that the arguments in the discussion of case f were uniform for all reals
$x$ which appear in a legal extension. So it is reasonable to define for the
pair $(m,k)$ an assignment function which assigns for every real $x$ a value
$g_{m,k}(x)\in\\{m,k\\}\times[\vec{S}]^{\omega}$, where $g_{m,k}(x)=(m,b)$
should mean that, when applying the reasoning of case f to $x$ we end up
coding the triple $(x,m,k)$ into the $m$-side, i.e. we code $(x,m,k)$ into
$\vec{S^{1}}$, while $b$ is the countable set of blocks of Suslin trees we
have to preserve in all future legal extensions to guarantee that no
pathological situation (in the sense as described above) will happen for the
pair $(m,k)$. We again emphasize that the definition of $g_{m,k}(x)$ also
works for any $x$ which is a real in some arbitrary legal extension of the
universe we are in. This uses the fact that legal forcings can be iterated.
The case where $g_{m,k}=(k,b)$ is defined similarly.

Now if we continue the iteration from the proof of the last theorem, whenever
we encounter a stage where case $c,d,e$ or $f$ applies, i.e stages where we
have to use some legal forcing
$\mathbb{Q}=(\mathbb{Q}_{\beta},\dot{\mathbb{Q}}(\beta))_{\beta<\gamma}$, in
order to keep the veracity of the earlier added codes, we should demand from
the legal forcing
$\mathbb{Q}=(\mathbb{Q}_{\beta},\dot{\mathbb{Q}}(\beta))_{\beta<\gamma}$ to
satisfy additionally:

  1. $(+)$

whenever $\alpha<\gamma$ and $\dot{\mathbb{Q}}(\alpha)$ is a coding forcing
which codes a triple of the form $(y,m,k)$ for $y\in 2^{\omega}$ into
$\vec{S}$, then the placement is in accordance with the value of $g_{m,k}(y)$.
This means that if $g_{m,k}(y)=(m,b)$ then $(y,m,k)$ is coded into
$\vec{S^{1}}$ (and similarly for $g_{m,k}(y)=(k,b)$) and $b$ is not touched by
$\mathbb{Q}$. We say in this case that the legal forcing $\mathbb{Q}$ respects
$g_{m,k}$.

Note that this reasoning is sound, as we assumed that
$\varphi_{m}\land\varphi_{k}$ can never have non-empty intersection in legal
extensions. Legal forcings which additionally satisfy this property will be
called $1$-legal forcings (with respect to $(m,k)$). Note that 1-legal
forcings can be iterated with finite support and remain 1-legal as seen from
the ground model. Note further that whenever we use a 1-legal forcing, then no
new pathological situation can occur for the pair $(A_{m},A_{k})$ in the
generic extension. Thus when restricting the iteration from that point on to
only use 1-legal forcings will guarantee the existence of a countable ordinal
from which on all codes concerning $A_{m}$ and $A_{k}$ are correct.

Hence we alter the usual definition of the iteration, from the moment we first
encounter a pair $(A_{m},A_{k})$ as above, and replace every instance of
“legal$"$ with “1-legal$"$ in the definition of the iteration, and as just
argued, this will yield that the separating sets $D^{1}_{m,k}$ and
$D^{2}_{m,k}$ for $A_{m}$ and $A_{k}$ will have a
$\Sigma^{1}_{3}(\alpha)$-definition, where $\alpha$ is the stage where $(m,k)$
is first considered by the bookkeeping $F$.

If we reach a first pair $(m^{\prime},k^{\prime})\neq(m,k)$ in which the now
altered case $f$ applies for $(y,m,k)$, then it is possible to define a
1-assignment function $g^{1}_{m^{\prime}k^{\prime}}$ just as before. Note here
that in the definition of $g^{1}_{m^{\prime},k^{\prime}}$, we might have to
consider two unions of countable sets of blocks of $\vec{S}$ which we must not
touch in all future extensions. This of course is no problem, as we always
have $\aleph_{1}$-many fresh Suslin trees available.

From that point on, in the iteration, we restrict ourselves to legal forcings
$\mathbb{Q}=(\mathbb{Q}_{\beta},\mathbb{Q}(\beta))_{\beta<\gamma}$ which
satisfy the now altered property:

  1. $(++)$

All placements of $\mathbb{Q}$ of triples of the form $(z,m,k)$ and
$(z,m^{\prime},k^{\prime})$ are in accordance with the assignment functions
$g_{m,k}=g^{0}_{m,k}$ and $g^{1}_{m^{\prime}k^{\prime}}$, and the additional
blocks of Suslin trees introduced by these assignments should not be touched
by $\mathbb{Q}$ as well. We say that $\mathbb{Q}$ respects the assignment
$g^{0}_{m,k}$ and $g^{1}_{m^{\prime},k^{\prime}}$.

These legal forcings will be denoted with 2-legal (with respect to $(m,k)$ and
$(m^{\prime},k^{\prime})$, note here that the order does matter).

The above notions can be iterated and will be the key concept to make a proof
of the theorem possible.

###  4.2 Definition of the iteration

We start again with $W$ as our ground model and fix our two definable
sequences of $W$-Suslin trees of height $\omega_{1}$, $\vec{S^{1}}$ and
$\vec{S^{2}}$. We use as coding forcings exactly the same forcings we used in
the last theorem, i.e. we write codes into $\vec{S^{1}}$ and $\vec{S^{2}}$ via
adding branches of elements of $\vec{S}$ and almost disjoint coding. We let
$F$ be our bookkeeping function which determines the countably supported
iteration. $F$ maps from $\omega_{1}$ to $\omega_{1}^{4}\times\omega^{2}$. The
goal is to find for every quadruple $(y^{1}_{m},y^{2}_{k},m,k)\in
2^{\omega}\times 2^{\omega}\times\omega^{2}$ a pair of
$\bf{\Sigma^{1}_{3}}$-sets of reals $D^{1}_{y^{1}_{m},y^{2}_{k},m,k}$ and
$D^{2}_{y^{1}_{m},y^{2}_{k},m,k}$ such that $A_{m,y^{1}_{m}}\subset
D^{1}_{y^{1}_{m},y^{2}_{k},m,k}$ and $A_{k,y^{2}_{k}}\subset
D^{2}_{y^{1}_{m},y^{2}_{k},m,k}$.

Assume that we are at stage $\alpha<\omega_{1}$ of our iteration. Assume that
$F(\alpha)=(\eta_{1},\eta_{2},\eta_{3},\eta_{4},\eta_{5},\eta_{6},m,k)$ and
assume that $\dot{x}$ is the $\eta_{1}$-th name of a real in
$W^{\mathbb{P}_{\eta_{2}}}$. Assume further that $\dot{y}_{1}$ and
$\dot{y}_{2}$ are the $\eta_{3}$-th name of a real of
$W^{\mathbb{P}_{\eta_{4}}}$ and $\eta_{5}$-th name of a real in
$W^{\mathbb{P}{\eta_{6}}}$. Let $\dot{x}^{G_{\alpha}}=x$ and
$\dot{y}_{1}^{G_{\alpha}}=y_{1},\dot{y}_{2}^{G_{\alpha}}=y_{2}$. By induction
we will have constructed already the following list of objects.

  * •

A sequence
$(g^{\beta}_{m_{\beta},k_{\beta},y^{1}_{\beta},y^{2}_{\beta}}\,:\,\beta\in
I_{\alpha}\subset\alpha)$ of assignment functions, we introduced at earlier
stages of the iteration. We always introduce one whenever, for a given pair
$\varphi_{m}(v_{0},y^{1}_{m})\land\varphi_{k}(v_{0},y^{2}_{k})$, we encounter
for the first time a situation similar to case $f$ of the last iteration. Let
$I_{\alpha}:=\\{\beta<\alpha$
$\exists(m_{\beta},k_{\beta},y^{1}_{\beta},y^{2}_{\beta})$ such that
$g^{\beta}_{m_{\beta},k_{\beta},y^{1}_{\beta},y^{2}_{\beta}}$ is defined$\\}$.

  * •

Let $\beta_{\alpha}$ be the ordertype of $I_{\alpha}$. Then for every
$\beta\leq\beta_{\alpha}$, a notion of $\beta$-legal. We inductively assume
that $\beta$-legal becomes a stronger notion when we increase $\beta$. We also
assume that the iteration so far satisfies that for every
$\beta\in\beta_{\alpha}$, the tail of the iteration
$\mathbb{P}_{[\gamma_{\beta},\alpha)}$ is a $\beta$-legal iteration as seen
from the ground model $W[G_{\gamma_{\beta}}]$, where $\gamma_{\beta}$ is the
$\beta$-th ordinal in $I_{\alpha}$.

  * •

A countable set $b_{\alpha}$ of $\omega$-blocks of $\vec{S}$ which shall be
preserved along the iteration. These blocks are introduced in case f from the
last section and ensure that no bad patterns occur beyond certain countable
ordinals.

  * •

A set $C_{\alpha}$ which should denote all the quintuples
$(x,y^{1},y^{2},m,k)$ we have coded so far into blocks from $\vec{S^{1}}$ and
$\vec{S^{2}}$. There will be an ordinal $\gamma_{\alpha}<\omega_{1}$ which is
the supremum of all the indices of elements of $\vec{S^{1}}$ and $\vec{S^{2}}$
which have been detroyed so far, and all the blocks of Suslin trees we must
not use.

  * •

For every $\beta\in I_{\alpha}$, there is a $\delta_{\beta}<\gamma_{\alpha}$
such that $\delta_{\beta}$ is the starting point for the codes which will
define the sets $D^{1}_{y^{1}_{\beta},y^{2}_{\beta},m_{\beta},k_{\beta}}$ and
$D^{2}_{y^{1}_{\beta},y^{2}_{\beta},m_{\beta},k_{\beta}}.$ This
$\delta_{\beta}$ will play exactly the same role as the $\alpha_{0}$ did in
the proof of the last theorem, i.e. it is the ordinal from which on all the
codes which contain the quadruple
$(y^{1}_{\beta},y^{2}_{\beta},m_{\beta},k_{\beta})$ are intended ones, which
have not been created by accident in the process of forcing some other pair of
$\bf{\Sigma^{1}_{3}}$-sets to have non-empty intersection.

We turn to the definition of the forcing we want to use at stage $\alpha$ in
our iteration.

Assume that
$F(\alpha)=(\eta_{1},\eta_{2},\eta_{3},\eta_{4},\eta_{5},\eta_{6},m,k)$ and
assume that $\dot{x}$ is the $\eta_{1}$-th name of a real in
$W^{\mathbb{P}_{\eta_{2}}}$. Assume further that $\dot{y}_{1}$ and
$\dot{y}_{2}$ are the $\eta_{3}$-th name of a real of
$W^{\mathbb{P}_{\eta_{4}}}$ and $\eta_{5}$-th name of a real in
$W^{\mathbb{P}{\eta_{6}}}$. Let $\dot{x}^{G_{\alpha}}=x$ and
$\dot{y}_{1}^{G_{\alpha}}=y_{1},\dot{y}_{2}^{G_{\alpha}}=y_{2}$.

We distinguish the same six cases $a-f$ as we did in the previous proof. For
the cases $a-e$, all we need to do is to replace the notion “legal$"$ with the
according “$\beta_{\alpha}$-legal$"$ and otherwise proceed exactly as there.

What is left is case $f$. Thus we assume that $A_{m}(y_{1})\cap
A_{k}(y_{2})=\emptyset$ and $x\notin A_{m}(y_{1})$ and $x\notin A_{k}(y_{2})$
and there is no $\beta_{\alpha}$-legal forcing $\mathbb{Q}$ for which
$\Vdash_{\mathbb{Q}}\exists z(\varphi_{m}(z,y_{1})\land\varphi_{k}(z,y_{2})$
is true. We argue in $L[G_{\alpha}]$ and define the next forcing
$\dot{\mathbb{Q}}_{\alpha}$ as expected. Ask whether there is a
$\beta_{\alpha}$-legal $\mathbb{Q}$ such that
$\Vdash_{\mathbb{Q}}\varphi_{m}(x,y_{1})$. If this is true then proceed as in
case $f$ in the definition of the iteration in the proof of the first theorem.

Replacing in that argument every instance of “legal$"$ with the notion
$\beta_{\alpha}$-legal we argue, as there and using the fact that
$\beta_{\alpha}$-legal notions of forcing are closed under iteration, that one
can either have that $x$ will be coded into $\vec{S^{1}}$ while ensuring that
no further $\beta_{\alpha}$-legal iteration will ever force $x\in
A_{k}(y_{2})$ or $x$ will be coded into $\vec{S^{2}}$ while ensuring that no
further $\beta_{\alpha}$-legal iteration will force that $x\in A_{m}(y_{1})$.
Fix as assignment value $g^{\beta_{\alpha}+1}_{m,k,y_{1},y_{2}}(x)$ the
corresponding case we found ourselves in and the associated blocks of Suslin
trees we must not touch in all future extensions. Let $b_{\alpha+1}$ be
$b_{\alpha}$ and the second coordinate of
$g^{\beta_{\alpha}+1}_{m,k,y_{1},y_{2}}(x)$.

Lastly we want to define $\delta_{\alpha}$. We do so only if $\alpha$ is the
least ordinal such that for some fixed quintuple $(y_{1},y_{2},m,k)$ there is
a $\mathbb{P}_{\alpha}$-name $\dot{x}$ of a real, which evaluates to $x$ and
such that $F(\alpha)$ corresponds to $(x,y_{1},y_{2},m,k)$. These are the only
stages $\alpha$ where we define $\delta_{\alpha}$. If we are in such a
situation, we set $\delta_{\alpha}$ to be just $\gamma_{\alpha}$, where
$\gamma_{\alpha}$ is defined in the fourth item of the list of already defined
objects at the beginning of the definition of this iteration.

Finally we can say what $\beta_{\alpha}+1$-legal should mean. Note that after
forcing with $\dot{\mathbb{Q}}_{\alpha+1}$ we do have a set
$\\{g^{\gamma}_{m_{\gamma},k_{\gamma},y^{1}_{\gamma},y^{2}_{\gamma}}\,:\,\gamma\leq\beta_{\alpha+1}\\}$
for some natural numbers $m_{\gamma},k_{\gamma}$ and reals
$y^{1}_{\gamma},y^{2}_{\gamma}$.

######  Definition 4.2.

A legal forcing
$\mathbb{Q}=(\mathbb{Q}_{\eta}.\dot{\mathbb{Q}}_{\eta})_{\eta<\zeta}$ which
respects for every $\gamma\leq\beta_{\alpha+1}$ the assignment function
$g^{\gamma}_{m_{\gamma},k_{\gamma},y^{1}_{\gamma},y^{2}_{\gamma}}$ is called
$\beta_{\alpha+1}$-legal.

This definition makes it possible to gradually create good codes while keeping
control over the noise which we have to create as well in the process of
forcing $\bf{\Sigma^{1}_{3}}$-sets non-disjoint.

This ends the definition of the iteration. Use finite support and let
$W[G_{\omega_{1}}]=W_{1}$ be the resulting universe. We shall show that in
$W_{1}$ every pair of disjoint $\bf{\Sigma^{1}_{3}}$ sets can be separated by
a $\bf{\Delta^{1}_{3}}$-set.

###  4.3 Discussion of the resulting universe

As $W[G_{\omega_{1}}]$ is a ccc extension of $W$, $\omega_{1}$ is preserved.
Moreover $\mathsf{CH}$ remains true.

A second observation is that for every stage $\alpha$ of our iteration and
every $\eta>\alpha$, the intermediate forcing $\mathbb{P}_{[\alpha,\eta)}$,
defined as the factor forcing of $\mathbb{P}_{\alpha}$ and
$\mathbb{P}_{\eta}$, is always an $\beta_{\alpha}$-legal forcing. This is
clear as by the definition of the iteration, we force at every stage $\alpha$
with a $\beta_{\alpha}$-legal forcing and $\beta$-legal becomes a stronger
notion as we increase $\beta$.

For a pair of disjoint sets defined via $\\{x\in
2^{\omega}\,:\,\varphi_{m}(x,y_{1})\\}$ and $\\{x\in
2^{\omega}\,:\,\varphi_{k}(x,y_{2})\\}$ we consider the least $\beta$ such
that there is a $\mathbb{P}_{\beta}$-name $\dot{z}$ such that
$\dot{z}^{G_{\beta}}=z$ and $(z,y_{1},y_{2},m,k)$ are considered by $F$ at
stage $\beta$. We let $\delta_{\beta}$ be just as in the third item of the
definition of the iteration. Then for any real $x\in L[G_{\omega_{1}}]$:

$\displaystyle x\in
D^{1}_{y_{1},y_{2},m,k}(\delta_{\beta})\Leftrightarrow\exists\alpha>\delta_{\beta}($
$\displaystyle x\text{ can be read off as the first coordinate from a code}$
$\displaystyle\text{ written on an }\omega\text{ block of elements of
}\vec{S^{1}}\text{ starting at }\alpha.)$

and

$\displaystyle x\in
D_{y_{1},y_{2},m,k}^{2}(\delta_{\beta})\Leftrightarrow\exists\alpha>\delta_{\beta}($
$\displaystyle x\text{ can be read off as the first coordinate from an }$
$\displaystyle\omega\text{ block of elements of }\vec{S^{2}}\text{ starting at
}\alpha.)$

It is clear from the definition of the iteration that for any pair of real
parameters $y_{1}$ and $y_{2}$ and any $m,k\in\omega$,
$D^{1}_{y_{1},y_{2},m,k}\cup D^{2}_{y_{1},y_{2},m,k}=2^{\omega}$. The next
lemma is just an observation and follows directly from the definitions of the
iteration.

######  Lemma 4.3.

Let $y_{1}$ and $y_{2}\in 2^{\omega}\cap W[G_{\omega_{1}}]$ and let
$m,k\in\omega$ such that $\varphi_{m}(v_{0},y_{1})$ and
$\varphi_{k}(v_{0},y_{2})$ defines two disjoint $\bf{\Sigma^{1}_{3}}$-sets.
Then there is an ordinal $\delta<\omega_{1}$ such that the sets
$D^{1}_{y_{1},y_{2},m,k}(\delta)$ and $D^{2}_{y_{1},y_{2},m,k}(\delta)$
partition the reals.

###### Proof.

Let $\alpha$ be the least stage such that there is a real $x$ such that
$F(\alpha)$ evaluates with the help of the generic $G_{\alpha}$ to a quintuple
$(x,y_{1},y_{2},m,k).$ Then, as $\varphi_{m}(v_{0},y_{1})$ and
$\varphi_{k}(v_{0},y_{2})$ are disjoint in $W[G_{\omega_{1}}]$, by the rules a
new assignment $g^{\beta_{\alpha}}_{{m,k,y_{1},y_{2}}}$ is defined at stage
$\alpha$, which implies that every real gets assigned to either $m$ or $k$
after stage $\alpha$ of the iteration. Thus $\delta_{\alpha}=:\delta$ is as
desired.

∎

######  Lemma 4.4.

Let $y_{1}$ and $y_{2}\in 2^{\omega}\cap W[G_{\omega_{1}}]$ and let
$m,k\in\omega$ such that $\varphi_{m}(v_{0},y_{1})$ and
$\varphi_{k}(v_{0},y_{2})$ defines two disjoint $\bf{\Sigma^{1}_{3}}$-sets
$A_{m}(y_{1})$ and $A_{k}(y_{2})$ respectively. Then there is an ordinal
$\delta<\omega_{1}$ such that

$A_{m}(y_{1})\subset D^{1}_{y_{1},y_{2},m,k}(\delta)$

and

$A_{k}(y_{2})\subset D^{2}_{y_{1},y_{2},m,k}(\delta).$

###### Proof.

We consider the smallest ordinal $\alpha<\omega_{1}$ such that there is an $x$
and $F(\alpha)$ considers a set which corresponds to a quintuple of the form
$(x,y_{1},y_{2},m,k)$. As $A_{m}(y_{1})$ and $A_{k}(y_{2})$ are disjoint we
know that at stage $\alpha$ we were in either case a,b or case f. We may
assume that case f applies, i.e. $W[G_{\alpha}]\models x\notin A_{m}\cup
A_{k}$. We set $\delta:=\delta_{\alpha}$ and claim that $\delta$ is as
desired.

Indeed if not, then we can assume without loss of generality that there is a
real $z$ such that $z\in A_{m}(y_{1})$ and $z\in D^{2}_{y_{1},y_{2},m,k}$. Let
$\alpha^{\prime}$ be the least stage such that at $\alpha^{\prime}$
$(z,m,k,y_{1},y_{2})$ is considered by $F$. Then by the rules of the iteration
and as $z\in D^{2}_{y_{1},y_{2},m,k}$,
$g^{\beta_{\alpha^{\prime}}}_{m,k,y_{1},y_{2}}(z)=k$. As from stage
$\alpha^{\prime}$ on we only use at least $\beta_{\alpha^{\prime}+1}$-legal
forcings, the iteration from $\alpha^{\prime}$ on will respect
$g^{\beta_{\alpha^{\prime}+1}}_{m,k,y_{1},y_{2}}$, i.e. it will ensure that
$z$ will not become an element of $A_{m}(y_{1})$. But this is a contradiction
as we assumed that $W[G_{\omega_{1}}]\models z\in A_{m}(y_{1})$.

∎

The next lemma will finish the proof of our theorem:

######  Lemma 4.5.

In $W[G_{\omega_{1}}]$, if $y_{1},y_{2}$ are arbitrary real parameters and
$m,k$ natural numbers, then the sets $D_{r,y_{1},y_{2},m,k}$ and
$D_{r,y_{1},y_{2},m,k}^{c}$ are $\Sigma^{1}_{3}(\delta_{\alpha})$-definable,
where $\delta_{\alpha}$ is a countable ordinal

###### Proof.

The proof is almost identical to the proof of Lemma 3.8, the only thing added
is the countable ordinal $\delta_{\alpha}$ which should be chosen as in the
definition of the iteration. ∎

##  5 Forcing the lightface $\Sigma^{1}_{3}$-separation property

The techniques developed in the previous sections can be used to force a model
where the (lightface) $\Sigma^{1}_{3}$-separation property is true. In what
follows, we heavily use ideas and notation from earlier sections, so the
upcoming proof can not be read independently.

######  Theorem 5.1.

Starting with $L$ as the ground model, one can produce a set-generic extension
$L[G]$ which satisfies $\mathsf{CH}$ and in which the
${\Sigma^{1}_{3}}$-separation property holds.

###### Proof.

The ground model over which we form an iteration is the universe $W$ again,
which was defined earlier. Over $W$ we will perform first an $\omega$-length,
finitely supported iteration
$(\mathbb{P}_{n},\dot{\mathbb{P}}(n))_{n\in\omega}$ of legal posets (where
again the term legal is defined almost as in previous sections, with the
difference that we code instead of triples $(x,m,k)$ quadruples of the form
$(x,0,m,k)$ and $(x,1,m,k)$ into $\vec{S}$), and then a second iteration of
length $\omega_{1}$. The codes of the form $(x,0,m,k)$ shall eventually define
the separating sets for $\varphi_{m}$ and $\varphi_{k}$; codes of the form
$(x,1,m,k)$ shall correspond to countable ordinals which indicate the
correctness of certain codes of the form $(x,0,m,k)$ beyond these countable
ordinals.

We let $\\{(\varphi_{m_{n}},\varphi_{k_{n}})\,:\,n\in\omega\\}$ be an
enumeration of all pairs of $\Sigma^{1}_{3}$-formulas. Assume that
$(\varphi_{m_{0}},\varphi_{k_{0}})$ is such that there is no legal forcing
$\mathbb{Q}$ such that $W[\mathbb{Q}]\models\exists
z(\varphi_{m_{0}}\land\varphi_{k_{0}})$. Repeating the arguments from before,
we can define an assignment function $g_{m_{0},k_{0}}:$
$\omega^{\omega}\rightarrow\\{m_{0},k_{0}\\}\times[\vec{S}]^{\omega}$. Then we
say that a legal iteration $\mathbb{Q}$ is _1-legal_ if and only if whenever a
quadruple of the form $(x,0,m_{0},k_{0})$ is coded into $\vec{S}$ by
$\mathbb{Q}$, the coding respects the assignment function $g_{m_{0},k_{0}}$.
Additionally we demand that no quadruple of the form $(x,1,m_{0},k_{0})$ is
coded into $\vec{S}^{1}$ by $\mathbb{Q}$. As will become clear in a second,
every step of the iteration
$(\mathbb{P}_{n},\dot{\mathbb{P}}_{n})_{n\in\omega}$ will either use a legal
forcing or define a new and gradually stronger notion of legality. We let
$l_{n}\in\omega$ denote the degree of legality we have already defined at
stage $n\in\omega$ of our iteration and define $l_{0}$ to be $0$ (where
0-legal should just be legal) and $l_{1}$ to be 1 for the base case of our
induction; likewise $\mathbb{P}_{0}$ is the set to be the trivial forcing and
$b_{0}=\emptyset$.

The forcing $\mathbb{P}_{\omega}$ is the finitely supported iteration of
$(\mathbb{P}_{n},\dot{\mathbb{P}}_{n})$, which we will define inductively.
Assume we are at stage $n\in\omega$ of the iteration and we have defined
already the following list of objects and notions:

  1. 1.

$\mathbb{P}_{n-1}$ and the generic filter $G_{n-1}$.

  2. 2.

A natural number $l_{n}\leq n$ and a notion of $l_{n}$-legal, which is a
strengthening of 1-legal.

  3. 3.

A finite set of countable ordinals
$\\{\alpha_{0}<\alpha_{1}<...<\alpha_{n-(l_{n}-1)}\\}$. The choice of the
indices will become clear later.

  4. 4.

A countable set $b_{n-1}$ of Suslin trees in $\vec{S}$ which we must not touch
throughout the iteration.

Consider now the $n$-th pair $(\varphi_{m_{n}},\varphi_{k_{n}})$ and split
into cases.

  1. $(a)$

There is an $l_{n}$-legal forcing $\mathbb{Q}$ such that
$W[G_{n-1}][\mathbb{Q}]\models\exists
z(\varphi_{m_{n}}(z)\land\varphi_{k_{n}}(z))$, then we must use the forcing
$\mathbb{Q}$. We calculate the supremum of $b_{n-1}$ and the supremum of the
indices of all the Suslin trees which we killed or assigned to not use in
$\mathbb{Q}$. Let $\alpha_{n-l_{n}}$ denote the maximum of these two suprema.
In second step, we use the usual method to code the quadruple
$(r_{\alpha_{n-l_{n}}},1,m_{h(l_{n})},k_{h(l_{n})})$ into the first allowed
block of $\vec{S}^{1}$, where $r_{\alpha_{n-l_{n}}}$ is a real coding the
ordinal $\alpha_{n-l_{n}}$ and $h(l_{n})$ is the stage where the notion
“$l_{n}$-legal$"$ is defined. Define $b_{n+1}$ in the obvious way via adding
all the new blocks of $\vec{S}$ which must not be used which are introduced by
$\mathbb{Q}$.

  2. $(b)$

In the second case there is no $l_{n}$-legal forcing $\mathbb{Q}$ which forces
$\varphi_{m_{n}}$ and $\varphi_{k_{n}}$ to have non-empty intersection. In
that cases we force with the trivial forcing and define the notion
$l_{n+1}$-legal. We first define a new assignment function $g_{m_{n},k_{n}}$
just as in the previous sections, with the slight difference that we code
instead of triples $(x,m_{n},k_{n})$ quadruples of the form
$(x,0,m_{n},k_{n})$ into $\vec{S}^{1}$ or $\vec{S^{2}}$ while leaving out
certain blocks of elements of $\vec{S}$. Thus, in order to define
$g_{m_{n},k_{n}}(x)$ for an arbitrary real $x$ we ask whether there is an
$l_{n}$-legal forcing $\mathbb{Q}$ which forces
$\Vdash_{\mathbb{Q}}\varphi_{m_{n}}(x)$ to be true. If so then we set
$g_{m_{n},k_{n}}(x)=(m,b)$ where $b$ is the set of blocks of Suslin trees
which are used by $\mathbb{Q}$. Then we say that an $l_{n}$-legal forcing is
$l_{n+1}$-legal if it respects the assignment function $g_{m_{n},k_{n}}$ and
does not code a quadruple of the form $(x,1,m_{n},k_{n})$ into $\vec{S}^{1}$.

We let $\mathbb{P}_{\omega}$ be the direct limit of the forcings
$\mathbb{P}_{n}$ and consider the universe $W[\mathbb{P}_{\omega}]$. We shall
and will assume from now on that in $\mathbb{P}_{\omega}$, case $(b)$ is
applied infinitely many times.

######  Lemma 5.2.

For every $n\in\omega$, the tail of the iteration $(\mathbb{P}_{m}\,:\,m\geq
n)$ is at least an $l_{n}-1$-legal iteration as seen from $W[G_{n}]$.

###### Proof.

This can easily seen if one stares at the definition of the iteration. At
stage $n$ we either follow case $(a)$ which is an $l_{n}-1$-legal forcing, or
we apply case $(b)$, thus define $l_{n}+1$-legality and every further factor
of the iteration must be $l_{n}$-legal. As finite support iterations of
$l_{n}-1$-legal forcings yield an $l_{n}-1$-legal forcing, this ends the
proof.

∎

The arguments which are about to follow will depend in detail heavily on the
actual form of the iteration $\mathbb{P}_{\omega}$. The theorem will of course
be true, no matter how $\mathbb{P}_{\omega}$ does look like. To facilitate the
arguments and notation, however, we assume without loss of generality from now
on that the sequence $(\varphi_{m_{n}},\varphi_{k_{n}})$ is so chosen that in
the definition of $\mathbb{P}_{\omega}$ the cases $(a)$ and $(b)$ are
alternating. Thus whenever $n$ is even then
$(\varphi_{m_{n}},\varphi_{k_{n}})$ is such that case $(b)$ has to be applied
and whenever $n$ is odd then for $(\varphi_{m_{n}},\varphi_{k_{n}})$ case
$(a)$ is the one which one should apply. Via changing the order of
$(\varphi_{m_{n}},\varphi_{k_{n}})$, this can always be achieved.
Consequentially, at even stages $2n$ of the iteration, we define the new
notion of $n+1$-legal, while forcing with the trivial forcing; on odd stages
$2n+1$, we use the $n+1$-legal forcing to force that $\varphi_{m_{2n+1}}$ and
$\varphi_{k_{2n+1}}$ have non-empty intersection and then code the ordinal
$\alpha_{2n+1-n}=\alpha_{n+1}$ first as a real $r$ and then the quadruple
$(r,1,m_{2n},k_{2n})$ (as $h(l_{n})=2(n-1)$, hence $h(n+1)=2n$) into
$\vec{S^{1}}$.

A consequence of the last lemma (and our assumption on the form of
$\mathbb{P}_{\omega}$) is that for every even natural number $2n$, there is a
final stage in $\mathbb{P}_{\omega}$ where we create new codes of the form
$(r_{\alpha},1,m_{n},k_{n})$. Indeed, by the definition of $l_{n+1}$-legal, no
codes of the form $(r_{\alpha},1,m_{n},k_{n})$ are added by $l_{n+1}$-legal
forcings and we have that

$\displaystyle\alpha_{n}=max\\{\alpha\,:\,\exists r_{\alpha}$
$\displaystyle\text{ which codes }\alpha\text{ and
}(r_{\alpha},1,m_{2n},k_{2n})$ $\displaystyle\text{ is coded into
}\vec{S^{1}}\\}.$

To introduce a useful notion, we say that a real $x$, which is coded into an
$\omega$-block of $\vec{S^{1}}$ or $\vec{S^{2}}$, has starting index $\beta$,
if the index of the first Suslin tree of the $\omega$-block, which is used to
code $x$ is $\beta$.

######  Lemma 5.3.

In $W[\mathbb{P}_{\omega}]$ for every $n\in\omega\backslash 0$, there is only
one ordinal $\alpha<\omega_{1}$, namely $\alpha_{n}$ which has a code of the
form $(r_{\alpha},1,m_{2n},k_{2n})$ written into an $\omega$-block of elements
of $\vec{S^{1}}$ with starting index $>\alpha_{n-1}$.

###### Proof.

This is just a straightforward consequence of the definition of the iteration
and of our assumption on the form of $\mathbb{P}_{\omega}$. For $n=1$, note
that $\alpha_{0}$ is the unique ordinal for which $(r_{\alpha},1,m_{0},k_{0})$
is coded into $\vec{S^{1}}$. Then the next forcing $\mathbb{P}(2)$ is trivial
while 2-legal is defined and the forcing $\mathbb{P}(3)$ first forces
$\varphi_{m_{3}}$ and $\varphi_{k_{3}}$ to intersect without creating any code
of the form $(r_{\alpha},1,m_{0},k_{0})$ or $(r_{\alpha},1,m_{2},k_{2})$,
computes $\alpha_{1}$ and writes $(r_{\alpha_{1}},1,m_{2},k_{2})$ into
$\vec{S}^{1}$ with starting index greater than $\alpha_{0}$. As all later
factors of the iteration are 2-legal, there will be no new codes of the form
$(r_{\alpha},1,m_{2},k_{2})$, hence $\alpha_{1}$ is the unique ordinal for
which $(r_{\alpha},1,m_{2},k_{2})$ is written into $\vec{S^{1}}$ with starting
index greater than $\alpha_{0}$.

The argument for arbitrary $n$ works exactly the same way with the obvious
replacements of letters.

∎

######  Lemma 5.4.

In $W[\mathbb{P}_{\omega}]$, every ordinal $\alpha_{n}$ is
$\Sigma^{1}_{3}$-definable.

###### Proof.

This is by induction on $n$. For $n=0$, $\alpha_{0}$ is the unique ordinal for
which $(r_{\alpha},1,m_{0},k_{0})$ is coded into $\vec{S^{1}}$. This can be
written in a $\Sigma^{1}_{3}$-way:

$\displaystyle x=\alpha_{0}\Leftrightarrow\exists R\forall M$
$\displaystyle(|M|=\aleph_{0}\land M\text{ is transitive }\land R\in
M\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\rightarrow$ $\displaystyle M\text{
sees with the help of the coded information in }R\text{ that }$ $\displaystyle
x\text{ is the unique ordinal such that }(r_{x},1,m_{0},k_{0})\text{ is coded
in}$ $\displaystyle\text{ a block of }\vec{S^{1}}).$

Now assume that there is a $\Sigma^{1}_{3}$-formula which uniquely defines
$\alpha_{n}$, then, by the last lemma, $\alpha_{n+1}$ is the unique ordinal
which has a code of the form $(r_{\alpha},1,m_{2(n+1)},k_{2(n+1)})$ written
into an $\omega$-block of elements of $\vec{S^{1}}$ with starting index
$>\alpha_{n}$. Let $\psi$ be the $\Sigma^{1}_{3}$-formula which defines
$\alpha_{n}$, then

$\displaystyle x=\alpha_{n+1}\Leftrightarrow\psi(\alpha_{n})\land\exists
R\forall M$ $\displaystyle(|M|=\aleph_{0}\land M\text{ is transitive }\land
R\in M\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\rightarrow$ $\displaystyle
M\text{ sees with the help of the coded information in }R\text{ that }$
$\displaystyle x\text{ is the unique ordinal such that
}(r_{x},1,m_{0},k_{0})\text{ is coded in}$ $\displaystyle\text{ a block of
}\vec{S^{1}}\text{ above }\alpha_{n}).$

∎

The ordinals $\alpha_{n}$ indicate the point above which every code of the
form $(x,0,m_{2n},k_{2n})$ which is written into $\vec{S}$ respects the
assignment function $g_{m_{2n},k_{2n}}$. Indeed the iteration
$\mathbb{P}_{\omega}$, after the stage where we coded the quadruple
$(r_{\alpha_{n}},1,m_{2n},k_{2n})$ into $\vec{S^{1}}$ will be $2n-1$-legal,
just by the definition of the iteration, which means that the tail of
$\mathbb{P}_{\omega}$ will respect the assignment $g_{m_{2n},k_{2n}}$.

Finally we can form our desired universe of the $\Sigma^{1}_{3}$-separation
property. We force with $W[\mathbb{P}_{\omega}]$ as our ground model, we use a
finitely supported iteration of length $\omega_{1}$ where we force every
quadruple of the form $(x,0,m_{2n},k_{2n})$, $x\in 2^{\omega}$, into either
$\vec{S^{1}}$ or $\vec{S^{2}}$ with starting point $>\alpha_{n}$, according to
the assignment function $g_{m_{2n},k_{2n}}$. Note that, by assumption, all
pairs $(\varphi_{m_{n}},\varphi_{k_{n}})$, $n$ odd, do have a non-empty
intersection. Let $W_{1}$ denote the universe we obtain this way.

As a consequence we can define in $W_{1}$ the desired separating sets as
follows. For a pair $(\varphi_{m_{2n}},\varphi_{k_{2n}})$ we let $\psi_{n}$ be
the $\Sigma^{1}_{3}$-formula which defines $\alpha_{n}$. Now for any real $x$
we let

$\displaystyle x\in
D_{m_{2n},k_{2n}}\Leftrightarrow\psi(\alpha_{n})\land\exists R\forall M$
$\displaystyle(|M|=\aleph_{0}\land M\text{ is transitive }\land R\in
M\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\rightarrow$ $\displaystyle M\text{
sees with the help of the coded information in }R\text{ that }$
$\displaystyle(x,0,m_{2n},k_{2n})\text{ is coded into a block of
}\vec{S^{1}}\text{ above }\alpha_{n}).$

and

$\displaystyle x\notin
D_{m_{2n},k_{2n}}\Leftrightarrow\psi(\alpha_{n})\land\exists R\forall M$
$\displaystyle(|M|=\aleph_{0}\land M\text{ is transitive }\land R\in
M\land\omega_{1}^{M}=(\omega_{1}^{L})^{M}\rightarrow$ $\displaystyle M\text{
sees with the help of the coded information in }R\text{ that }$
$\displaystyle(x,0,m_{2n},k_{2n})\text{ is coded into a block of
}\vec{S^{2}}\text{ above }\alpha_{n}).$

Both formulas are $\Sigma^{1}_{3}$, hence the $\Sigma^{1}_{3}$-separation
property holds in $W_{1}$.

∎

##  6 Further applications and open problems

The method which was used to prove the consistency of
$\bf{\Sigma^{1}_{3}}$-separation can be applied to the generalized Baire space
as well as we will sketch briefly. Let $BS(\omega_{1})$ be defined as
$\omega_{1}^{\omega_{1}}$ equipped with the usual product topology, i.e. basic
open sets are of the form
$O_{\sigma}:=\\{f\supset\sigma\,:\,f\in\omega_{1}^{\omega_{1}},\,\sigma\in\omega_{1}^{\omega}\\}$.
The projective hierarchy of $BS(\omega_{1})$ is formed just as in the
classical setting via projections and complements. The
$\bf{\Sigma^{1}_{1}}$-sets are projections of closed sets, the
$\bf{\Pi^{1}_{1}}$-sets are the complements of the $\bf{\Sigma^{1}_{1}}$-sets
and so on.

The corresponding separation problem in $BS(\omega_{1})$ is the following:
does there exist a set generic extension of $L$ where
$\bf{\Sigma^{1}_{1}}$-sets can be separated with $\bf{\Delta^{1}_{1}}$-sets?
Our above proof can be applied here as well. All we have to do is to lengthen
our sequence of stationary sets we will use to code.

We start with $L$ as our ground model, fix our definable sequence of pairwise
almost disjoint, $L$-stationary subsets of $\omega_{1}$,
$(R_{\alpha}\,:\,\alpha<\omega_{2})$. We again split $\vec{R}$ into
$\vec{R}^{1}$ and $\vec{R}^{2}$, add $\omega_{2}$-many Suslin trees $\vec{S}$
generically and use $\vec{R}$ to code up $\vec{S}$ just as we did it in the
construction of the universe $W$, but leave out the almost disjoint coding
forcings as we quantify over $H(\omega_{2})$ anyway. Next we list the
$\bf{\Sigma^{1}_{1}}$-formulas $\varphi_{n}$ and start an $\omega_{2}$-length
iteration where we add branches of members of the definable
$(S_{\alpha}\,:\,\alpha<\omega_{2})$ whenever our bookkeeping function $F$
handles us a triple $(x,m,k)$, just as in the situation of the usual Baire
space. As there we distinguish the several cases and restrict ourselves to
_legal_ forcings, where legal is the straightforward adjustment of legal in
the $\omega$-case. The separating sets $D_{m,k}$ are defined using
$\aleph_{1}$-sized, transitive models as which witness the wanted patterns on
$\vec{S}^{1}$ and $\vec{S}^{2}.$

The sequence of the fixed $W$-Suslin trees
$(S_{\alpha}\,:\,\alpha<\omega_{1})$ is $\Sigma_{1}(\omega_{1})$-definable,
thus the codes we write into them are $\Sigma_{1}(\omega_{1})$-definable as
well. We do not have to add almost disjoint coding forcings, as we quantify
over subsets of $\omega_{1}$ in this setting anyway. All the factors will have
the ccc, thus an iteration of length $\omega_{2}$ is sufficient to argue just
as above that in the resulting generic extension $L[G]$, every pair of
$\bf{\Sigma^{1}_{1}}$-sets is separated by the according $D_{m,k}$.

The just sketched method is not limited to the case $\omega_{1}$. Indeed, if
$\kappa$ is a successor cardinal,in $L$ then we can lift the argument to
$\kappa$ as well. The proof will rely on a different kind of preservation
result for iterated forcing constructions, as we can not use Shelah’s theory
of iterations of $S$-proper forcings anymore. Also, the choice of the
definable sequence of $L$-stationary subsets of $\kappa$ has to be altered
slightly, as we can not shoot clubs in a nice way through arbitrary stationary
subsets of $\kappa$. How to solve some of the just posed problems is worked
out in [2].

What remains an interesting open problem is the following:

######  Question 1.

Can one force the $\Sigma^{1}_{1}$-separation property for $BS(\kappa)$ where
$\kappa$ is inaccessible? What if $\kappa$ is weakly compact?

One can also try to apply the techniques of this paper to
$\bf{\Sigma^{1}_{n}}$-separation for odd $n>3$. Note that due to Moschovakis,
boldface $\Delta^{1}_{4}$-determinacy implies the $\Pi^{1}_{5}$-uniformization
property, hence $\Sigma^{1}_{5}$-separation. The proof strategy of this paper
yields a better large cardinal assumption for the same conclusion. We start
with $M_{2}$, the canonical inner model with two Woodin cardinals as our
ground model and define the $\omega_{1}$-sequence of $M_{2}$-stationary
subsets of $\omega_{1}$ just as above. Note that $M_{2}$ satisfies generic
$\Sigma^{1}_{4}$-absoluteness, thus our proof of the
$\Sigma^{1}_{3}$-separation property carries over to $M_{2}$ almost without
any problems. This makes a proof of the $\Sigma^{1}_{5}$-separation property,
given the canonical inner model with two Woodin cardinals, possible. This is,
to the knowledge of the author, the currently lowest large cardinal assumption
to obtain the $\Sigma^{1}_{5}$-separation property.

The proofs of this article rely heavily on the fact that $\mathsf{CH}$ is
true. A model of the $\Sigma^{1}_{3}$-separation property with the negation of
$\mathsf{CH}$ would require a completely new approach to the problem.

######  Question 2.

Can one force the $\Sigma^{1}_{3}$-separation property over $L$ and
$\lnot\mathsf{CH}$? Is the $\Sigma^{1}_{3}$-separation property and
$\mathsf{MA}_{\omega_{1}}$ consistent?

On a last note, we turn our attention to a stronger principle, namely the
$\Pi^{1}_{3}$-uniformization property. It is well-known that
$\Pi^{1}_{n}$-uniformization implies $\Sigma^{1}_{n}$-separation, and that
boldface $\Delta^{1}_{2}$-determinacy implies $\Pi^{1}_{3}$-uniformization. It
is tempting to construct a model for the $\Pi^{1}_{3}$ uniformization property
using again just some coding forcing over $L$.

######  Question 3.

Assuming just the consistency of $\mathsf{ZFC}$, is there a model of the
$\Pi^{1}_{3}$-uniformization property?

## References

  * [1] V. Fischer and S.D. Friedman Cardinal characteristics and projective wellorders. Annals of Pure and Applied Logic 161, pp. 916-922, 2010.
  * [2] S.D. Friedman, L. Wu and L. Zdomskyy $\Delta_{1}$-Definability of the Nonstationary Ideal at Successor Cardinals Fundamenta Mathematica 229 (3), pp. 231-254, 2015.
  * [3] M. Goldstern Tools for your Forcing Construction. In: Haim Judah, editor, Set Theory of the Reals, Israel Mathematical Conference Proceedings, pp. 305-360, 1992.
  * [4] S. Hoffelner $\hbox{NS}_{\omega_{1}}$ $\Delta_{1}$-definable and saturated. To appear.
  * [5] T. Jech Set Theory. Third Millenium Edition. Springer 2006.
  * [6] V. Kanovei and V. Lyubetsky Models of set theory in which separation theorem fails, Arxiv.
  * [7] V. Kanovei and V. Lyubetsky On Harrington’s model in which Separation holds but Reduction fails at the 3rd projective level, and on some related models of Sami, Arxiv.
  * [8] A. Kechris Classical Descriptive Set Theory. Springer 1995.
  * [9] A.S. Kechris, D.A. Martin, J.R. Steel (eds.), Appendix: Victoria Delfino problems II, in: Cabal Seminar 81–85, Lecture Notes in Math. vol. 1333, Springer, Berlin, 1988, pp. 221–224.
  * [10] A. Lévy Definability in Axiomatic Set Theory. In Logic, methodology and philosophy of science. Proceedings of the 1964 International Congress, Y. Bar-Hillel, ed., North-Holland, Amsterdam, 1965, pp.127-151.
  * [11] A.D.R. Mathias Surrealist Landscape with Firgures. Periodica Mathematica Hungarica Vol. I0 (2-3), (1979), pp. 109–175
  * [12] Y. Moschovakis Descriptive Set Theory. Mathematical Surveys and Monographs 155, AMS.
  * [13] Y. Moschovakis Uniformnization in a playful Universe. Bulletin of the American Mathematical Society 77 (1971), no. 5, 731-736.