
\input amstex
\documentstyle{imcp}
\hey
\NoBlackBoxes
%



\leftheadtext{   MARTIN GOLDSTERN}
\rightheadtext{  TOOLS FOR YOUR FORCING CONSTRUCTION}

\topmatter
\title 
 Tools for your forcing construction
\endtitle
\author \byau    Martin Goldstern
    \endauthor
\address Department of Mathematics, 
Bar Ilan University, 52900 Ramat Gan, Israel
\endaddress
\curraddr 2. Mathematisches Institut, FU Berlin, Arnimallee 3, 10000
Berlin 33, Germany\endcurraddr
\email
goldstrn\@bimacs.cs.biu.ac.il, goldstrn\@math.fu-berlin.de
\endemail

%  The following items give publication information for the IMCP logo;
%  authors should NOT update these three lines.
\cvol{06}
\cvolyear{1992}
\cyear{1992}


\abstract
 A preservation theorem is a theorem
of the form: ``If  $\langle P_\alpha,
Q_\alpha:\alpha<{\delta}\rangle$ is an iteration of forcing notions,
and every $Q_\alpha$ 
satisfies $\varphi$ in $V^{P_\alpha}$, then $P_{\delta}$
satisfies~$\varphi$.''  
\\
We give a simplified version of a general preservation theorem for
countable support iteration due to Shelah. This version is
particularly useful for problems dealing with sets of reals. 
  We give several examples
of applications, among them ``countable support iteration of proper
$\omega^\omega$-bounding forcing notions is $\omega^\omega$-bounding.''
We also review the basic facts about  countable
support iteration and  proper forcing, as well as Souslin proper
forcing notions. 
\endabstract



\endtopmatter

\document
\input paging

%  This is a TeX file for "SET THEORY OF THE REALS", Proceedings of
%  the Bar Ilan Conference 1991. 
%  Paper number: 7
%  By:   Martin Goldstern
%  Title: Tools for your forcing construction
%  short title:  Tools for your forcing construction

%  which TeX: plain TeX (but be careful!)


\input mssymb
\def\on{{\restriction}}
%%%%%%%% head_preserv begin
%% input system.tex
  
% defining frakturfont  (from ams)
\edef\oldcatcode{\the\catcode`@}
\catcode`@=11
\def\relaxnext@{\let\next\relax}
\font\teneuf=eufm10

\font\seveneuf=eufm7
\font\fiveeuf=eufm5
\newfam\euffam
\textfont\euffam=\teneuf
\scriptfont\euffam=\seveneuf
\scriptscriptfont\euffam=\fiveeuf
\def\frak{\relaxnext@\ifmmode\let\next\frak@\else
 \def\next{\errmessage{Use \string\frak\space only in math mode}}\fi\next}
\def\goth{\relaxnext@\ifmmode\let\next\frak@\else
 \def\next{\errmessage{Use \string\goth\space only in math mode}}\fi\next}
\def\frak@#1{{\frak@@{#1}}}
\def\frak@@#1{\fam\euffam#1}
\catcode`@=\oldcatcode
% end define frakturfont
%%%%%% end system.tex 

%%%  input logic.etc.symbols
%%%%%%%%  file logic.etc.symbols.tex (thesis version) start %%%
%%  logic.etc.symbols.tex



%       ---- logical symbols  -----
\def\nnot{$\lnot$}
\def\impl{\mathrel{\Rightarrow}}
\def\limpl{\mathrel{\Rightarrow}}
\def\repl{\mathrel{\Leftarrow}}
\def\liff{\Leftrightarrow}
\def\lifff{\!\Leftrightarrow\!\!}
\def\land{\wedge}
\def\logand{\,\&\,}
\def\lor{\vee}
\def\proves{\mathrel{\vdash}}
\def\thinks{\models}

%   ----  set theory ---
\def\union{\bigcup}
\def\arrows{\longrightarrow}
\def\pre#1#2{{}^{#1}\!#2}
\def\erp#1^#2{\pre{#2}{#1}}
\def\to{\rightarrow}
\def\nn{n \in \omega}

\def\cut{\cap}
\def\extend{\mathord{{}^{\frown}}}
 %%%%%%%\def\extend{\!\widehat{\ \ }\!}
\def\vxtend{\!\!\!\extend}



\def\R{\hbox{I}\!\hbox{R}}
 %%  ------   sequences -------
\def\fct{\pre{\omega}{\omega}}
\def\fctfin{\pre{\omega}{\left(\finSet\right)}}
\def\finSeq{\omega^{\lless\omega}}
\def\finxSeq#1{{#1}^{\lless \omega}}
\def\finSet{{[\omega]^{\mathord{<}\omega}}}
\def\xSeq#1{\omega^{\mathord{<}{#1}}}
\def\nSeq{\omega^{\mathord{<}{n}}}
\def\zerooneseq{\pre{\omega}{2}}
\def\finzerooneseq {2^{\lless \omega}}
\def\kzerooneseq#1 {\pre{#1}{2}}
\def\ox#1{{[ #1 ]}^{\omega}}
\def\fsq#1^#2{\pre{#2}{#1}}  % used only for pmbc, Jan 27, 91
\def\oob/{$\fct$-bounding}


%%  -------- long  sequences ----
\def\sq#1#2#3{\<#1_#2: #2< #3>}
\def\sqo#1:#2{\<{#1_{#2}:#2 < \omega _{1}}>}
\def\<#1>{\hbox{$\langle #1\rangle$}}  %% new definition, avoids
					%% splitting across lines.
					%% October 1990, used in
					%% preserv. 
\def\sqn#1{\<#1_n:n<\omega>}
\def\iter{\hbox{$\<P_\alpha, Q_\alpha: \alpha<\varepsilon >$}}

%%   -- forcing  -- 
 \def\stronger{\le}
 \def\weaker{\ge}
 \def\emptycondition{\mathchoice
{\hbox{$1\!\vrule\,$}}{\hbox{$1\!\vrule\,$}}{1}{1}}
\def\lessdot{\mathrel{\mathord{<}\!\!%
  \raise 0.8 pt\hbox{$\scriptstyle\circ$}}}
\def\baar#1{\overline{#1}}

\def\ccc{\hbox{\rm ccc}}

%       --- roman symbols (like sin, max, etc.) ---

\def\sup{\mathop{\rm sup}}
\def\dom{\mathop{\rm dom}\nolimits}
\def\rng{\mathop{\rm rng}\nolimits}
\def\min{\mathop{\rm min}}

%    ---  slanted symbols -----
\def\sll{\rm}
\def\stem{{\sll stem}}
\def\support{{\sll supp}}        \def\supp{\dom}
\def\succ{{\sll succ}}
\def\Succ{{\sll Succ}}
\def\split{{\sll split}}
\def\height{{\sll ht}}
\def\sll{\rm}  %% would like \sl, but printer won't do it for
	       %% subscripts 


%%%  --- trees ----
\def\vu{\nu}
\def\trim#1^#2{{#1}^{[#2]}}





\def\eps{\mathord{\in}}
\def\lless{\mathord{<}}
\def\lleq{\mathord{\le}}

\def\bull{$\bullet$}

\def\splus{{\scriptscriptstyle +}}



\def\rvec{\hbox{$\vec R$}}
\def\rvec{\hbox{$\smash{\vec R}\vphantom{R}$}}
\def\rvec{\hbox{$\sqsubset$}}
\def\re{\sqsubset}





\def\toplus(#1){$\hbox{(#1)}^{+}$}
\def\n2{n^*}
\def\nn2{\name n^*}

\def\bool#1 {[\![ #1 ]\!]}

%
\long\def\set(#1:#2&#3){\setbox0=\hbox{#2}%
\{#1 :%\}
\vtop{\hsize=\wd0\parindent=0cm\parskip=0cm%
\rightskip=0pt plus 0.1\wd0 minus 0.1\wd0%
#2 #3$%\{
\}$}}

%\long\def\Set#1{\set({#1})}
%% % For example, write $$A:=\set( |X|: $X$ is a finite&
%% %                                 subset of bla bla, satisfying
%% %                                  etc. )$$
%


%%%%%%%% file logic.etc.symbols.tex end %%%%%%%%
%%%  end   input logic.etc.symbols

%% input format.tex
%%%%%%%%  file format.tex (thesis version) start %%%
%        ---  formatting  ---

\def\newline{\hfil\break}

%%\def\endproclaim{\medskip}

%%%  begindent-endindent = like roster-endroster
\def\begindent{\par\smallskip \begingroup \parindent=2cm}
\def\begindent{\par\smallskip\begingroup\advance\parindent by
1cm\advance\rightskip by 1.5 cm plus 1 cm minus 1 cm\relax}
\def\ite#1 {\item{(#1)} }
\def\endent{\smallskip\endgroup}


\def\quote#1\etouq{$$\vbox{\hsize=0.75\hsize\relax
\noindent #1}$$}

\def\breaklines(#1&#2){\setbox0=\hbox{#1}%
\vtop{\hsize=\wd0\parindent=0cm\parskip=0cm%
\hangindent=1cm\hangafter=1 %
\rightskip=0pt plus 0.1\wd0 minus 0.1\wd0%
#1 #2}}

%%%%%%%% file format.tex end %%%%%%%%
%% end input format.tex

%%%% input labelit
%%%%%%%%  file labelit.tex (thesis version) start %%%
\relax
%%%  this is file labelit.tex   
%    version of May 18, 1990
%    used in what is now ``sous.tex'', but not (yet) in hc.tex, bc.tex
%  \chapternumber does not quite work yet
% maybe better now, oct 9. 
% dec 9: uses \newwrite
%  feb 12:  has markitwell and markitsoso

 \newcount\secno
 \newcount\theono   
 \newcount\chapno 

\catcode`@=11
\def\exone/{0.1} %(1)
\def\extwo/{0.2} %(2)
\def\exthree/{0.3} %(2)
\def\theNotation/{0.4} %(3)
\def\exComplete/{0.5} %(4)
\def\starle/{0.6} %(4)
\def\starleFact/{0.7} %(4)
\def\densedef/{0.8} %(4)
\def\PQequiv/{0.9} %(4)
\def\pqequiFact/{0.10} %(4)
\def\interprt/{0.11} %(4)
\def\AAproblem/{0.12} %(5)
\def\randomproblem/{0.13} %(5)
\def\Cohenproblem/{0.14} %(5)
\def\composeDef/{1.1} %(6)
\def\class?/{1.2} %(6)
\def\starFact/{1.3} %(6)
\def\iterDef/{1.4} %(6)
\def\examIter/{1.5} %(7)
\def\RemIter/{1.6} %(7)
\def\factL/{1.7} %(7)
\def\factS/{1.8} %(7)
\def\FactA/{1.9} %(7)
\def\filterFact/{1.10} %(7)
\def\recRemark/{1.11} %(7)
\def\firstland/{1.12} %(8)
\def\firstandFact/{1.13} %(8)
\def\oneeight/{1.14} %(8)
\def\abFact/{1.15} %(8)
\def\subNotation/{1.16} %(8)
\def\Factfour/{1.17} %(8)
\def\filterCor/{1.18} %(9)
\def\factLL/{1.19} %(9)
\def\nonew/{1.20} %(9)
\def\cccChar/{2.1} %(10)
\def\cccCharCor/{2.2} %(10)
\def\cccComp/{2.3} %(10)
\def\cccPres/{2.4} %(10)
\def\Deltalemma/{2.5} %(11)
\def\genericDef/{3.1} %(12)
\def\trivEq/{3.2} %(12)
\def\newgeneric/{3.3} %(12)
\def\strongergeneric/{3.4} %(12)
\def\chicon/{3.5} %(12)
\def\chinames/{3.6} %(13)
\def\PROPER/{3.7} %(13)
\def\PROPERremark/{3.8} %(13)
\def\antichains/{3.9} %(13)
\def\propeq/{3.10} %(13)
\def\propeqRem/{3.11} %(14)
\def\cccEx/{3.12} %(14)
\def\propercover/{3.13} %(14)
\def\AlephOne/{3.14} %(14)
\def\elemFact/{3.15} %(14)
\def\compFact/{3.16} %(15)
\def\newPrelim/{3.17} %(15)
\def\inducL/{3.18} %(15)
\def\ShelahsThm/{3.19} %(17)
\def\quotDef/{4.1} %(17)
\def\againsub/{4.2} %(17)
\def\quotFactA/{4.3} %(17)
\def\quotFactB/{4.4} %(17)
\def\quotfactC/{4.5} %(18)
\def\intermediate/{4.6} %(18)
\def\context/{5.1} %(20)
\def\incon/{5.2} %(20)
\def\csAssume/{5.3} %(20)
\def\goodDef/{5.4} %(20)
\def\preservOne/{5.5} %(21)
\def\preserveCover/{5.6} %(21)
\def\ooExample/{5.7} %(21)
\def\interpret/{5.8} %(21)
\def\interCrem/{5.9} %(21)
\def\inconDef/{5.10} %(22)
\def\preservDef/{5.11} %(22)
\def\composeCover/{5.12} %(22)
\def\pInduction/{5.13} %(23)
\def\mainCor/{5.14} %(24)
\def\pPrelim/{5.15} %(24)
\def\clopen/{6.1} %(28)
\def\counterex/{6.2} %(28)
\def\ooDef/{6.3} %(29)
\def\ooR/{6.4} %(29)
\def\boundlemma/{6.5} %(29)
\def\boundCor/{6.6} %(29)
\def\nullSet/{6.7} %(30)
\def\outRdef/{6.8} %(30)
\def\frggaf/{6.9} %(30)
\def\outerFact/{6.10} %(30)
\def\applynull/{6.11} %(31)
\def\randDef/{6.12} %(31)
\def\starfour/{6.13} %(31)
\def\outerClaim/{6.14} %(31)
\def\randomrandom/{6.15} %(31)
\def\helprandom/{6.16} %(32)
\def\ismeager/{6.17} %(33)
\def\meagerRdef/{6.18} %(33)
\def\xy/{6.19} %(33)
\def\meagerfact/{6.20} %(33)
\def\applymeager/{6.21} %(33)
\def\whenpreserveCohen/{6.22} %(33)
\def\meagerEx/{6.23} %(33)
\def\coneDef/{6.24} %(34)
\def\LaverProp/{6.25} %(34)
\def\LaverEq/{6.26} %(34)
\def\LaverEqDef/{6.27} %(34)
\def\hNotation/{6.28} %(34)
\def\ChDef/{6.29} %(34)
\def\RhDef/{6.30} %(34)
\def\hrsdef/{6.31} %(34)
\def\SLlemma/{6.32} %(35)
\def\Hcor/{6.33} %(36)
\def\SacksDef/{6.34} %(36)
\def\SacksEq/{6.35} %(36)
\def\Souslinforcingdef/{7.1} %(38)
\def\univNot/{7.2} %(38)
\def\ssfDef/{7.3} %(38)
\def\sfRem/{7.4} %(38)
\def\genDef/{7.5} %(38)
\def\spfRem/{7.6} %(38)
\def\setUp/{7.7} %(39)
\def\PdvecDef/{7.8} %(39)
\def\PvecNot/{7.9} %(39)
\def\restDef/{7.10} %(39)
\def\corrDef/{7.11} %(39)
\def\corrconv/{7.12} %(39)
\def\restRem/{7.13} %(39)
\def\simplyGeneric/{7.14} %(40)
\def\itpropTheo/{7.15} %(40)
\def\itpropCor/{7.16} %(40)
\def\SouslinPlus/{7.17} %(41)
\def\effgendef/{7.18} %(41)
\def\effgenFact/{7.19} %(41)
\def\SacksEx/{7.20} %(41)
\def\splitDef/{7.21} %(42)
\def\Dlemma/{7.22} %(42)
\def\coroffronts/{7.23} %(42)
\def\finalrem/{7.24} %(42)
\def\newcontext/{8.1} %(43)
\def\finAssumption/{8.2} %(43)
\def\moClosed/{8.3} %(43)
\def\finiteTheo/{8.4} %(43)
\def\finExone/{8.5} %(43)
\def\finbd/{8.6} %(44)
\def\finExtwo/{8.7} %(44)
\def\secondfact/{8.8} %(44)
\def\IteratedForcing
{1}
\def\GraysThesis
{2}
\def\pmbc
{3}
\def\JechSt
{4}
\def\SouslinForcing
{5}
\def\DeltaOneThree
{6}
\def\KunenMiller
{7}
\def\Kunen
{8}
\def\Chaz
{9}
\def\ProperForcing
{10}
\def\ProperImproper
{11}
\def\CLXXVII
{12}
\def\IteratedCohen
{13}



\newwrite\mgfile
\openin\mgfile=\jobname.mg
\ifeof\mgfile \message{No file \jobname.mg}\closeout\mgfile \else
\input \jobname.mg\fi

\openout\mgfile=\jobname.mg

\newif\ifproofmode
\proofmodefalse            %may want to reset this in main body of paper



\def\chapternumber{}
\def\printchapternumber{}

\def\@nofirst#1{}

\def\neusection{\advance\secno by 1\relax \theono=0\relax}
\def\neuchap{\advance\chapno by 1\relax\secno=0\relax\theono=0\relax}

\neuchap


\def\labelit#1{\global\advance\theono by 1%
\global\edef#1/{%
\chapternumber%                         %%%%% chapno here
\number\secno.\number\theono}%
\write\mgfile{\@definition{#1/}}}

%%  for example, if \secno=1, \theono=3, 
%%  \labelit{\thisTheorem}   will make \thisTheorem/ and abbreviation
%%  for 1.4, and \theono will be advanced to 4. 
%%  \neusection sets \theono to 0, so that is ok.  
%%  Assuming the main file is called paper.tex, it will write this
%%  abbreviation into the file paper.mg

% the following is a modified version of ppro
\def\pprop#1/#2{\labelit{#1}%
\smallbreak\noindent%
%%%%%%%%%%%%%%%%%%%%%%\@markit{#1}%
{\bf #2\ #1/:}}

\def\@definition#1{\string\def\string#1{#1}
\expandafter\@nofirst\string\%\printchapternumber
(\the\pageno)}

\def\@markit#1{\leavevmode
\ifproofmode\llap{{\tt \expandafter\@nofirst\string#1\ }}\fi
{\bf  \printchapternumber#1/\ }}


\def\labelcomment#1{\write\mgfile{\expandafter\@nofirst\string\%---#1}}
\catcode`@=12


%%%%%%%% file labelit.tex end %%%%%%%%
%%%% end input labelit

%%%% input name
%% notforces, modified 

\newbox\notbox
\setbox\notbox\hbox{\ $\not$}
\wd\notbox=0cm


\def\notforces{{\copy\notbox\forces}}
\def\forces{{\mathrel\Vert\joinrel\mathrel-}}
\def\Forces_#1``#2''{\forces_{#1}\hbox{``#2''}}
\def\forcess{\mathop\forces\limits}


\def\name#1{\mathchoice%
{\setbox0=\hbox{$\displaystyle #1$}% 		displaystyle
\setbox1=\vtop{\ialign{##\crcr
$\hfil{\displaystyle #1}\hfil$\crcr\noalign{\kern2pt%
\nointerlineskip}$\hfil\mathord{\displaystyle \sim}%
\hfil$\crcr\noalign{\kern2pt\nointerlineskip}}}%
\vphantom{\copy1}%
\setbox2=\hbox{$\displaystyle \sim$}%
\wd1=\wd0\dp1=0cm\ifdim\wd2>\wd1 \wd1=\wd2\else\relax\fi
\ht1=\ht0\relax
\box1}%
{\setbox0=\hbox{$\textstyle #1$}%		textstyle
\setbox1=\vtop{\ialign{##\crcr
$\hfil{\textstyle #1}\hfil$\crcr\noalign{\kern1.2pt%
\nointerlineskip}$\hfil\mathord{\textstyle \sim}%
\hfil$\crcr\noalign{\kern1.5pt\nointerlineskip}}}%
\vphantom{\copy1}%
\setbox2=\hbox{$\textstyle \sim$}%
\wd1=\wd0\dp1=0cm\ifdim\wd2>\wd1 \wd1=\wd2\else\relax\fi
\ht1=\ht0\relax
\box1}{\setbox0=\hbox{$\scriptstyle #1$}%	scriptstyle
\setbox1=\vtop{\ialign{##\crcr
$\hfil{\scriptstyle #1}\hfil$\crcr\noalign{\kern1pt%
\nointerlineskip}$\hfil\mathord{\scriptstyle \sim}%
\hfil$\crcr\noalign{\kern2.1pt\nointerlineskip}}}%
\setbox2=\hbox{$\scriptstyle \sim$}%
\vphantom{\copy1}%
\wd1=\wd0\dp1=0cm\ifdim\wd2>\wd1 \wd1=\wd2\else\relax\fi
\ht1=\ht0\relax
\box1}{\setbox0=\hbox{$\scriptscriptstyle #1$}%	scriptscriptstyle
\vtop{\ialign{##\crcr
$\hfil{\scriptscriptstyle #1}\hfil$\crcr\noalign{\kern1pt%
\nointerlineskip}$\hfil\mathord{\scriptscriptstyle \sim}%
\hfil$\crcr\noalign{\kern1.5pt\nointerlineskip}}}%
}}


{\catcode`\@=11\gdef\neubox{\alloc@ 4\box \chardef \insc@unt}
\gdef\neudimen{\alloc@ 1\dimen \dimendef \insc@unt}}

\def\assign#1{\neubox\current\neudimen\thedepth
\setbox\current=\hbox{$\name #1$}
\thedepth=\dp\current
\dp\current=0cm
\edef\next{\noexpand\edef
\csname n#1\endcsname{\vrule width 0cm height 0cm depth \the\thedepth
		\noexpand\copy\the\current}}\next} 


\def\nofirst#1{}
\def\assignp#1{\neubox\current\neubox\prepend
\setbox\current=\hbox{$\name #1$}
\setbox\prepend=\copy\current
\wd\prepend=0cm
\dp\current=0cm
\edef\next{\noexpand\edef
\csname
n\expandafter\nofirst
\string#1\endcsname{\noexpand\copy\the\prepend\copy\the\current}}\next}

\assignp\tau
\let\nt=\ntau
\assign f
\assign g
\assign q
\assign Q
\assign p
\assignp\sigma
\assignp\alpha
\assign r
\assign x
\assign y
\assign k


  %%% Example:  \assign x   defines a control sequence \nx, whose
  %%% value is an hbox containing an $\name x$ with a tilde below.
  %%% The point is that this has to be computed only once.  Using \nx
  %%% just results in copying the hbox.   (Disadvantages: 1: Uses
  %%% storage, 2: Cannot use this for sub/superscripts.  3:  Cannot
  %%% use it on fractions, as depth=0.)
  %%%  CAUTION ! \nx_n works fine, but {\nx}_n doesn't !


%

\def\compile#1#2{\neubox\current
\setbox\current=\hbox{$#2$}
\edef#1{\noexpand\copy\the\current}}

%%%% end input name

%%%% input fraktur
%%%%% fraktur.tex  thesis version
\let\fraktur\frak
\def\c{{\fraktur c}}   %% should use mathchardef - but what's the use if
		    %% we have only 10pt anyway? 

\def\R{\hbox{I}\!\hbox{R}} %% .. june 25, for pmbc 
\def\P{{\fraktur P}}
\let\polishL\L
\let\polishl\l
\def\L{\hbox{I}\!\hbox{L}}  %% Laver forcing June 11, pmbc
                  %% the only other one-letter command sequence used
		  %% in pmbc is \S. 
\def\S{{\Bbb S}}
\def\F{{\cal F}}  %% the omega-1-club filter on omega-2, June 18, pmbc
\def\Q{{\bf Q}}   %% the rationals, Oct 23, 1990, preserv
\def\C{{\bf C}}   %% a closed set \subseteq \fct, Nov 1, preserv 
\def\U{{\cal U}} %% ultrafilter, Nov 7, ch0/1 

%%\def\b{{\bf b}}   %% bounding number, Nov 8, ch0/1 
\def\b{{\fraktur b}}
%%\def\d{{\bf d}}   %% dominating number, Nov 8, ch0/1 
\def\d{{\fraktur d}}
\def\J{{\cal J}}  %% any ideal on \R, Nov 12, ch0
\def\H{{\cal H}}  %% dominating family
\def\A{{\cal A}}  %% p-points, in smz

%%% end of fraktur.tex 
%%%% end input fraktur


%%%% input dst
%%%%%%%%  file dst.tex (thesis version) start %%%
% macros for descriptive set theory


\def\PA{{\bf \Sigma^1_1}}
\def\CA{{\bf \Pi^1_1}}
\def\PCA{{\bf \Sigma^1_2}}
\def\field{{\it field}} 

\def\meager{{\cal M}}  
      %  = the ideal of meager sets 
      %   M for meager, or C for category?
\def\measure0{{\cal N}}
      %  = the ideal of null sets 
      %  N for null, or M for measure?  
%%%%%\def\SMZ/{\hbox{$\kappa_U(\smz)=\c$}} 
      % = all small sets are smz. 
      %  Haim writes SMZ for this. 
%%%%%\def\SMZ/{\hbox{\bf SMZ}}
\def\SMZ/{\hbox{$\Unif(\smz)$}}
\def\smz{{\cal S}}
      % = the ideal of strong measure zero sets.

\def\Add{{\bf Add}}
\def\Cov{{\bf Cov}}
\def\Unif{{\bf Unif}}
%%%%%%%% file dst.tex end %%%%%%%%

%%%% end input dst



\def\sf{f^*}
\def\nsf{\name f^*}

\def\ffk{\<\sf_0, \ldots, \sf_{k-1}>}
\def\nffk{\<\nf_0, \ldots, \nf_{k-1}>}

\def\bffk{\bar f^*}
\def\bsffk{\bar f^*}
\def\bpffk{\bar f'}
\compile\bsnffk{\name{\bar f}^*}
\compile\bnffk{\name{\bar f}}
\compile\bOnenff{\name{\bar f}^1}
\compile\bTwonff{\name{\bar f}^2}


\def\nff#1 #2 {\<\nf_0^{#1}, \ldots, \nf_{#2}^{#1}>}
\def\ff#1 #2 {\<f_0^{#1}, \ldots, f_{#2}^{#1}>}
\def\ffk{\ff {*} {k-1} }
\def\nffk{\nff {} {k-1} }
\def\pffk{\<f_0', \ldots, f_{k-1}'>}
\def\nsffk{\nff {*} {k-1} }


%\def\fct{\pre{\omega}{\omega}}
%\def\fctfin{\pre{\omega}{\left(\finSet\right)}}

%%%%%%%% head_preserv end 


%\proofmodetrue  \relax \advance\hoffset by 0.7 true cm

%% input head_souslin
%%%%%%%%%%%   file head_souslin.tex (Helsinki version) start %%%%%%

\def\dvec{{\vec{d}}}
\def\dveca{{\vec{d}\on \alpha}}
\def\cvec{{\vec{c}}}
\def\cveca{{\vec{c}\on \alpha^S}}
\def\dvecg{{\vec{d}\on\gamma}}
\def\cvecg{{\vec{c}\on \gamma^S}}
\def\evec{{\vec{e}}}
\def\eveca{{\vec{e}\on \alpha^S}}
\def\dval#1{d_{#1}[G_{#1}]}
\def\cval#1{c_{#1^S}[G'_{#1}]}
\def\iter{\hbox{$\<P_\alpha,Q_\alpha:\alpha<{\varepsilon}>$}}
\def\flt#1on #2 #3{#1\on (#2, #3)}
\def\flta#1on #2 #3{#1\on (#2, #3, {\cvec}\on\alpha^S, {\dvec}\on\alpha)}
\def\collapse{R}
\def\splus{{\scriptscriptstyle +}}
\def\field{{\hbox{field}}}
%%%%%%  file head_souslin.tex end %%%%%%%%%%%%%%%%%%
%% end input head_souslin








%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%                      %%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%  end of definitions  %%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%                      %%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
^^L
%% history: original style -- from my thesis.  Then changed to look
%% similar to other proceedings papers. 

\font\huge=cmr10 scaled \magstep2
\font\small=cmr8 scaled \magstep0


\def\beep{\vrule height 0.1pt width 0.3\hsize\relax}




%% history: original style -- from my thesis.  Then changed to look
%% similar to other proceedings papers. 

\font\huge=cmr10 scaled \magstep2
\font\small=cmr8 scaled \magstep0

\long\outer\def\PROCLAIM#1/#2:#3\ENDPROCLAIM
{\pprop{#1}/{#2}{\it #3}\smallskip}



\let\em\it





\beginsection 0\quad Introduction

The main objective of this paper is to present a simplified version of
Shelah's preservation theorems.  We hope that the reader will find
here  powerful tool for his/her forcing constructions, as well as good
open problems in this abstract area of mathematical research: The
study of (iterated) forcing. 
%



Iterated forcing is a powerful tool for proving independence results.
       In an iterated forcing argument the ``ground model'' $V_0$ is
       first extended to a model $V_1$ using some forcing notion~$Q_0$.
Then $V_1 $ is extended to some universe $V_2$, using 
       some forcing notion $Q_1$ in $V_1$, etc.   After $\omega$ many
       steps, a model $V_\omega$ containing $\bigcup_n V_n$ is
       constructed, and the iteration can continue---usually up to
       $\omega_1$, $\omega_2$ or some large cardinal. 


In an iterated forcing argument there two main points we have to take
care of: 
\begindent
\ite 1 In each extension by a single forcing notion $Q_i$ we have to add
       certain generic objects that we want to have present in the
       final model. 
\ite 2 At no stage are we allowed to add certain objects that we do
       not want to have in the final model. 
\endent


The argument given to deal with (1) usually depends heavily on the
       special properties of the forcing notions~$Q_i$.  Similarly,
       dealing with (2) at a successor step $i+1$ is  done by
       arguments that are characteristic for the forcing notion~$Q_i$.

A ``preservation theorem'' is a theorem that deals with  problem (2)
       at limit stages, i.e.\ a theorem ensuring that no
       ``unwanted'' objects are introduced at limit stages whenever 
       all 
the forcing notions $Q_i$ that are used satisfy certain
       ``niceness'' conditions. 


For example, the problem of preserving 	certain cardinals and
       cofinalities is an instance of  (2).     The earliest
       preservation theorem we are aware of is  the following
       ([from~\IteratedCohen])

\quote The finite support limit of an iteration in
       which all iterands satisfy the countable chain condition also
       satisfies the countable chain condition (and thus preserves 
       cofinalities and cardinals) 
\etouq

\medskip

The corresponding theorem for countable support iteration is the
       following ([\ProperForcing]): 
\quote The countable support  limit of an iteration in
       which all iterands are proper is itself proper (and thus does
       not collapse $\aleph_1$).  Also, starting from CH,  if the
       length of the iteration 
       is $\le \aleph_2$ and all iterands have size $\le \aleph_1$,
       then the limit satisfies the $\aleph_2$-cc, so all cardinals
       and cofinalities are preserved.        
\etouq




\bigskip

The following example shows that the question of what reals are
  introduced in limit stages of an iteration is usually nontrivial: 


\PROCLAIM\exone/Example 1:  Assume that $V_0$ satisfies CH,  $Q_0$ adds
no new
  reals to $V_0$, $Q_1$ adds $\aleph_1^{V_0}$ many new reals to $V_1$,
  $Q_2$ adds $\aleph_2^{V_0}$ many new reals to $V_2$, etc.  Let
  $P_n:=Q_0 * Q_1 * \cdots *Q_{n-1}$.   So $V_n$ is the generic
  extension of $V_0$ by~$P_n$. 

 Then in $V_\omega$ we will have at least $\aleph_\omega$ many new
  reals. But as the cofinality of the continuum must be uncountable,
  this means that in $V_\omega$ will have at least
  ${\aleph_{\omega+1}^{V_0}}$ many new reals.   Since only
  $\aleph_\omega$ many of them appear in  intermediate stages,
  ``most'' of these reals appear only in the limit stage.  This
  shows that it is not trivial to keep control over which reals are
  added in a limit stages by controlling what reals are added in
  intermediate stages. 
\ENDPROCLAIM


\PROCLAIM\extwo/Example 2:  Consider an iteration $\<P_n, Q_n:n<\omega>$,
  where for all $n$, $\forces_{P_n} $``$ Q_n$ is nontrivial, i.e.,
       contains   incompatible   conditions.'' 
  
If we define $V_\omega$ as $V^{P_\omega}$, where $P_\omega$ is the
  finite support limit of the iteration 
sequence
  $\<P_n, Q_n:n<\omega>$, then
  (no matter what the forcing notions $Q_n$ are), $P_\omega$ will add
  Cohen reals over the ground model.  (Let $\forces_n$``$q^0_n\perp_{Q_n}
  q^1_n$,'' then the function $f: \omega\to 2$, defined by $f(n)=0 \liff
  q^0_n\in G(n)$ will be a Cohen real, where $G(n)$ is the generic
  filter on~$Q_n$.)	
\ENDPROCLAIM




This example shows an {\bf inherent limitation of the method of finite 
  support iteration}:  In limit stages of cofinality $\omega$, Cohen
  reals are always added.  


%%In this introduction we will only consider countable support iteration.
  The general problem of whether Cohen reals can be added in a limit
  stage of a {\bf countable support iteration}  is {\bf open}: 

\quote Assume $P_\omega$ is the countable support iteration of $\<P_n,
  Q_n: n<\omega>$, where for all $n$ we have: 
      $$ \forces_{P_n} \hbox{``There are no Cohen reals over $V$''}$$
  Does this imply $ \forces_{P_\omega} \hbox{``There are no Cohen
  reals over $V$''}$? 
\etouq

At this moment it seems impossible to apply the preservation theorem
  we prove below to this problem directly.  There are, however,
  stronger properties (of forcing notions) than ``not adding Cohen
  reals'', that can be shown to be preserved under  countable support
  iteration.  The best known of them are ``$\fct$-bounding'' and
  ``Laver property.'' (see \ooDef/ and \LaverProp/, below) 
   

\medskip
\PROCLAIM\exthree/Remark:
The same proof that shows that finite  support iteration always adds
      Cohen reals in stage  $\omega$ also shows an
{\bf     inherent limitation of countable support iteration}:  In stage
      $\omega_1$ (or indeed at any stage of cofinality $\omega_1$) we
      add an     ``$\omega_1$-Cohen set,'' i.e., a generic filter
      for the forcing notion $Fn(\omega_1, 2, \omega_1)$ of all
      countable partial functions from $\omega_1$ to~$2$.   At first
      generic filters for this forcing notion seem innocent for
      problems concerning sets of reals, as $Fn(\omega_1,2,\omega_1)$
      does not add any reals.  However, a simple density argument
      shows that the continuum of the ground model is collapsed
to~$\aleph_1$.  This makes it impossible to have $\c>\aleph_2$ at 
      any limit stage of uncountable cofinality during a countable
      support iteration. 
\ENDPROCLAIM

\bigskip

For a specific  example of where a preservation theorem can be used,
  consider the problem of proving 
\quote Con($\Cov(\measure0)$ + $\b=\c$ + $\lnot\Unif(\measure0)$) \etouq
using iterated forcing.



Explanation: 
\item{} $\Cov(\measure0)$ means: the real line cannot be
       covered by less than $\c$ (=continuum) many sets from
      $\measure0$, the ideal of null (=measure zero) sets. 
\item{}  $\b=\c$ means:
       Whenever $F \subseteq \fct$ is a family of less than $\c$ many
       functions, there exists a function $g$ bounding every element
       of $F$, where ``$g$ bounds $f$'' means $\exists k \, \forall
       n\ge k\,\, g(n) > f(n)$. 
\item{} $\lnot\Unif(\measure0)$ means that there is  a set of reals of
       cardinality $<\c$ that does not have  measure zero.


\medskip
There are two approaches to get a model satisfying the condition
       above: 

\begindent
\ite 1 Start with  a model where (some big fragment of) Martin's axiom
       holds and $\c$ is big. 
       Then construct a short iteration of length~$\kappa<\c$. In each
       iteration stage $i<\kappa$, add a real $r_i$ in such a way that
       at the end the set $\{r_i:i<\kappa \}$ is nonmeasurable. Preserve
       enough of Martin's axiom to ensure that in the final model,
       $\Cov(\measure0) + \b=\c$ holds. 
\ite 2 Start with the constructible universe $L$  (or some model
       satisfying enough of GCH) and construct a long iteration of
       length $\kappa> \aleph_1$. In each stage $i<\kappa$, add a
       function $f_i$ and a real $r_i$ such that $f_i$ is not bounded
       by any function constructed so far, and $r_i$ is not in any
       measure zero set constructed so far.  Assuming that no new
       reals appear in stage $\kappa$, in the final model we will have
       $\c=\kappa$, the set $\{r_i:i<\kappa\}$ will be a set of reals
       that cannot be covered by $<\kappa $ many measure zero sets,
       and $\{f_i:i<\kappa \}$ will witness~$\b=\c$.  We have to take
       care not to cover the set of constructible reals by a measure
       zero set.   This will ensure that there is a non-null set of
       size $\aleph_1< \c$. 
\endent

\bigskip

At the end of section 6, we will consider approach (2). Since a Cohen
real makes the 
  set of all old reals a measure zero set, we should not add Cohen
  reals during the iteration.  So we cannot use finite support
  iteration.

$r_i$ will be a random real. It is easy to see that any set that is
  not of measure zero in $V$  will also not be of measure zero after
  adding a random real. 

$f_i$ will be a Laver real. [\KunenMiller] showed that Laver reals
  also do not make non null sets into null sets. 

This two observations show that if in stage $i$, the set of
  constructible reals was not null, the also in stage $i+1 $ this
  property will hold.   So it remains to show that in limit stages
  the constructible reals are not covered by a measure zero set. For
  this purpose we will use the iteration theorem proved below (\mainCor/),
  with parameters given in application 2 (\outRdef/, \randDef/)


\bigbreak\bigskip

\PROCLAIM\theNotation/Notation for forcing: 
\rm
    A forcing notion $P =
\<P, \le_P, \emptycondition_P>$ is a set $P$ equipped with a
transitive reflexive relation $\le_P$ and a greatest element
$\emptycondition_P$.  $\forces_P$ denotes the forcing relation of~$P$.

{\bf  We interpret $p \weaker q$ (or $p\weaker_P q$)  as ``$q$ extends
  $p$,''  ``$q$ is stronger than $p$,'' or ``$q$ has more information
  then~$p$.''}    $p$ is ``incompatible'' with $q$  ($p\perp q$ or
  $p\perp_P q $) means~$\lnot \exists r\in P: p \weaker r \logand q
  \weaker r$.

   Note that $p \perp q \, \liff\, p \,\forces q\notin G_P$. 

		
A set $D \subseteq P$ is called dense if $\forall p\in P \, \exists
q\in D: q \stronger p$.  $D$ is open iff $\forall q\in D\,\, \forall r
\stronger q: r\in D$.   $D$ is an antichain if $\forall p,q\in D:
p\not=q \limpl p\perp q$. $D$ is predense if $\forall p\in P\,\exists
  d\in D\,\, d\not\perp p$.   $D$ is predense below $p$ iff $\forall q
\stronger p \, \exists d\in D \,\, d\not\perp p$. 


$D$ is a ``filter'' if any two elements
  of $D$ are compatible with a witness in $D$, i.e.\ $\forall p,q\in
D\,\exists t\in D \,\, p \weaker r\logand q \weaker r$. 



If $V$ is a model of set theory, $G \subseteq P$ is called generic
(over $V$) (for $P$), if $G\cut D\not=0$ for all dense~$D\in V$.   We
often omit mentioning  $P$ and/or $V$, if the context makes it clear
what $P$ and $V$ should be. 





The class of $P$-names is defined by $\in$-recursion:  $\nx$ is a
  $P$-name iff every element of $\nx$ is a pair of the form $\<\name
  y,p>$ where $\name y$  is a $P$-name and~$p\in P$. 


 To avoid having
  to work with a proper class, we introduce an equivalence relation
  $\equiv$ on   $P$-names by $\name x \equiv \name y$ iff
  $\emptycondition_P\forces_P 
  \name x = \name y$, and choose a set of  representatives from each
  class, say, those   of least possible rank. 

  So for example,  the {\bf set} of $P$-names for functions from
  $\omega$ to $\omega$ is the set of all representatives $\nx$ such
  that $\emptycondition\forces \nx:\omega\to \omega $.  (It can easily
  be seen that this is in fact a set.)







 Usually we write (variables for) $P$-names with a tilde, as in~$\nx$. 
  For a $P$-name $\name{x}$ and a generic $G \subseteq P$, we let
        $\name{x}[G]$ be the evaluation of $\name{x}$ by $G$:
$$ \nx[G] := \{\ny[G]: \<\ny,p>\in \nx, p\in G\}$$
  But if
        $M$ is a model of a large fragment of ZFC, then we let
        $M[G]:=\{ \name{x}[G]: M \thinks \hbox{$\name{x}$ is a
        $P$-name}\}$.  Sometimes (if $G$ is clear from the context) we
        use for the evaluation of a name by $G$ the same variable as
        the one used for the name, but leaving out the tilde, i.e., if
        $G$ is given, $x$ abbreviates $\nx[G]$, $p$ abbreviates
        $\np[G]$, etc. Similarly $p^1_n$ is $\np^1_n[G]$, etc.)

For an element $x$ of $V$, $\widehat x$ or $(x)\widehat{\ }$ is the
standard $P$-name for 
$x$, $\widehat x := \{\<\widehat y, \emptycondition_P>: y\in x\}$ but we
  usually write $x$ for~$\widehat x$. 
\medskip

  For a forcing $P$, $G_P$ is (depending on the context) either  
   $= \{\<\widehat p,p>: p \in P \} $, the canonical
   name for the generic object (also called the generic filter) added
   by $P$,  or a variable ranging over all $V$-generic filters $G
   \subseteq P$.     

\ENDPROCLAIM
We will freely use the following ``existential completeness lemma'',
sometimes without explicitly mentioning it: 

\PROCLAIM\exComplete/Lemma: 
   For any forcing $P$, any formula
   $\varphi(x)$ there is a name $\ntau$ such that 

$$ \hbox{ $\emptycondition \forces \exists x\, \varphi(x) \
       \liff \ \varphi(\ntau)$} $$
\ENDPROCLAIM
(See [\Kunen] for a proof.)


We will also need the following well-known definitions and facts about
forcing:  


\PROCLAIM\starle/Definition:  For $p,q$ elements of a  forcing notion $P$,
	we define $p \weaker^* q$ iff for all $r \stronger q$, $r$ is
	compatible with~$p$. 
\ENDPROCLAIM
\PROCLAIM\starleFact/Fact:  $p \weaker^* q $ iff $q \forces_{P} p\in G_P$.
	In particular, $p \weaker q $ implies $p \weaker^* q$.
\ENDPROCLAIM

Most properties of $\le$ are also shared by~$\le^*$. E.g., $p\perp q$
iff there is no condition $r$ satisfying $p \weaker^* r $ and $q
\weaker^* r$.  Also, if $p \forces \varphi$, and $p \weaker^* q$, then
$q \forces \varphi$.  



\PROCLAIM\densedef/Definition:  If $P,Q$ are forcing notions, we say that
	$i:P\to Q$ is a ``dense* embedding'', iff
\begindent
\ite 1 $\forall p_1,p_2\in P$: $p_1 \le^*_P p_2$ iff~$i(p_1)\le_Q^*
	i(p_2)$.  (``$i$ is an embedding with respect to $\le^*$'')
\ite 2 $\forall q\in Q\, \exists p\in P: q \weaker^* i(p)$.  (``$i$ is
  dense*'') 
\endent
      Note that $i$ is not necessarily 1-1. 
If (1) and (2) hold with $\le $ instead of $\le^*$, then we say that
  $i$ is a dense embedding. 
\ENDPROCLAIM



\PROCLAIM\PQequiv/Definition:  If there exists a dense* embedding $i:P\to
	Q$, we say that $P$ and $Q$ 
	are equivalent, and we write $P\approx Q$. 
\ENDPROCLAIM


  This is justified by the following fact: 


\PROCLAIM\pqequiFact/Fact:  Assume $i:P\to Q$ is a dense* embedding.  Then
	whenever $G \subseteq P$ is generic, then the set~$H$ defined
	by
  $$H:=\{q\in Q: \exists	p\in G, i(p) \stronger q\}$$
is generic for~$Q$.   Conversely, if a set $H \subseteq Q$ is generic,
	then the set~$G$, defined by 
$$ G:=\{p\in P: i(p)\in H\}$$
is generic for~$P$. 

Moreover, in both cases $V[G]=V[H]$, and there is a canonical
	translation function that maps $P$-names $\nx$ to corresponding
	$Q$-names $\nx'$, and conversely.  We will often identify names with
	their image under this translation function. 

We have that $p \forces_P \varphi(\nx)$ iff $i(p)
	\forces_Q\varphi(\nx')$.  
\ENDPROCLAIM


The proof is a routine computation. 



\medskip
Finally, we define the concept of an ``interpretation'': 


\PROCLAIM\interprt/Definition: Assume $Q$  is  a forcing notion,   $\nf$,
   is a  $Q$-name of a  functions in $ \fct$, $f^*$  is a function in
   $\fct$, $\sqn p $ 
   an increasing  sequence of conditions.  

We say that $\sqn p$
   interprets  $\nf $ as $f^*$, if  for all $n$, 
        $p_n \forces \nf\on n  =  f^*\on n$.  

We say that $f^*$ is an interpretation of $\nf$ if there exists an
  increasing sequence as above. 
\ENDPROCLAIM


\bigskip


The main theorem (\mainCor/) of this paper is a simplified version of
a theorem of Shelah ([\ProperImproper, XVIII]).  See also
[\ProperForcing, V, VI], [\CLXXVII] and [\KunenMiller] for
  precursors. 
   The proof presented here is a joint work  of Judah and the author.

  Theorem \finiteTheo/ has been proved for various
instances by several people. 

Souslin forcing and Souslin Proper forcing were  introduced in
[\SouslinForcing].  
\bigskip
\begingroup
\parskip=0cm
 Contents of this paper: 

In section 1, we give a review of composition and iteration of forcing
   notions in a general context. 

In section 2 we introduce finite support iteration and  show that the
   countable chain condition is preserved in finite support limits. 

In section 3 we explain the concept of properness, and give a
   simple proof of Shelah's theorem ``properness is preserved under
   countable support iteration.''  This proof will serve as a basis
   for the proof of the preservation theorem in section 6. 

In section 4  we continue the review of countable and finite support
   iteration, by considering the relationship between an intermediate
   model and the final model. 


In section 5 we formulate and prove a general preservation for
   countable support iteration.



In section 6 we show how to apply the preservation theorem for
   countable support iteration by giving several examples of
   properties that can be preserved in this framework.  

In section 7 we review the concept of ``Souslin Proper forcing'',
and we prove the corresponding preservation theorem. 

In section 8 we formulate and prove a general preservation theorem for
finite  support iteration, and we give examples. 




Those readers who are interested only in finite support iteration can
   skip section 3 and all references to countable support iteration in
   section 4 without loss of continuity.   A dual remark applies to
   readers only interested  in countable support iteration. 


\bigskip
\bigskip
We conclude this introduction by mentioning some open problems
concerning countable support iteration and proper forcing: 

\PROCLAIM\AAproblem/Problem (Judah):  Is ``MA(Axiom A) + projective
measurability'' equiconsistent with the existence of 2 weakly compact
cardinals? 
\ENDPROCLAIM

From [\IteratedForcing] it essentially follows that MA(Axiom A) is
equiconsistent with one weakly compact cardinal. 


\bigskip

\PROCLAIM\randomproblem/Problem (Judah):  Find a sequence $\< \re_n:n\in \omega>$,
such that ``$Q$ 
preserves $\rvec$'' iff $Q$ does not add random reals. 
\ENDPROCLAIM

%For $\fct$-bounding forcing notions, this can be done using [??]. 


 The most outstanding problem concerning countable support
iteration is the following: 
\PROCLAIM\Cohenproblem/Problem (Judah-Shelah):  If $\<P_n, Q_n:n<\omega>$
is a countable 
support iteration with countable support limit~$P_\omega$.  Does 
$$ \forall n: \hbox{ $P_n$ does not add Cohen reals over $V$}$$
imply that $P_\omega$ does not add Cohen reals over $V$? 
\ENDPROCLAIM


(For a partial solution see [\DeltaOneThree].)


\bigskip

I want to thank Saharon Shelah for fruitful discussions about
iterated forcing. 

\endgroup
%%%% end of pres_intro

%------------------------------------------------------
%           ****** 1: comp & iter   ********
%------------------------------------------------------
%%%%%%%% pres_forcing.tex (from forcing.tex, thesis version) 
\def\hoch#1^#2{#1^{\langle#2\rangle}}
\def\here{\par\centerline{$\bullet$}\par}
\newcount\hyper
\newcount\hypo
\def\bP{\bar P}
\def\bQ{\bar Q}
 % some basic facts about forcing, iteration, composition.
\def\limi{\lim\nolimits_I}


\neusection
\beginsection \printchapternumber 1\quad Composition and iteration of
				forcing 

We briefly review a few facts about composition of forcing and
iterated forcing.   


If $P$ is a forcing notion, and $\name Q$ is a $P$-name of a forcing
notion, then we can force in $V^P$ with $\name Q$ to obtain a new
extension~$(V^P)^Q$.  There is a single forcing notion $P*\name Q$
(the ``composition'' of $P$ and $\nQ$) such that the extension
$V^{\smash{P*\name Q}}$ is canonically isomorphic
to~$(V^P)^{\smash{\name Q}}$.  



\PROCLAIM\composeDef/Definition:  Assume that $P$ is a forcing notion, and
$\nQ$ is a $P$-name for a forcing notion.  Then we let $P*\nQ$
be the set of all pairs $\<p, \nq>$ such that $p\in P$ and
$p\Forces_{ Q}``$\nq\in \nQ$''$. 

We let $\<p,q> \weaker_{P*\name Q} \<p', q'>$ iff $ p \weaker p' $ and
$p'\Forces_{ P}``$q \weaker_{\name Q} q'$''$. 
\ENDPROCLAIM


\PROCLAIM\class?/Remark:  As defined, $P*\nQ$ is a proper class.  However,
as in [\JechSt],  we choose for each class of
equivalent $P$-names a representative.  Then the official definition
of $P*\nQ$ is:  The set of all pairs $\<p,\nq>$, where $p\in P$, $\nq$
a representative $P$-name, and $p \forces \nq\in \nQ$.  Then $P*\nQ$
is a set.     
\ENDPROCLAIM

A similar remark will apply to iteration of forcing.  

([\Kunen] chooses a different way to avoid proper classes.  However,
this solutions causes anomalies that we want to avoid.  See [\Kunen,
Exercise VIII E2--E4] and [\Chaz].) 




\medskip
\PROCLAIM\starFact/Fact: Assume that $P$, $\nQ$ are as above.  Then
(see  [\Kunen]) 
\begindent
\ite 1 If $G \subseteq P$ is generic over $V$, $H \subseteq 
{\nQ}[G]$ generic over $V[G]$, then 
 $$ G*H:= \{ \<p, \nq> \in P * \name Q: p\in G, \nq[G] \in H\}$$
is generic for $P*{\name Q}$ over $V$,and $V[G*H]= V[G][H]$. 
\ite 2 Conversely, if $J \subseteq P*\nQ$ is generic over $V$,
then $G:=\{p: \exists \nq\, \<p,\nq>\in J\}$ is generic for $P$ over
$V$, $H:= \{\nq[G]: \exists p\in G, \<p,\nq>\in J\}$ is generic for
$\nQ$ over $V[G]$, and~$J=G*H$.
\ite 3 Moreover, $P*\nQ$-names can be translated to $P$-names for
$Q$-names, i.e., for every  $P*\nQ$-name $\nx$ there is $\nx'$,  a
$P$-name  for a $\nQ$-name such that whenever $G$, $H$ are as above,
then  
 $$ \nx [G*H] = (\nx'[G]) [H]$$
 Conversely, if $\nx'$ is $P$-name for a $Q$-name, we can find a
corresponding $P*\nQ$-name~$\nx$.  

{\bf We often  identify $\nx  $ and
$\nx'$.  }
\endent
\ENDPROCLAIM      
\bigskip


\PROCLAIM\iterDef/Definition:  Let $\kappa$ be ordinal, and let $I$ be an
ideal on $\kappa$ containing all finite sets. ($I$ is not necessarily
a proper ideal.)  By induction on
$\varepsilon<\kappa$ we 
will define what an $I$-supported iteration of length
$\varepsilon$ is, and what the $I$-supported limit of such an
iteration is.  
\ENDPROCLAIM

``finite support'' means that we let $I$ be the  ideal of finite
subsets  of $\kappa$, and ``countable support'' means that we let $I$
be the (possibly improper) ideal of all countable subsets of~$\kappa$.
In this context, ``countable'' is understood to include ``finite''.  


\begindent
\ite 1 $\bar Q^\varepsilon  := \<P_\alpha,
\nQ_\alpha:\alpha<\varepsilon>$ is an  $I$-supported iteration  
       iff for all $\alpha<\varepsilon$,  
     \itemitem{} $P_\alpha  = 
   \limi \<P_{\beta}, \nQ_{\beta}:{\beta}<\alpha>$,  and 
     \itemitem{} $\Forces_{ P_\alpha }``$Q_\alpha= \<\nQ_\alpha,
       \le_{\name Q_\alpha}, \emptycondition_{\name Q_\alpha}>$ is
       a forcing notion''$.   
\ite 2 \itemitem{(a)}
       The underlying set of $\limi\bar Q^\varepsilon $ is the set of
       all  partial functions $p$ with $\dom(p)\in I$ satisfying  
 $$ \forall {\beta} \in \dom(p): p\on {\beta} \forces_{\beta}
        p({\beta})\in 	\nQ_{\beta}$$ 
\itemitem{(b)}   For $p,q\in \limi\<P_\alpha,
\nQ_\alpha:\alpha<\varepsilon>$ we   define $p \weaker_{\limi 
       \bar Q^\varepsilon} q $ iff  
  $$ \forall {\beta} \in \dom(p) \cup \dom(q): \quad q\on {\beta}
\forces p({\beta}) \weaker_{\name Q_{\beta}} q({\beta})$$
\itemitem{} (where we agree to let
$p({\beta})=\emptycondition_{\name Q_{\beta}}$ for ${\beta}\notin
         \dom(p)$.) 
\itemitem{(c)} $\emptycondition_{\limi\bar Q^\varepsilon}= \emptyset$. 
\endent
      
	


Whenever we consider a $I$-supported iteration
$\<P_\alpha,\nQ_\alpha: \alpha<\varepsilon>$, we automatically define
$P_\varepsilon$ to be the $I$-supported limit of this iteration.
This allows us to avoid the more awkward notation $\<P_\alpha,
\nQ_{\beta}: \alpha\le \varepsilon, {\beta}<\varepsilon>$. 


\PROCLAIM\examIter/Example:  $P_0=\{\emptyset\}$.  $\nQ_0$ is a
$P_0$-name for a 
forcing notion.   Since $P_0$ is the  trivial forcing notion,
$G_0:=P_0$ is a ``generic filter'', and $V = V[G_0]$.  We identify
$\nQ_0$ with~$Q_0:=\nQ_0[G_0]$. 


$P_1$ is the set of all partial functions from $\{\emptyset\}$ to
  $Q_0$, i.e., $P_1$ is isomorphic to $Q_0$, similarly,  $P_2$ is
  isomorphic   to  
$Q_0*\nQ_1$ by 
the map that sends $p\in P_2$ to $\<p(0), p(1)>\in Q_0*\nQ_1$. 
\ENDPROCLAIM

\PROCLAIM\RemIter/Remark:  By expanding definitions it is easy to see that
in general the forcing notion  $P_{\alpha+1}:=
	\limi\<P_{\beta}, \nQ_{\beta}: {\beta}<\alpha+1>$ is
isomorphic to $P_\alpha * \nQ_\alpha$,  
via the map that sends $p\in P_{\alpha+1}$ to $\<p\on
\alpha, p(\alpha)>$.
\ENDPROCLAIM





\medskip
The following two facts follow easily from the definitions. 

\PROCLAIM\factL/Fact:  If $\varepsilon$ is a limit ordinal, then 
\begindent
\ite 1 $p\in P_\varepsilon$ \ iff \ $\dom(p) \subseteq \varepsilon $
  is in $I$, and $\forall \alpha<\varepsilon$, $p\on \alpha\in
  P_\alpha$. 
\ite 2 For $p,q\in P_\varepsilon$, $p\le_\varepsilon q$ iff $\forall
  \alpha<\varepsilon$, $p\on \alpha \le_\alpha q\on \alpha$. 
\endent
See also \factLL/. 
\ENDPROCLAIM

      
\PROCLAIM\factS/Fact:  If $\varepsilon=\alpha+1$, then 
\begindent
\ite 1 $p\in P_\varepsilon$ \ iff \  $p\on \alpha\in
  P_\alpha$, and $p\on \alpha \forces_\alpha p(\alpha)\in Q_\alpha$.
  (Again, this includes the case that $\alpha\notin \dom(p)$, where we
  declare $p(\alpha)= \emptycondition_{Q_\alpha}$.)
\ite 2 For $p,q\in P_\varepsilon$, $p \weaker_\varepsilon q$ iff $p\on
  \alpha \weaker_\alpha q\on \alpha$ and $q\on \alpha \forces_\alpha
  p(\alpha)\weaker_{Q_\alpha} q(\alpha)$. 
\ite 3  For $p,q\in P_\varepsilon$, $p \weaker^*_\varepsilon q$ iff $p\on
  \alpha \weaker^*_\alpha q\on \alpha$ and $q\on \alpha \forces_\alpha
  p(\alpha)\weaker^*_{Q_\alpha} q(\alpha)$. 
\endent
\ENDPROCLAIM




\PROCLAIM\FactA/Fact:  For all $\alpha \le \varepsilon$: 
\begindent
\ite 1 $P_\alpha \subseteq P_\varepsilon$. In fact, $P_\alpha = \{p\in
       P_\varepsilon: \dom(p) \subseteq \alpha\}$. 
\ite 2 If $p,q\in P_\alpha$, then $p \weaker_\alpha q$ iff $p
       \weaker_\varepsilon q$. 
\ite 3      If $p\in P_\alpha$, $q\in P_\varepsilon$,  then $p
\weaker_\varepsilon q$ iff $p \weaker_\alpha q\on \alpha $. 
\endent
Proof: (1) and  (2)  follow immediately from the definition.  For
  (3), 
 note that for $\beta\in\dom(q) - \alpha$,
 $p({\beta})=\emptycondition_{\name Q_{\beta}}$, so $q\on {\beta}
  \forces 
 p({\beta}) \weaker q({\beta})$. 
\ENDPROCLAIM



\PROCLAIM\filterFact/Fact and Notation: Let  \iter{} be an iteration. 
  If $G_\alpha \subseteq P_\alpha$ is generic, and $H \subseteq
   \nQ_\alpha[G_\alpha]$ is any set, we let $$G_\alpha * H = 
     \{r\in P_{\alpha+1}: r\on \alpha \in G_\alpha,
  \,r(\alpha)[G_\alpha] 
\in H\}$$

Then:  $G_\alpha*H$ is generic iff $G_\alpha$ is
   generic and $H \subseteq \nQ_\alpha[G_\alpha]$ is generic
  over~$V[G_\alpha]$. 

  Conversely, writing $G(\alpha)$ for $\{q(\alpha)[G_\alpha]:
q \in G_{\alpha+1}\}$, we know that is a generic
     filter on $\nQ_\alpha[G_\alpha]$ over the model
  $V[G_\alpha]$, and 
     $G_{\alpha+1}=G_\alpha * G(\alpha)$.
\ENDPROCLAIM

Proof:  This is just a restatement of \starFact/, using \RemIter/. 

\medskip





\PROCLAIM\recRemark/Remark: 
	The recursion theorem tells us that if $F$ is a function
(possibly a class) then for all $\varepsilon$ there exists an
$I$-supported iteration $\bar Q = \<P_\alpha, \nQ_\alpha :
\alpha<\varepsilon>$ such that:  

$$ \eqalign{&\hbox {If for all $\alpha<\varepsilon$,
$F(\bar Q\on \alpha)$ is (defined and) a $P_\alpha$-name for a
       forcing notion,}\cr
&\hbox{then for all $\alpha<\varepsilon$ $\forces_\alpha
\nQ_\alpha=F(\bar Q\on \alpha)$}}$$
\ENDPROCLAIM
\bigskip
For the following, let $\<P_\alpha, \nQ_\alpha:\alpha<\varepsilon> $ be 
 an $I$-supported iteration forcing iteration, and let
 $P_\varepsilon$ be the $I$-supported limit of this iteration, and
 let $\alpha $  range over $\varepsilon\cup \{\varepsilon\}$.



\PROCLAIM\firstland/Definition:  Assume $\alpha\le \varepsilon$. 
 If $p\in P_\varepsilon $, $r\in P_\alpha$, and $p\on \alpha
       \weaker r$, then we let $p \land r: = r \cup p\on
[\alpha,\varepsilon)$. 
\ENDPROCLAIM
\begingroup
\midinsert
\def\shortstrut{\vrule height 3pt depth 1pt}
\def\hrf#1{\multispan#1\hrulefill}
\def\hf#1{\multispan#1\hfill}
\def\marker{\hrulefill\shortstrut\hrulefill}
\def\marka{\hfill\shortstrut\hrulefill}
\def\marko{\hrulefill\shortstrut\hfill}
\def\nomarka{\hfill\hrulefill}
\def\nomarko{\hrulefill\hfill}
\def\cn#1{\hfill$#1$\hfill}
\def\cnd#1{\rlap{\ $#1$}}
\def\hdotfill{\leaders\hbox{.}\hfill}

 % -----------r
 % ------------------------p
$$\vcenter{
\baselineskip=12pt\ialign{&#\cr
   \marka&\hrf        1&\marko \cnd r\cr
   \marka&\hrf 3&\marko\cnd p\cr
\noalign{\vskip16pt}
   \marka&\hrf1&\marker&\hrf1&
\marko\cr
\strut 0\hfil&\hf1&$\alpha$\hfil&\hf1
&$\varepsilon$\hfil\cr
 &\qquad\qquad\quad & &\qquad\qquad \quad & \cr}
}\qquad \raise 1cm\hbox{$\Longrightarrow$}
 % -----------
 %            ------------- p /\ r
\qquad\vcenter{
\baselineskip=12pt\ialign{&#\cr
   \marka&\hrf        1&\nomarko \cr
   \hfil&\hfil&\nomarka&\hrf 1&\marko\cnd {p\land r}\cr
\noalign{\vskip16pt}
   \marka&\hrf1&\marker&\hrf1&
\marko\cr
\strut 0\hfil&\hf1&$\alpha$\hfil&\hf1
&$\varepsilon$\hfil\cr
 &\qquad\qquad\quad & &\qquad\qquad \quad & \cr}
}
$$
\endinsert
\endgroup

\PROCLAIM\firstandFact/Fact: Assume $p$, $r$ are as above. Then: 
\begindent
\ite 1  $p\land r\in P_\varepsilon$
\ite 2   $p\land r \stronger p$. 
\ite 3  If $p_1 \weaker p_2$, then $p_1\land r \weaker p_2\land r$. 
\endent
\ENDPROCLAIM

Proof: By induction on ${\beta}$ we can show (simultaneously) $(p\land
           r)\on {\beta}\in P_{\beta}$ and  $(p\land  r)\on {\beta}
           \stronger p \on {\beta}$: 

If ${\beta}\le \alpha$, we have $(p\land r) \on {\beta} = r\on {\beta}
\stronger_{\beta} p\on {\beta}$. 

If ${\beta}>\alpha$, ${\beta}$ limit, then by induction hypothesis
for all ${\gamma}<{\beta}$ we have $(p\land r)\on ({\gamma}+1) \in
P_{{\gamma}+1}$, so $(p\land r)\on {\gamma} \forces (p\land
r)({\gamma})\in \nQ_{\gamma}$.  So by \factL/, $(p\land r)\on
{\beta})\in P_{\beta}$.      Also by induction hypothesis for all
${\gamma}<{\beta}$ we have $(p\land r)\on {\gamma} \stronger_{\gamma}
p\on {\gamma}$, so by \factL/, $(p\land r) \stronger_{\beta} p$. 


If ${\beta}>\alpha$ is a successor ordinal, say ${\beta}={\gamma}+1$,
then $(p\land r) \on {\gamma} \in P_{\gamma}$ by induction hypothesis,
and $(p\land r)\on {\gamma} \forces (p\land
r)({\gamma})=p({\gamma})\in \nQ_{\gamma}$, as $(p\land r)\on {\gamma}
\stronger p\on {\gamma}$.  So by \factS/, $(p\land r)\on {\beta} \in
P_{\beta}$.        Also by induction hypothesis 
 have $(p\land r)\on {\gamma} \stronger_{\gamma}
p\on {\gamma}$, so by \factS/, $(p\land r) \stronger_{\beta} p$. 






(3): By induction, $(p_1\land r)\on {\beta} \weaker (p_2\land r ) \on
           {\beta}$. 


\medskip

\PROCLAIM\oneeight/Fact:  
If $\alpha \le \varepsilon$,  $p\in P_\alpha$, $q\in P_\varepsilon$,
then $p  \perp_\varepsilon q $ iff $p \perp_\alpha q\on \alpha$.  
\ENDPROCLAIM


Proof: 
By \FactA/(3),  if $r\in P_\varepsilon$, $r \stronger_\varepsilon
p,q$, then $r\on \alpha \stronger_\alpha p, q\on \alpha$.
Conversely, if $r\in P_\alpha$, $r \stronger_\alpha p, q\on \alpha$,
then $r\land q \stronger_\varepsilon  p, q$. 

\PROCLAIM\abFact/Fact: 
\begindent
\ite 1 If $A \subseteq P_\alpha $ is a maximal antichain, $\alpha \le
\varepsilon$, then $A$ is also a maximal antichain 
        in~$P_{\varepsilon}$. 
\ite 2 If $G_{\varepsilon} $ is generic for $P_{\varepsilon}$, then
        $G_\alpha:= G_{\varepsilon} \cut P_\alpha$ is generic for~$P_\alpha$.
\endent
\ENDPROCLAIM
      
Proof of (1):  $A$ is an antichain in $P_\varepsilon$, by \oneeight/.
Assume that $r\in P_\varepsilon$, $r\perp_\varepsilon a$ for all $a\in
A$. Then again by \oneeight/, $r\on \alpha \perp_\alpha a$ for all
$a\in A$, so $A$ is not maximal in~$P_\alpha$. 



(2) follows immediately from (1). 



\bigskip

\PROCLAIM\subNotation/Notation:  We write $\le_{\alpha}$ for
$\le_{P_\alpha}$, similarly $\forces_\alpha$, etc.  
  We may write $G_\alpha $ for $G_{P_\alpha}$, and $G(\alpha)$ for
$G_{Q_\alpha}$. 

  When we talk about a $I$-supported iteration \iter, it is
   understood that $P_\varepsilon$ is defined as the $I$-supported
   limit of this iteration. 



   If $\beta \le \alpha$,
   and \iter\ is an iteration, then $G_\beta $ always denotes
  $G_\alpha 
   \cut P_\beta$. 

When we fix a ground model $V=V_0$, and consider an iteration
   $\iter\in V_0$, we write $V_\alpha$ for~$V[G_\alpha]$. 
{\bf Note that this conflicts with the notation that some authors
   use for the sets of rank~$<\alpha$.}
\ENDPROCLAIM


\PROCLAIM\Factfour/Fact: Assume that $\lambda$ is a limit ordinal. 
  Then for a generic $G_\lambda \subseteq P_\lambda$, for all $p\in
   P_{\lambda}$, 
   $$ p\in G_\lambda\,\, \liff  \,\, \forall \alpha<\lambda\,\, p\on
       \alpha \in G_\alpha$$
\ENDPROCLAIM

Proof: Assume not, then there exists a condition $q$
forcing this. 

So $q \forces_\alpha \forall \beta < {\lambda} \, p\on \beta \in
G_\beta\logand p\notin G_{\lambda} $.
For $\alpha \in \dom(p)\cup \dom(q)$ we let $q'(\alpha)$ be a name
such that 
 $$\forces_\alpha q'(\alpha) \stronger q(\alpha) \logand
  \left(q'(\alpha) \stronger p(\alpha) \lor q'(\alpha) \perp
p(\alpha)\right)$$
(We can get such $q'(\alpha)$ using \exComplete/)  Now
we claim that 
for all $\alpha$, $q'\on \alpha \forces q'(\alpha) \stronger
p(\alpha)$.  Assume not, then there exists a generic filter $G_\alpha$
containing $q'\on \alpha$ such that $p(\alpha)[G_\alpha] \perp
q'(\alpha)[G_\alpha]$.  So we can extend $G_\alpha$ to a generic
$G_{\alpha+1}:=G_\alpha * G(\alpha)$ containing $q'\on \alpha+1$ but
not $p\on \alpha+1$. 
Now we can extend $G_{\alpha+1}$ to $G_{\varepsilon}$, containing $q'$
(hence $q$) but not $p\on \alpha+1$, a contradiction.






\PROCLAIM\filterCor/Corollary: For $p\in P_{\lambda}$, we have $p\in
  G_{\lambda}$ iff for all ${\beta}<{\lambda}$,
  $p({\beta})[G_{\beta}]\in G({\beta})$.   
\ENDPROCLAIM

Proof of the corollary: By induction on ${\beta}<{\lambda}$ we can
  show 
$p\on {\beta}\in G_{\beta}$.   Limit steps are handled by
\Factfour/, and successor steps by \filterFact/. 




\PROCLAIM\factLL/Corollary: 
  If $\varepsilon$ is a limit ordinal, then 
\begindent
\item{} For $p,q\in P_\varepsilon$, $p\weaker^*_\varepsilon q$ iff $\forall
  \alpha<\varepsilon$, $p\on \alpha \weaker^*_\alpha q\on \alpha$. 
\endent
\ENDPROCLAIM
Proof: If for all $\alpha<\varepsilon$ $q\on \alpha  \forces_\alpha
p\on \alpha\in G_\alpha$, then $q \forces_\varepsilon p\in
G_\varepsilon$, by \Factfour/.   

Conversely, if for some $\alpha<\varepsilon$ we have $p\on \alpha \not
\weaker^* q\on \alpha$, then there is $r\in P_\alpha$, $r \stronger
q\on \alpha$, $ r \perp p\on \alpha$.   Letting $q':= q\land r$ we
get $q' \forces p\notin G_\varepsilon$.  Since $q \weaker q'$, we 
do NOT have
$q \forces p\in G_\varepsilon$, so $q \not \stronger^* p$. 





The following fact shows that in finite support iteration of ccc
forcing notions and in countable support iteration of proper forcing
notions no new reals are added in limit steps of cofinality~$>\omega$. 

\PROCLAIM\nonew/Lemma:  Assume $\iter$ is an iteration, and ${\delta}$ is
a limit ordinal  of cofinality $>\omega$, and all there are no
conditions in $P_{\delta}$ whose domain is unbounded in~${\delta}$.
(In particular, this will be true for finite or countable support
iteration.) Then: 
$$ \forces_{\delta}  \hbox{If $cf({\delta})>\omega$, then
	$\fct \cut V[G_{\delta}] = \bigcup_{\alpha<{\delta}} \fct \cut
	V[G_\alpha]$}$$ 
\ENDPROCLAIM
Proof:  For any $\alpha<{\delta}$ we define a $P_\alpha$-name $\name
	f_\alpha$ satisfying the following: 
$$ \forall n\ \forces _\alpha 
\vtop{\hbox{``If there is $p\in G_\alpha$, $j\in \omega$ such that $V
	\thinks  p \forces_{\delta} \nf(\check n) = \check \jmath$,}
\hbox{then $\nf_\alpha(n)=j$}}$$
(Note that it is possible to define such a function, since any two
	$p,p'\in G_\alpha$ must be compatible (in $P_{\delta}$) hence
	cannot force two different values for~$\nf(n)$.) 

We will show that $\forces_{\delta} \exists \alpha \nf = \nf_\alpha$. 


 Work in~$V[G_{\delta}]$.  For any $n$, let $j_n:=
	\nf[G_{\delta}](n)$, and find a condition $p_n\in G_{\delta}$
	such that $V\thinks p_n \forces _{\delta} \nf(n)=\check
	\jmath_n$.  

Since (in $V[G_{\delta}]$) we have $cf({\delta} )>\omega$, and the
	supports of the $p_n$ are bounded in ${\delta}$,  we can find
	$\alpha<{\delta}$ such that for all $n$, $p_n\in P_{\alpha}$,
	and hence also $p_n\in G_\alpha$.   Clearly $\nf[G_{\delta}] =
	\nf_\alpha[G_\alpha]$. 





%------------------------------------------------------
%           ****** 2: finite supp   ********
%------------------------------------------------------	
\neusection 
\beginsection \printchapternumber 2\quad  Finite support iteration and
ccc 


A forcing notion $P$ is said to satisfy the countable chain condition,
 if there is no uncountable set of
pairwise incompatible conditions. 

\PROCLAIM\cccChar/Fact:  ``$P $ has the $ \ccc$'' is equivalent to the
following statement: 

\quote
Whenever $\nalpha$ is a $P$-name,  and $ \forces
\hbox{``$\nalpha$ is an ordinal''}$, then there exists a countable set
$A$ of ordinals such that $ \forces \nalpha \in A$.\etouq

(Equivalently, if $ \forces \nx \in V$ for some $P$-name $\nx$, then
there exists a countable set $A$ in $V$ such that $ \forces  \nx\in
A$.)
\ENDPROCLAIM


Proof:  Assume that $P$ has the~$\ccc$. Let $C \subseteq P $ be a maximal
set of conditions satisfying 
\begindent
\ite 1 $p \in C \limpl \exists {\beta}\, p \forces
		\nalpha=\widehat{\beta}$.  
\ite 2 $p_1, p_2\in C \limpl p_1 \perp_P p_2$. 
\endent
It is easy to see that $C$  must be a maximal antichain in $P$
(because the set of conditions satisfying (1) is dense). 

Let $A:=\{{\beta}: \exists p \in C:  p\forces \nalpha = \widehat{\beta}\}$.
Then  $A$ is countable because $C$ is countable, and clearly  $\forces
\nalpha \in A$. [Proof:  Every condition $p\in C$ forces $\nalpha \in
A$.  A condition forcing $\nalpha \notin A$ cannot be compatible with
any condition in $C$, which contradicts the above observation that $C$
is a maximal antichain.] 
\smallskip

Conversely, assume that $\<p_i:i<\omega_1>$ is an antichain.  Let
$\nalpha$ be a name of an ordinal such that 
$$ \forces \exists i\, p_i\in G_P \limpl p_{\name \alpha} \in G_P$$
Assume, towards a contradiction,  that there is a countable set $A$ of
ordinals such that $\forces \nalpha \in A$.  Let $i\in \omega_1 - A$.
Then $p_i \forces p_i \in G_P$, but for all $j\not=i$, $p_i \forces
p_j \notin G$.  So $p_i \forces \nalpha = i\notin A$, a contradiction. 



The same proof also shows:  $P$ has the ccc, iff 
\quote
Whenever $\nx$ is a $P$-name,  and $ \forces
\hbox{``$\nx\in V$''}$, then there exists a countable set
$A$  such that $ \forces \nx\in A$.
\etouq




\PROCLAIM\cccCharCor/Corollary: If $P$ has the $ \ccc$, and $\name X$ is a
  name of a countable set $\subseteq V$, then there exists a countable
  set $A$  in $V$   such that $\forces \name X \subseteq A$.   
\ENDPROCLAIM


The next theorem can be phrased ``ccc is preserved under composition
of forcing notions.'' 


\PROCLAIM\cccComp/Corollary: Assume $P $ has the $ \ccc$, and
$\forces_P$``$\name Q$ has the~$\ccc$.''   Then $P * \nQ $ has the~$\ccc$. 
\ENDPROCLAIM

Proof: Let $\nalpha$ be a $P*\nQ$-name of an ordinal.  We consider
$\nalpha$ as a $P$-name for a $\nQ$-name of an ordinal.  So since 
$\forces_P$``$\name Q$ has the $ \ccc$,''  (and using the existential
completeness lemma) we can find a $P$-name $\name A$ such that 
\begindent
\ite 1 $\forces_P \hbox{``$\name A$ is countable''}$
\ite 2 $\forces_P \hbox{``${} \forces_Q \nalpha \in \name A$''}$. 
\endent
By \cccCharCor/ we can find a countable set $A'$ in $V$ such that
$$ \forces_P A \subseteq A'.$$
So $\forces_P \forces_{\name Q} \nalpha \in A'$, hence
$\forces_{P*\name Q} \nalpha\in  A'$. 

\medskip

The next theorem shows that the property of satisfying the countable
chain condition is satisfied under finite support iteration.


\PROCLAIM\cccPres/Theorem: Assume that $\iter$ is a finite support
iteration of forcing notions, and 
$$ \forall \alpha<\varepsilon: \ 
 \forces_\alpha \hbox{``$ Q_\alpha$ has the $\ccc$''}$$ 
Then $P_\varepsilon $ has the~$\ccc$. 
\ENDPROCLAIM

The proof of this theorem proceeds by induction on~$\varepsilon$.
Successor steps are handled by  \cccComp/ and \RemIter/.  

As for limit steps, from the  induction hypothesis we can conclude
that 
$$ (*)\qquad\qquad \forall \alpha<\varepsilon \,\, P_\alpha \thinks \ccc$$
We will show that $(*)$ implies that $P_\varepsilon$ has the~$\ccc$.  We
need to use the following combinatorial fact (called the
$\Delta$-system lemma): 


\PROCLAIM\Deltalemma/Lemma: Assume  that $\<F_i:i<\omega_1>$ is a family
of finite sets.  Then there is a set $S \subseteq \omega_1$ of size
$\aleph_1$ such that the family $\<F_i:i\in S>$ is a
${\Delta}$-system, i.e. 
$$ \exists F \hbox{ finite } \forall i,j\in S: i\not= j \limpl F_i\cut
F_j  \subseteq 
F$$

$F$ is called a ``kernel'', ``root''  or ``heart'' of the ${\Delta}$-system
$\<F_i:i\in S>$. 
\ENDPROCLAIM

See [\Kunen, II.1.5] for a proof. 


{\bf Proof of \cccPres/, limit step: }

Assume (toward a contradiction) that $\<p_i:i<\omega_1>$ is an
antichain of conditions in~$P_\varepsilon$. Since
$\<\dom(p_i):i<\omega_1>$ is a family of finite sets, the
${\Delta}$-lemma applies. 

So we can find a set  $S \subseteq \omega_1$ of size $\aleph_1$  and a
finite set $F$ such that for all distinct $i$ and $j$ in $S$,
$\dom(p_i) \cut \dom (p_j) \subseteq F$.  Let $F \subseteq {\alpha} <
\varepsilon$. 

The family $\<p_i\on {\alpha}:i\in S>$ is an uncountable familiy of
conditions in~$P_{\alpha}$.  By our assumption $(*)$, it cannot be an
antichain. So there are $i\not= j$ in $S$  and a condition $r\in
P_{\alpha}$ such that $p_i \weaker r $ and $p_j \weaker r$. 

Now define $p\in P_\varepsilon$ as follows: 
\begindent
\item{} $p\on {\alpha} = r$.
\item{} $\forall \gamma \in \dom (p_i) - {\alpha} $:~$p(\gamma)=p_i(\gamma)$. 
\item{} $\forall \gamma \in \dom (p_j) - {\alpha} $:~$p(\gamma)=p_j(\gamma)$. 
\endent
      Note that $\dom(p_i) \cut \dom (p_j) \subseteq F \subseteq
        {\alpha}$, so $\dom(p_i) - {\alpha}$ and $\dom (p_j)-{\alpha}$
        are disjoint. 

We leave it as an exercise to check that $p$ is indeed a condition in
$P_\varepsilon$, and $p_i \weaker p$, $p_j \weaker p$.

This is a contradiction, as $\<p_i:i<\omega_1>$ was supposed to be an
antichain.


%------------------------------------------------------
%           ****** 3: properness   ********
%------------------------------------------------------	
\neusection      
\beginsection \printchapternumber 3\quad  Properness and countable
					support iteration 


\PROCLAIM\genericDef/Definition:  Assume that  $(N, \mathord{\in})$ is a
model of a fragment of ZFC (which should be large enough to develop
the general theory of forcing).   Let $P\in
N$ be a forcing notion, and assume that for all $p_1, p_2\in P \cut
N$: $N \thinks p_1\perp_P p_2 \limpl V \thinks p_1 \perp_P p_2$.   We
say that $G$ is $N$-generic for $P$ iff:  
\begindent
\item{} For all $A\in N$, if $N \thinks$ ``$ A \subseteq P$ is a
  maximal 
        antichain of $P$'', then $G \cut N \cut A \not=\emptyset$. 
\endent
(So $G$ is $N$-generic iff $G\cut N$ is $N$-generic.)
\ENDPROCLAIM

It is easy to see that we by replacing ``maximal antichain'' by
      ``dense subset'', ``dense open subset'' or ``predense
      subset'', we get an equivalent definition. 


In fact, the following holds: 

\PROCLAIM\trivEq/Fact: Assume $p\in P\cut N$, $P\in N$, $p\le q\in P$.
Then the following are equivalent: 
\begindent
\def\\#1.#2.#3.{\ite {#1} For all $D_{#1}\in N$:  If $N
\thinks$``$D_{#1}$ is #2 $\subseteq P$,'' then $q \forces D_{#1}\cut N
\cut G \not= \emptyset$.}
\ite 1 For all $D_1\in N$:  If $N \thinks$``$D_1$ is predense below
$p$'', then $D_1\cut N $ is predense below~$q$.  
\\2.predense..
\\3.dense..
\\4.a maximal antichain..
\\5.open dense..
\endent
\ENDPROCLAIM

Proof: We will show $\vcenter{\tabskip=10 pt plus 10 pt\offinterlineskip
\halign{&\hfil$#$\hfil\cr
&&   &      &   &        &(3)\cr
&&   &      &   &\nearrow&    &\searrow\cr
&&(1)&\to   &(2)&        &    &         &(5)& \to (1). \cr
&&   &      &   &\searrow&    &\nearrow\cr
&&   &      &   &        &(4)\cr}}$



(2) $\limpl$  (4), (2) $\limpl$ (3), (3) $\limpl$ (5) are
trivial. 


\medskip

(1) $\limpl$ (2):  Let $D_2$ be predense.  Then $D_2$ is predense
below $p$, so $D_2\cut N$ is predense below~$q$. Hence $q \forces
(D_2\cut N) \cut G \not=\emptyset$. 


\medskip

(4) $\limpl$ (5): Work in~$N$.  Assume that $D_5$ is open dense.  Let
   $D_4$ be a maximal antichain $\subseteq D_5$ (i.e., let $D_4
   \subseteq D_5$ be an antichain such that there is proper superset
   $D_4' \subseteq D_5$ that is also an antichain).  It is enough to
   see that $D_4$ is a maximal antichain in $P$ (in $N$): Assume not,
   and let $r$ be incompatible with every element of $D_4$, let $s
   \stronger r$ be in $D_5$, then also $s$ is incompatible with every
   element of $D_4$, contradicting the maximality of~$D_4$.

\medskip

(5) $\limpl$ (1): Let $D_1\in N$, $N \thinks $``$D_1$ is predense
below~$p$.''  The following takes place in $N$: 

 Let $D_5:= \{r: \hbox{either $r\perp p$, or $\exists d\in D_1\, r
   \stronger d$}\}$.  Then $D_5$ is open.  We claim that $D_5$ is
   dense.  To prove this, let $s$ be any condition in~$P$.  If $s\perp
   p$, then $s\in D_1$.  Otherwise, there is a $t\in P$, $s \weaker
   t$, $p \weaker t$.  $t$ is compatible with some $d\in D_1$, so
   there is $t'$ extending~$d,t,s,p$.  So $t\in D_5$.

 Hence $N \thinks$``$D_5$ is dense'', so $V \thinks q \forces D_5\cut
   N\cut G  \not=\emptyset$. 

 Finally we will to show that (in $V$), $D_1\cut N$ is predense
below~$q$.  Let $r \stronger q$ be incompatible with all elements of 
   $D_1\cut N$.  Let $r' \stronger r$, and $r' \forces s\in D_5\cut N
   \cut G$.  Then $s\in D_5\cut N$.  Either $N \thinks s\perp p$, then
   $s\perp p$, which implies $s\perp r'$, a contradiction to $r'
   \forces s\in G$. Otherwise $N \thinks \exists d\in D_1\, 
   s\stronger d$.  As $r'$ and $s$ are compatible, $r'$ and $d$ are
   compatible, so $D_1\cut N$  is indeed predense below~$q$. 

      \bigskip




\PROCLAIM\newgeneric/Definition:  
We say that $q\in P$ is $N$-generic (or $(N,P)$-generic) iff $$V
   \thinks q \Forces_P``$G_P$ is $N$-generic''$$ (iff \trivEq/(2)--(5)
   hold).
\ENDPROCLAIM


\PROCLAIM\strongergeneric/Remark:   If $q$ is $N$-generic, and $q'
   \stronger q$, then also $q'$ is $N$-generic. 
\ENDPROCLAIM


\medskip

\PROCLAIM\chicon/Notation:  For the following, 
we let $\chi$ be a ``large enough'' regular cardinal.   ``large
enough'' means that for all forcing notions $P$ we consider, we have
$\P(P)\in H(\chi)$, i.e., the power set of $P$ is hereditarily of size
$<\chi$.    Since all forcing notions we consider will be
hereditarily countable, or countable support iterations of length $\le
\aleph_2$ of hereditarily countable forcing notion, and all the
universes we consider satisfy  GCH except for possibly $2^{\aleph_0} =
        \aleph_2$,  we could choose~$\chi:=\aleph_3$.  To be on the
        safe side, we let $$\chi:=\beth_{\omega}^+$$
\ENDPROCLAIM



(So also in every extension that we consider,
$\chi=\beth_\omega^+$).


We will consider countable elementary submodels of $(H(\chi), {\in})$.
  




(The notions we will define below will depend on $\chi$,
but a careful examination [which we will not carry out here] shows
that this dependence is only apparent.) 

Note that all essential properties of $P$ are absolute between $V$ and
$H(\chi)$, for example 
$$ V \thinks A \hbox{ is a maximal antichain of $P$} \ \ \liff 
\ \ H(\chi) \thinks A \hbox{ is a maximal antichain of $P$}$$

We also have the following fact: 

\PROCLAIM\chinames/Fact: If $\forces \name x \in H(\chi)$, then there is a
name $\name {\bar x}\in H(\chi)$ such that $\forces \nx = \name {\bar x}$. 
\ENDPROCLAIM

Proof:  First note that for each element $x$ of $H(\chi)$ there is
${\lambda} < \chi$ and a sequence $\<x_i:i\le  {\lambda}>$ of sets in
$H(\chi)$ such that for all $i\le {\lambda}$ $x_i \subseteq \{x_j:j<i\}$,
and $x = x_{\lambda}$. 

Applying this fact in $V[G]$ to $\name x$, we get a sequence
$\<\nx_i:i\le \name {\lambda} >$.  We can find an ordinal ${\lambda}$
such that $\forces \name {\lambda} \le  {\lambda}$, so wlog we may
assume $\forces \name {\lambda} = {\lambda}$ (since we can define
$\name x_i = \emptyset$ for $\name {\lambda} < i < {\lambda}$. 

Now we define by induction $\name {\bar x}_i:= \{\<\name {\bar x}_j,
p>: p \forces \nx_j \in \nx_i\}$, and prove by induction $\forces
\name{\bar x}_i = \nx _i$. 




\PROCLAIM\PROPER/Definition:   A forcing notion $P$ is called proper, if
   for some $x\in H(\chi)$, for all countable models $(N, {\in})\prec
   (H(\chi), {\in})$ that contain $x$ and $P$, and for all $p\in P\cut
   N$ there exists a  $q \stronger p$ which $N$-generic. 
\ENDPROCLAIM


\PROCLAIM\PROPERremark/Remark:  The clause ``for some $x$ \dots''  above
is not essential, but it makes some proofs slightly simpler.  For
example, when we consider an iterated forcing notion $P_\varepsilon\in
N$, we could reconstruct the iteration  $\<P_\alpha,
\nQ_\alpha:\alpha<\varepsilon>$ from $P_\varepsilon$ (in $N$),
  but the 
above definition makes it unnecessary, as we can include
``$\<P_\alpha, \nQ_\alpha:\alpha<\varepsilon>\in N$'' into our
assumption. 
\ENDPROCLAIM


We leave as an exercise to the reader to show the following fact.  (We
will not use it  in the rest of the paper).   Note that this fact is
independent of~$\chi$. 


\PROCLAIM\antichains/Fact:  $P$ is proper iff player II has a winning
strategy in the following infinite game (see also [\GraysThesis]): 

In the first move, player I plays a condition $p$, and a maximal
antichain~$A_1$. Player II responds with a countable subset $B_1^1
\subseteq A_1$. 

In the $n$-th move ($n>1$), player I plays a maximal antichain $A_n$,
and player II plays countable sets $B_1^n \subseteq A_1$, \dots, $B_n^n
\subseteq A_n$. 

After $\omega$ many moves, player II wins iff there is a condition $q
\stronger p$ such that for all $n$, the set $B_n:= \bigcup_{k \ge n}
B_n^k$ is predense below~$q$.
\ENDPROCLAIM


[Sketch of proof:  If player II has a winning strategy, and player I
plays all maximal antichains of the model $N$, then all responses of
player II will be subsets of~$N$.  Conversely, player II can, in each
move generate
a  Skolem hull $N_n$ (inside $H(\chi)$) of everything played so far.
At the end  any condition generic for $N:= \bigcup_n N_n$ will work.
This definition of the strategy does not take place in $H(\chi)$,
since $H(\chi)$ is needed as a parameter, but the resulting strategy
itself IS in $H(\chi)$.]




\PROCLAIM\propeq/Fact:  For $N$ as above, $q\in P$ is $N$-generic iff for
   all $\nalpha\in N$:  

$$\hbox{If $N \thinks$``$\nalpha$ is a $P$-name for an ordinal'',
   then $q \forces \nalpha\in N$}$$



(Note that  $q \forces
   \nalpha\in N$ really means $q \forces \nalpha[G_P]\in \widehat N$.)
\ENDPROCLAIM
  

Proof: Let $A \in N$, $N \thinks $``$A$ is a maximal antichain.''
   Working in $N$, we can find a cardinal $\kappa$, a function $f$
   from $\kappa$ onto $A$, and a $P$-name $\nalpha$ of an ordinal such
   that $\forces_P f(\nalpha)\in G_P\cut A$.  Then if $q \forces
   \nalpha\in N$, also $q \forces f(\nalpha)\in N$, so $q \forces
   N\cut A \cut G \not=\emptyset$.   Hence $q$ satisfies \trivEq/(4). 

Conversely, let $\nalpha\in N$ be a $P$-name of an ordinal.  Then the
   set $D:= \{r\in P: \exists {\beta}\, r \forces \nalpha={\beta}\}$
   is dense.  Let $f$ be a function with domain $D$ such that for all
   $r\in D$, $r \forces \nalpha=f( r)\widehat{\ }$.  Then $f\in N$, so
        if $q \forces \exists r\in D\cut N \cut G$, then also $q
        \forces \nalpha\in N$, as $\forces$``$r\in N \limpl f(r)\in
        N$.''

\PROCLAIM\propeqRem/Remark:  A similar proof shows: $q$ is $N$-generic iff

$$\forall \nx\in N: \hbox{If $\nx $ is a $P$-name and $\forces \nx\in
        V$, then $q \forces \nx \in N$}$$
(or in other words, $q \forces N[G]\cut V = N$). 
\ENDPROCLAIM


\PROCLAIM\cccEx/Example:  If $P$ satisfies the countable chain
   condition, then every condition (or equivalently, the condition
   $\emptycondition_Q$) is $N$-generic, for any countable model
   $N\prec H(\chi)$ containing~$P$.   Thus, any ccc forcing notion is proper.
\ENDPROCLAIM

Proof:   Note that if $A\in N$ is countable, then $A \subseteq N$,
   because $A$ must be the range of a function $f\in N$ that has
domain~$\omega$.   As $f\in N$, and for all $n\in \omega$, $n\in N$, also 
   $f(n)\in N$ for all $n$, so $A = \rng(f) \subseteq N$.   

Let $A\in N$ be a maximal antichain, then $\forces_Q A \cut G
   \not=\emptyset$.   So also $\emptycondition_Q\forces_Q A\cut N \cut
   G = A\cut G    \not=\emptyset$.   Hence $\emptycondition_Q$
   satisfies condition \trivEq/(4). 

\medskip
(Alternatively, we could use \cccChar/ to show that ccc $\limpl$
proper.) 
\medskip



\PROCLAIM\propercover/Fact: If $Q$ is proper, and $A\in V[G_Q]$  a
countable set of ordinals, then there is a countable
set $B\in V$ of ordinals such that $A \subseteq B$.   
\ENDPROCLAIM

Proof:  Let $\name A$ be a name for $A$, and let $\<\nalpha_n:n\in
\omega>\in V$ be a sequence of names for 
all ordinals in $\name A$.  For each $n$, let $A_n$ be a maximal antichain
of conditions deciding~$\nalpha_n$. We will show that the set of
conditions forcing ``there exists a countable $B$ in $V$ covering
$A$''  is dense.  

So fix a condition~$p$.     Let $N \prec H(\chi)$ be a countable elementary
model  containing $p$, $Q$ and $\<A_n:n\in \omega>$
 and let $q \stronger p $ be $N$-generic. 

Let $B:= \bigcup_{n\in \omega} \{{\beta} : \exists r\in A_n\cut N: r
\forces \alpha_n = {\beta}\}$.  $B$ is countable, and the genericity
of $q$ easily implies that $q \forces \name A \subseteq B$. 


\PROCLAIM\AlephOne/Corollary: If $Q$ proper and  $cf({\delta})> \omega$,
then $\forces_Q cf({\delta})>\omega$.   In particular, $\aleph_1$ is
not collapsed. 
\ENDPROCLAIM

Proof: $Q$ cannot add a countable cofinal sequence in ${\delta}$, by
the previous fact.  (Note that this proof works only for
${\delta}<\chi$, but for ${\delta}\ge \chi$ or indeed ${\delta} >|P|$
a much simpler argument shows that the cofinality of ${\delta}$ is
preserved.) 

\medskip


\PROCLAIM\elemFact/Fact:  If $N\prec H(\chi)$,  and $Q\in N$,  then 
        $\emptycondition \forces  N[G] \prec H(\chi)^{V[G]}$. 
\ENDPROCLAIM

Proof:  (Remember that $\chi$ is quite large compared to~$Q$.) 
We will use the Tarski-Vaught criterion.  So it is enough to see for
        all names $\name a$ in $N$: 
$$ \emptycondition_Q \forces_Q \big(\exists x \, \varphi(x,\name
        a)\big)^{H(\chi)}  \
        \limpl\  \exists x\in N[G]\, \big(\varphi(x,\name
        a)\big)^{H(\chi)}  \leqno(*)\qquad $$ 
By \exComplete/, there is a name $\ntau$ such that 
$$ \emptycondition_Q
\forces_Q 
\ntau\in H(\chi) \logand \Big( (\exists x\,\varphi(x,\name a))^{H(\chi)}
        \limpl \varphi(\ntau, \name a)\Big)^{H(\chi)}.\leqno (**)\qquad$$
As this last statement can be rewritten as a statement in $H(\chi)$
(thanks to \chinames/), 
        we can find such $\ntau$ in~$N$.    


Thus $\emptycondition_Q \forces_Q \ntau \in N[G] \logand \big(
        (\exists x\, \varphi(x,\name a))^{H(\chi)} \limpl
        \varphi(\ntau,\name a)^{H(\chi)}\big)$, which implies~$(*)$. 


\medskip


Note that the same proof actually shows we even have $(N[G], N[G]\cut
H(\chi), {\in})\prec (H(\chi)^{V[G]}, H(\chi)^V, {\in})$.  
So if we work with a proper forcing notion, by \propeqRem/ we also get 
 $(N[G], N, {\in } ) \prec(H(\chi)^{V[G]}, H(\chi)^V, {\in})$. 



\medskip

\PROCLAIM\compFact/Lemma:  Assume that $Q_0*\nQ_1$ is a composition of
   forcing notions.  Then $(q_0, \nq_1)$ is $N$-generic, iff $q_0$ is
   $N$-generic for $Q_0$, and $q_0 \forces$``$\nq_1$ is
   $N[G_0]$-generic for~$\nQ_1[G_0]$.'' 

Similarly, if we have an iteration \iter, $\alpha\le \varepsilon$,
   then $q\in P_{\alpha+1}$ is $(P_{\alpha+1}, N)$-generic  iff:
  \newline 
   $q\on \alpha $ is $(P_\alpha,N)$-generic, and 
$q\on \alpha \forcess_{\alpha}$``$q(\alpha)$ is
        $(Q_\alpha,N[G_\alpha])$-generic.'' 
\ENDPROCLAIM

Proof: (Recall that we identify $Q_0*\nQ_1$-names with $Q_0$-names
   for $\nQ_1$-names) 

We will use \propeq/. For any name $\nalpha\in N$ of an ordinal we
  have $$(q_0, \nq_1) 
   \forces_{Q_0*\name Q_1} \nalpha[G_{Q_0*\name Q_1}]\in N 
\quad \hbox { iff }\quad q_0 \forces_{Q_0} \big(\nq_1 \forces_{\name
  Q_1[G_0]} 
   \nalpha[G_0][G_1]\in N\big)$$


\bigskip
This shows that properness is preserved under composition of forcing
 notions.  The following two lemmata will show that properness is also
 preserved under countable support iteration.  Note that the first one
 does not mention properness or countable models---even the fact that
 the iteration has countable support plays no role. 





\PROCLAIM\newPrelim/Preliminary Lemma:
\newline 
Let $\<P_\alpha, \nQ_\alpha:\alpha<\varepsilon>$ be a countable
  support 
iteration. 

Assume $\alpha_1 \le \alpha_2 \le \beta\le \varepsilon$, $\np_1$
is a $P_{\alpha_1}$-name for a condition in~$P_\varepsilon$.
Let $D$ be a dense open set of~$P_\beta$. 

Then  $\emptycondition_{P_{\alpha_2}} \forcess_{\alpha_2} \exists p_2 \,\,
\varphi(p_2)$,  where $\varphi(p_2)$ is the conjunction of the
  following 
clauses:

\begindent
\item{ (1)} $ p_2\in \widehat P_\beta$, $p_2  \stronger_{\beta}
		\np_1$. 
\item{ (2)} $ p_2 \in \widehat D$. 
\item{ (3)} If $\np_1\on \alpha_2\in G_{\alpha_2}$,
            then $p_2 \on \alpha_2\in G_{\alpha_2}$.
\endent
\ENDPROCLAIM



Remark 1: By the existential completeness lemma there is an
  $\alpha_2$-name 
$\np_2$ for a condition in  
$P_\beta$ such that $\forcess_{\alpha_2} \varphi(\np_2)$. 

Remark 2:  The $P_{\alpha_1}$-name $\np_1$ corresponds naturally to
a $P_{\alpha_2}$-name, which we also call~$\np_1$.  
 In other
 words,  we may wlog assume that~$\alpha_1=\alpha_2$. 
\medskip


{\bf Proof of the lemma:} Assume $\emptycondition_{P_{\alpha_2}}
\mathop{\notforces}_{\alpha_2} \exists p_2 \,\, \varphi(p_2)$, then there
exists a condition 
${r_2}\in P_{\alpha_2}$ such that 
\smallskip
\centerline{$ {r_2} \forces_{\alpha_2}{}$ there is no $p_2$  satisfying 
(1)--(3).}
  We may assume that ${r_2}$ decides what $\np_1$ is, (i.e.\ ${r_2}
\forcess_{\alpha_2} $``$\np_1 = \widehat p_1$'' for some $p_1\in V$),
 and ${r_2}$ also decides whether $p_1\on\alpha_2\in G_{\alpha_2}$.

Case 1:  
 ${r_2} \forcess_{\alpha_2}  p_1\on\alpha_2\notin G_{\alpha_2}$:
  \newline 
 But then (3) is true for any $p_2$, so 

\centerline{$ {r_2} \forcess_{\alpha_2} $ there is no $p_2$
  satisfying  
(1)--(2).}
which is a contradiction since $D$ is dense open. 

Case 2:  ${r_2} \forcess_{\alpha_2}  p_1\on\alpha_2\in G_{\alpha_2}$.
  We may assume ${r_2} \stronger_{\alpha_2} p_1\on \alpha_2$. 
 Now let  $r := p_1\land r_2 =  {r_2} \cup p_1\on[\alpha_2, \beta)
\stronger p_1$, and find 
${p_2}\in D$, ${p_2} \stronger_{{\beta}} r$.  Then 
$$ {p_2}\on \alpha_2 \forcess_{\alpha_2}  {p_2}\hbox{ satisfies
  (1)--(3),}$$ 
again a contradiction, because 
${p_2}\on \alpha_2 \stronger {r_2}$. 



\medskip



\PROCLAIM\inducL/Induction Lemma:
Let $\bar Q:=\<P_\alpha, \nQ_\alpha:\alpha<\varepsilon>$ be a
  countable 
support iteration, and assume that for all $\alpha<\varepsilon$, 
$\forces_\alpha$``$\nQ_\alpha$ is a proper forcing notion.''
  Let 
$N\prec H(\chi)$ be a countable model containing $\bar Q$.  Then: 

For all $\beta  \in N \cut {\varepsilon} $:

 
For all  $\alpha\in N \cut {\beta}  $, all  $\np\in N$: 
\newline
 {\bf Assume} $ \np $ is a $P_{\alpha}$-name for a 
condition in $P_{\beta}$, and 
\begindent
\item{(a)} $q\in P_\alpha$
\item{(b)} $q$ is $(P_\alpha,N )$-generic. 
\item{(c)} $q \forcess_\alpha  \np\on {\alpha} \in
             G_\alpha \cut  N$
\endent

{\bf Then} there is a condition $q^+$: 
\begindent
\item{(a)$^{\splus}$} $q^+\in P_\beta$, $q^+\on \alpha = q$
\item{(b)$^{\splus}$}  $q^+$ is $(P_{\beta},N)$-generic
\item{(c)$^{\splus}$} 
 $q^+ \forces_\beta  \np\on\beta \in
 G_\beta \cut N $
\endent
\ENDPROCLAIM






The proof is by induction on~$\beta$.

\medbreak

{\bf Successor step:}


Let $\beta = \beta' + 1$.  Since we can first use the induction
hypothesis on $\alpha$, $\beta'$ to extend $q$ to a condition 
$q'\in P_{\beta'}$ satisfying the appropriate version of (a)--(c), we
may simplify the notation by assuming $\beta = \alpha+1$. 

Since $q \forcess_\alpha N[G_\alpha ] \prec H(\chi)^{V[G_\alpha]}$,
 we also have $$q 
\forcess_\alpha \hbox{``there is a $(Q_\alpha, N[G_\alpha ])$-generic
condition $\stronger \np(\alpha)$''}$$  By ``existential
completeness'', there is a
$P_\alpha$-name $q^+(\alpha)$ for it.  By \compFact/, 
 we are done. 





\bigbreak

{\bf Limit step:}

Let $\beta \in N$ be a limit ordinal,  ${\delta}:= \sup(\beta \cut N)
 = \bigcup_n \alpha_n$, $\alpha= \alpha_0 < \alpha_1 < \cdots\,$,
 $\alpha_n\in N$.   
  Let $\<D_n:n\in \omega> $ enumerate
all dense subsets of $P_{\beta}$ that are in~$N$. 



First we will define a sequence $\<\np_n: n \in \omega>$, 
$\np_n\in N$,  $\np_0 = \np$ such that the following will hold: 
\begindent
\item{(0)}
 $\np_n$ is a $P_{{\alpha_n}} $-name for a condition in
$P_{\beta}$ 
\item{(1)} $\forcess_{{\alpha_{n+1}}} \np_{n+1} \stronger \np_n$
\item{(2)} $\forcess_{{\alpha_{n+1}}} \np_{n+1}\in D_n$. 
\item{(3)} $\forcess_{{\alpha_{n+1}}}$
``If  $\np_n\on{\alpha_{n+1}} \in G_{\alpha_{n+1}}$ then 
 $\np_{n+1}\on {\alpha_{n+1}} \in G_{\alpha_{n+1}}$''. 
\endent
 
For each $n$ we thus get a name $\np_{n} $ that is in~$N$.   For
each $n$ we can  use
the ``preliminary lemma''  (and remark 1 before its proof)
$\underline{\hbox{in $N$}}$  to obtain~$\np_{n+1}$. 


Now we define a sequence $\<q_n: n \in \omega>$, $q_n \in
P_{\alpha_n}$,  $q=q_0 \subseteq q_1 \subseteq \cdots\,$,
$q_{n+1}\on \alpha _n = q_n$, 
and $q_n$ satisfies (a), (b), (c) (if we write $q_n$
for $q$, $p_n$ for $p$, $\alpha_n$ for~$\alpha$.)

  $q_{n+1} = q_n^+$  can be obtained  by the
induction hypothesis, applied to ${{\alpha_n}}$, ${\alpha_{n+1}}$, and
$\np_n\on {\alpha_{n+1}} $.  By (c)$^\splus$ we know 
$$q_n^+ \forces \np_n\on
{\alpha_{n+1}}  \in
 G_{\alpha_{n+1}}  \cut N $$
Hence by (3) we have 
$$q_{n+1} \forces \np_{n+1}\on
{\alpha_{n+1}}  \in
 G_{\alpha_{n+1}}  \cut N $$

 Since $q_{n+1}\on {\alpha_n} = q_n$,
         $q = \lim q_n$ exists and is ${} \stronger q_n$  for all~$n$.
  

We have to show that $q \forces p \in G_{\beta} \cut N $ and that $q$
is generic. Let $G_{\beta}$ be a generic filter containing~$q$.  We
will write $p_n$ for~$\np_n[G_{\alpha_n}]$.  (Note that $p_n\in N$,
because $q_n$ was 
$N$-generic and $q_n\in G_{\alpha_n} $.)


Since $q_n \weaker q \in G_{\beta}$, we have $ p_n \on {\alpha_n}\in
G_{\alpha_n} 
\cut N$ and $N \models p_n \stronger p_{n-1} \stronger
\cdots\stronger p_0 $.  
Hence  $ p\on {{\alpha_n}} \in
 G_{\alpha_n} \cut N$ for all $n$, and so by \Factfour/, 
$ p\on {\delta}  \in  G_{\delta}  \cut N $.  As $dom(p) \subseteq
 {\delta}$, $p\on {\delta} = p$, so  $p\in G_{{\beta}}$. 
 Similarly, $p_n\in G_\beta$ for all~$n$. 

Consider a dense set $D_n \subseteq P_{\beta}$.  Since  $q_{n+1}
\forces$``$ \np_{n+1} \in  D_n$,'' we  have $p_{n+1}\in G_\beta \cut
D_n \cut N$. 

Hence $q$ is generic. 


\bigskip

\PROCLAIM\ShelahsThm/Corollary:  
Let $\<P_\alpha, \nQ_\alpha:\alpha<\varepsilon>$ be a countable
  support 
iteration of proper forcing notions $Q_\alpha$ (as in \inducL/).  Then
$P_\varepsilon$ (the countable support limit of this iteration) is
proper. 
\ENDPROCLAIM


Proof: Apply \inducL/ with $\alpha=0$, ${\beta} = \varepsilon$. 



%------------------------------------------------------
%           ****** 4: quotient forcing  ********
%------------------------------------------------------		
\neusection
\beginsection \printchapternumber 4\quad Quotient forcing 


Let $\<P_\alpha, Q_\alpha:\alpha<\varepsilon>$ be either a countable support
iteration of proper forcing notions, or a finite support iteration. 




\PROCLAIM\quotDef/Definition:   We define $P_\varepsilon/G_\alpha$ to be a
$P_\alpha$-name for a forcing notion such that 
$$ \forces_\alpha P_\varepsilon/G_\alpha = \{ p\in \widehat
P_\varepsilon: p\on \alpha\in G_\alpha\}$$
For $p,q\in P_\varepsilon/G_\alpha$ we let $p
\weaker_{P_\varepsilon/G_\alpha} q $ iff $p \weaker_{P_\varepsilon}
q$. 
\ENDPROCLAIM


\PROCLAIM\againsub/Notation:
We write $\le_{\alpha \varepsilon}$, $\forces_{\alpha \varepsilon}$,
\dots, for  $\le_{P_\varepsilon/G_\alpha}$,
$\forces_{P_\varepsilon/G_\alpha}$, etc. 
\ENDPROCLAIM




\smallbreak 






\PROCLAIM\quotFactA/Fact: $\emptycondition_{P_\alpha}$ forces the
following: 
\begindent
\ite  1  $P_\varepsilon/G_\alpha \subseteq \widehat P_\varepsilon $. 
\ite 2 If $p,q\in P_\varepsilon/G_\alpha $, then $p \le_{\alpha
   \varepsilon} q \liff p\le_\varepsilon q$.
\ite 3 If $p,q\in P_\varepsilon/G_\alpha $, then $p
  \perp_{\varepsilon} q $ implies $p\perp_{\alpha\varepsilon} q$. 
   (However, note that
   $p\perp_{\alpha\varepsilon}q$ does not necessarily imply
   $p\perp_\varepsilon q$!) 
\ite 4 If $A\in V$, $A \subseteq P_\varepsilon $ is a maximal
  antichain, then $A \cut P_\varepsilon/G_\alpha$ is a maximal
  antichain in~$P_\varepsilon/G_\alpha$.  
\endent
\ENDPROCLAIM
(1) and (2) are true by definition. 

For (3), note that any $r \stronger_{\alpha \varepsilon } p,q$ would
  also satisfy $r \stronger_\varepsilon p,q$.

Proof of (4): By (3),  $\forces_\alpha$``$ A\cut
P_\varepsilon/G_\alpha$ is an antichain.''    Assume that the
conclusion is not true, then  we can find a
condition $r\in P_\alpha$ and a condition $p\in P_\varepsilon$ such
that 
 $$ r \forces_\alpha \vtop{\hsize=0.8\hsize\parindent=0cm
``$p\in P_\varepsilon/G_\alpha$, but for all
$s\in A\cut P_\varepsilon/G_\alpha$ there is no $t\in
P_\varepsilon/G_\alpha$ extending both $p$ and~$s$.''}$$

Since $r \forces {}$``$p\on \alpha\in G_\alpha$,'' $r$ and $p\on
  \alpha $ are       compatible,
so  we may wlog assume $r \stronger p\on \alpha$.  Let $\bar p := p
\land r$, then $\bar p \stronger p$ and $\bar p \on \alpha \stronger
   r$. So 
  $$ \bar p \on \alpha \forces_\alpha
\vtop{\parindent=0cm\hsize=0.7\hsize
     ``$ \bar p \in  P_\varepsilon/G_\alpha$, 
       and for all $s\in A\cut P_\varepsilon/G_\alpha$ there is no
  $t\in 
       P_\varepsilon/G_\alpha$ extending  $\bar p$ and~$s$.''}$$
Let $s\in A$ be compatible with $\bar p$, and let $t \stronger s,\bar
       p$. Then $t\on \alpha \forces t\in
  P_\varepsilon/G_\alpha\logand  
       t \stronger s \logand t \stronger \bar p$, a contradiction,
because $t\on \alpha \stronger \bar p \on \alpha$. 





      
\PROCLAIM\quotFactB/Fact:  Assume $G_\alpha \subseteq P_\alpha$ is generic
over $V$, and $G_{\alpha \varepsilon} \subseteq
P_\varepsilon/G_\alpha$ is generic over~$V[G_\alpha]$. 
Then 
\begindent
\ite 1 $G_{\alpha\varepsilon} \subseteq P_\varepsilon$ is a filter. 
\ite 2 $G_{\alpha\varepsilon}$ is generic for $P_\varepsilon$ over
$V$. 
\ite 3 $G_{\alpha\varepsilon} \supseteq G_\alpha$.
\ite 4 $G_\alpha =  G_{\alpha\varepsilon}\cut P_\alpha$.
\endent
\ENDPROCLAIM
      
Proof: (1)  $G_{\alpha \varepsilon} \subseteq P_\varepsilon$ follows
  from 
$P_\varepsilon/G_\alpha \subseteq P_\varepsilon$.  Any two conditions
$p,q$ in $G_{\alpha\varepsilon}$ have a common extension in
$G_{\alpha\varepsilon}$, i.e., there is a $r\in
G_{\alpha\varepsilon}$, $p \weaker_{\alpha\varepsilon} r$, $q
 \weaker_{\alpha\varepsilon} r$.  Hence $p \weaker_\varepsilon r$, $q
 \weaker_\varepsilon r $.   


(2): Let $A \subseteq P_\varepsilon$ be a maximal antichain in~$V$.
Then in $V_\alpha$, $A \cut P_\varepsilon/G_\alpha$ is a maximal
antichain by   \quotFactA/(3).  So $G_{\alpha\varepsilon}\cut (A\cut
P_\varepsilon/G_\alpha)$ and thus also $G_{\alpha\varepsilon} \cut A$
are nonempty. 

Proof of (3): Assume $p\in G_\alpha$ but $p\notin
G_{\alpha\varepsilon}$. Then there is a condition $q\in
G_{\alpha\varepsilon}$ such that $q \perp_{\alpha\varepsilon} p$.  As
     $p\on \alpha$, $q\on \alpha\in G_\alpha$, there is a condition
     $r\in G_\alpha$ such that $r \stronger p\on \alpha, q\on \alpha$.
     Then $(q\land r)\on \alpha = r \stronger_\alpha      p$, so
     $q\land r \stronger_\varepsilon p$.  We also have $q\land r
     \stronger q$, and $q\land r \in P_\varepsilon / G_\alpha$.  This
     contradicts $q \perp_{\alpha\varepsilon} p$. 


(4): ``$\subseteq$'' follows from (3), and if $p\in
G_{\alpha\varepsilon} \cut P_\alpha$, then $p\in
P_\varepsilon/G_\alpha$, so $p=p\on \alpha \in G_\alpha$. 
\medskip


(Conversely, if $G_\varepsilon \subseteq P_\varepsilon$ is generic
  over 
$V$, and $G_\alpha:=G_\varepsilon\cut P_\alpha$, then $G_\alpha$ is
generic for  over $V$, and $G_\varepsilon \subseteq
P_\varepsilon/G_\alpha$ is generic over~$V[G_\alpha]$.)



So we can write $G_\varepsilon$ for $G_{\alpha \varepsilon}$.




 
\medskip



\PROCLAIM\quotfactC/Fact:  The map $i:P_\varepsilon \to P_\alpha *
(P_\varepsilon/G_\alpha)$, defined by 
$$ i(p)  = \<p\on \alpha, \widehat p>$$
is a dense embedding.  Hence, forcing with $P_\varepsilon$ amounts to
the same as first forcing with $P_\alpha$, and then with the
``quotient forcing''~$P_\varepsilon/G_\alpha$.
\ENDPROCLAIM

Proof: Note that $p \on \alpha \Forces_{\alpha}``$p\in
P_\varepsilon/G_\alpha$''$, so $\rng(i) \subseteq P_\alpha *
P_\varepsilon/G_\alpha$.   $i$ preserves the ordering, as $p \weaker q
$ clearly implies $q\on \alpha \forces \widehat p \weaker \widehat q$.
  

To show that $i$ is dense, let $\<r,\name s>\in P_\alpha *
P_\varepsilon/G_\alpha $.  So $r \forces_\alpha \name s\on \alpha \in
G_\alpha$.  Since $r \forces \name s\in P_\varepsilon$, we can find a
stronger  condition $r_0\in P_\alpha$ and a condition $s_0\in
P_\varepsilon$ such that $r_0 \forces \name s = s_0$.  As $r_0
\forces_\alpha s_0\on \alpha\in G_\alpha$, $r_0$ and $s_0\on \alpha $
are compatible, say $r_1  \stronger r_0, s_0\on \alpha$.   

Let $p:= s_0\land r_1$. 
Then $p\in P_\varepsilon$, $p \stronger s_0$, so $\<r,\name s >
\weaker \<r_0, \name s > \weaker \<r_0, \widehat s_0> \weaker 
 \<r_1, \widehat s_0> \weaker \<p\on \alpha , \widehat p>$. 


%\bigskip
%
%
% We will also use the following easy fact: 
%
%\PROCLAIM\denseEfact/Fact: 
%$$ \forces_\alpha \hbox{``If $E \subseteq Q_\alpha$ is open dense,
%   then $\bar E:= \{r\in P_{\varepsilon}/G_\alpha: r(\alpha)\in E\}$ is open
%   dense in $P_\varepsilon / G_\alpha$.''}$$
%

\goodbreak
\bigskip




How can we describe the forcing notion $P_\varepsilon/G_\alpha$ without
explicitly mentioning $P_\varepsilon$?  For example, comparing the
forcing notions $P_\alpha$ and 
$P_{\alpha+1}$, we have 
$$ P_{\alpha+1} \approx P_\alpha * Q_\alpha$$
and also 
$$ P_{\alpha+1} \approx P_\alpha * (P_{\alpha+1}/G_\alpha)$$
Similarly, 
$$ P_{\alpha+2} \approx P_\alpha * Q_\alpha * Q_{\alpha+1}$$
and also 
$$ P_{\alpha+2} \approx P_\alpha * (P_{\alpha+2}/G_\alpha)$$

This suggests that the forcing notions $P_{\alpha+{\beta}}/G_\alpha$
are isomorphic to iterations of length~${\beta}$.  Theorem
\intermediate/ below shows that this is indeed the case. 
%
%\PROCLAIM\iterequivDef/Definition:  Let $\<P_\alpha, Q_\alpha:
%	\alpha<\varepsilon>$ be an iteration.   For $p,q\in
%	P_\varepsilon$ we define  $p\equiv q$ iff 
%for all $\alpha<\varepsilon$, $p\on \alpha \forces
%	p(\alpha)=q(\alpha)$.  
%
%It is easy to see (by induction) that $\equiv$ is an equivalence
%	relation, and clearly $p\equiv q $ implies $p \stronger q$. 





\PROCLAIM\intermediate/Theorem: Assume $\<P_\alpha,
Q_\alpha:\alpha<\varepsilon>$ is a  countable support iteration of
proper forcing notions, or a finite support iteration.  Let
$\alpha+ {\beta} =\varepsilon$.    Then there exists a $P_\alpha$ name
$\<\bP_{\gamma}, \bQ_{\gamma}:{\gamma}<{\beta}>$ of a countable/finite
support iteration of length ${\beta}$, such that 
$$\forces _\alpha \forall {\gamma}\le {\beta}: \bP_{\beta} \approx
P_\varepsilon/G_\alpha$$ 
\ENDPROCLAIM

Proof:  We will fix $\alpha$, and proceed by induction on~${\beta}$.
We will work in $V[G_\alpha]$, where $G_\alpha \subseteq P_\alpha$ is
generic over~$V$. 


\def\imap{i_{\alpha {\beta}}}
\def\imapx_#1{\def\next##1+##2{{##1##2}}
i_{\next#1}}

By induction on ${\beta}$, we will 
\begindent
\ite 1 define a countable/finite support iteration $\<\bP_{\gamma},
	\bQ_{\gamma}:{\gamma}<{\beta}>$ 
\ite 2 define a map $\imap$ from $P_{\alpha+{\beta}}/G_\alpha$ into
	$\bP_{\beta}$
\ite 3 prove that $\imap$ is a dense* embedding.
\endent
      
Case 1:  ${\beta}=0$
\begindent
\ite 1 
       $\<\bP_{\gamma},	\bQ_{\gamma}:{\gamma}<{\beta}>$ is the
	empty sequence, and $\bP_{\beta} = P_0 = \{\emptyset\}$
\ite 2  $\imap$ is the constant map.
\ite 3  Any two conditions in $P_{\alpha+0}/G_\alpha$ are compatible, as
  are any two conditions in $\bar P_0$. 
	$p_1\le^* p_2$ is true for all $p_1, p_2\in
	P_\alpha/G_\alpha$.  
\endent

Case 2: ${\beta}={\beta} '+1$
\begindent
\ite 1  We have to define $\bar Q_{{\beta}'}$. 
\item{} In $V$, $\nQ_{\alpha+ {\beta} '} $ is a
	$P_{\alpha+\beta'}$-name for a forcing notion, which can be
	translated into a $P_\alpha$-name for a
	$P_{\alpha+\beta'}/G_\alpha$-name.  So in $V[G_\alpha]$,
	$\nQ_{\alpha+\beta'}$ is a
	$P_{\alpha+\beta'}/G_\alpha$-name, which by induction
	hypothesis can be translated to a $\bP_{{\beta} '}$-name
	$\name{\bar Q}_{{\beta} '}$.
\ite 2 For $p\in P_{\alpha+\beta}/G_\alpha$, we define $\imap(p)\in
	\bar P_{\beta}$ by defining $\imap(p)\on {\beta} '$ and
	$\imap(p)({\beta} ')$: 
  $$ \imap(p)\on {\beta} ' = \imapx_{\alpha+\beta'} (p\on
	({\alpha+\beta'}))$$
\item{}  If $p({\alpha+\beta'})$ is undefined, we let
	$\imap(p)({\beta} ')$ be undefined.  Otherwise,
	$p({\alpha+\beta'}) $ is (in $V[G_\alpha]$) a
	$P_{\alpha+\beta'}/G_\alpha$-name for an element of
	$Q_{\alpha+\beta'}$, which can be translated to a $\bar
	P_{{\beta} '}$-name for an element of $\bar Q_{{\beta} '}$.  This
	will be~$\imap(p)({\beta} ')$.  Or, more sloppily:
	$\imap(p)({\beta}' = p(\alpha + {\beta} ')$. 
\item{}  Note that $\imap$ extends~$\imapx_{\alpha+\beta'}$. 
\ite 3 To see that $\imap$ is an embedding, check that for $p_1,
	p_2\in P_{{\alpha{+}\beta}}$, 
% the spacing looks better with {+} than with + 
  $$\eqalign{
  p_1 \weaker^* p_2  \quad \hbox{ iff }& \quad  p_1\on {\alpha{+}\beta'}
	\weaker^* p_2 \on {\alpha{+}\beta'}  \ \logand \cr 
    &\qquad \logand \ 
	p_2\on {\alpha{+}\beta'}  
  \forces p_1({\alpha{+}\beta'} ) \weaker^* p_2({\alpha{+}\beta'})\cr}$$
        which by induction hypothesis and using translation functions
        is equivalent to 
$$\eqalign{
p_1 \weaker^* p_2  \quad \hbox{ iff }& \quad 
 \imap( p_1) \on
	{\beta} ' \weaker^* \imap({p_2}) \on {\beta} ' \ \logand \cr
    &\qquad \logand \ 
        \imap({p_2})\on {\beta} ' 
\forces \imap({p_1})({\beta}') \weaker ^*\imap({p_2})({\beta} ')\cr}$$
         i.e.,  $\imap({p_1})  \weaker^* \imap(p_2)$. 
\item{} It is also easy to see that $\imap$ is dense*.  
%In fact $\imap$
%	is onto a set of representatives for the equivalence relation
%	$\equiv$ (see \iterequivDef/). 
\endent
      

Case 3: ${\beta} $ is a limit ordinal. 
\begindent
\ite 1 We define $\bar P_{\beta} $ as the (countable/finite support)
	limit. 
\ite 2 We let  $\imap(p) := \bigcup_{\gamma<\beta}
	\imapx_{\alpha+{\gamma} }$. 
\ite 3 As before, we can show $p \weaker ^*q$ iff $\forall {\gamma}<{\beta}
	$, $p\on \alpha + {\gamma} \weaker ^* q\on \alpha +{\gamma}$
	iff $\forall {\gamma} <{\beta} $ $\imap(p)\on {\gamma} \le^* $
	etc. 
\endent
\def\bp{\bar p}
The crucial point is the density condition \densedef/(2).  So let
$\bp\in \bar P_{{\beta}}$.

First we will deal with the case of a finite support iteration.  So
$\bp\in \bar P_{\gamma}$, for some~${\gamma}<{\beta}$. By induction
hypothesis we can find $p\in P_{\alpha+{\gamma}}/G_\alpha$ such that
$\imapx_{\alpha+{\gamma}}(p) \stronger^*_{\bar P_{\gamma}} \bp$. 

Then we also have $p\in P_{\alpha+{\beta}}/G_\alpha$, and $\imap(p) =
\imapx_{\alpha+{\gamma}}(p) \stronger_{\bar P_{{\beta}}}\bp$. 
%
%[Note that $r \stronger_{P_{\alpha+{\gamma}}/G_\alpha} s  \ \limpl \ 
%r \stronger_{P_\alpha+ {\gamma}} s \ \limpl \  
%r \stronger_{P_\alpha+ {\beta}} s \ \limpl \  
%r \stronger_{P_{\alpha+{\beta}}/G_\alpha} s$.]


\medskip

Now assume that we are working with a countable support iteration of
proper forcing notions.  (If ${\beta}$ has cofinality $>\omega$ in
$V[G_\alpha]$, we can repeat the previous proof verbatim.)

In general, let $\bar p \in \bar P_{\beta}$. In $V[G_\alpha]$,
  $\dom(p)$ is a countable set of ordinals, whichis not necessarily an
  element of~$V$.  

Here we can use the fact that $P_\alpha$ is proper: By \propercover/,
  $\dom(\bar p)$ is covered by a countable set of ordinals that itself
  lies in~$V$.  So there is a countable set $F\in V$  such that
  $\dom(\bp) \subseteq \{{\gamma}: \alpha+{\gamma} \in F\}$. 

Find a name $\name {\bp}\in V$ for~$\bp$.  From $\name {\bp}$ and $F$
we can define a condition $p\in P_{\alpha+{\beta}}$, $p\in V$ as
follows: 
\begindent
\item{} $\dom (p) = F$.
\item{} If $\alpha+{\gamma}\in F$, then let $p({\alpha+\gamma})$ be a
name such that (in $V$)
$$ \forces_{\alpha+\gamma}\vtop{\hbox{``If $\name \bp({\gamma})\in
Q_{\alpha+\gamma}$, then $p({\alpha+\gamma})=\name{\bp}({\gamma})$}
\hbox{\qquad\qquad\qquad\qquad otherwise
$p({\alpha+\gamma})=\emptycondition_{Q_{\alpha+\gamma}}$.}}$$
\endent
(We use the translation function here.) 

Because of  $F$ we know that $p$ is indeed a function with countable
  domain. So  $p\in P_{\beta}$, and in fact $\forces_\alpha p \in
  P_{\beta} / G_\alpha$.  

Now we have to show that $\imap(p) \stronger \bp$.  We have to prove by
  induction on ${\gamma}$ that 
  $$ \forall {\gamma} \le {\beta} \, \, \imap(p)\on {\gamma} =
  \imap(p\on \alpha + {\gamma}) \stronger^* \bp \on {\gamma}
  \eqno(*)$$

We leave this as an exercise to the reader (use  \factL/ and
	\factS/). 





%%% end of pres_forcing.tex

%------------------------------------------------------
%           ****** 7: pres csi  ********
%------------------------------------------------------		
%%% pres_theorem.tex  (from main_preserv, thesis version)

\neusection
\beginsection{\printchapternumber 5\quad A general preservation
        theorem  for countable support iteration}  






\PROCLAIM\context/Context:
\rm We will consider functions $f$  from $\omega $
   to $\omega  $.  In 
   applications, these functions may actually be from $\omega $ to
   $HF$ (the hereditarily finite sets), or from $\finSeq$ to
   $\finSeq$, etc.  Since we can trivially (in a primitive recursive,
   absolute, \dots) way code such functions by functions in $\fct$,
   all results from this section apply also to functions in
   $\pre{\omega}{HF}$, etc. 


 We fix a closed set $\C \subseteq \fct$.  There is a tree $T
   \subseteq \finSeq$ such that $$\C=\{f\in \fct : \forall n \, f\on n
   \in T\}.$$ When we work in a universe $V_1$, we write $\C$ for the
   set $\{f\in \fct\cut V_1 : \forall n \, f\on n \in T\}$, i.e., we
   regard $\C $ not as a set per se, but as a formula defining  a
   certain  (closed) set.


Typical examples are $\C=\fct$, or $\C=\{f\in\fct: \forall n
f(n)<H(n)\}$ for some~$H\in\fct$. 


  $ \<\re _n: n\in \omega > $ is an increasing sequence of two place
	relations  on~$\fct$.   In general, we do not assume that
these relations are transitive. 

   $\re _n$ will always be given by an arithmetical  definition.  Again,
we consider 
   $\re_n$ not as a set in itself, but rather as a definition of a
   certain arithmetical set, so if $\re_n$ is defined in a universe
   $V_0$, $f \re_n g$ makes sense even for $f, g\notin V_0$.   These
definitions will be absolute between any two ${\in}$-models, as the
formula defining $\re $ is arithmetical. 

(We do not require that the $\re_n$ are uniformly arithmetical, i.e.,
  each $\re_n$ may be defined by a different formula.  However, in all
  our applications there $ f \re_n g$ is expressed by a single
formula~$\varphi(f,g,n)$.)  



  We let $\re  = \bigcup_n \re_n$. 




A typical example is given by $f \re_n g $ iff $\forall k\ge n$
	$f(n)<g(n)$. Then we have $f \re g $ iff $f\le ^* g$.
(Actually, this example is not so ``typical''  since here the
relations $\re_n$ are all transitive, which will not be true in
general.) 
\ENDPROCLAIM



\PROCLAIM\incon/Definition:  
We will only consider forcing notions that add a real, or at least
   introduce a new $\omega$-sequence of ordinals.  If $p \forces \nt
   : \omega \to Ord$, we say that $p $ decides $\nt \on n$, if for
   some $t: n \to Ord$, $p \forces \nt\on n = t$. 
\ENDPROCLAIM

Note that if $\forces_Q \nt: \omega \to Ord$ and $\forces_Q \nt \notin
   V$, then letting $$E_n= \{p\in Q: \hbox{$p$ decides $\nt\on
   n$}\},$$ $E_n$ is a dense open subset of $Q$ and $\bigcap_n
   E_n$ is empty. 




\PROCLAIM\csAssume/Assumption:     We assume that for all countable sets
   $a \subseteq \fct$ there is a $g$ such that 
   $\forall f\in a\cut \C\,\,f \re g$. 

We also assume that for every $g$ and every $n$  the set $\{ f: f
	\re_n g\}$ is closed. 
\ENDPROCLAIM



\PROCLAIM\goodDef/Definition: We say that $g$ {\it  ($\rvec$,
$\C$)-covers\/}) $N$ if for all    $f\in N\cut \C$ we have $f \re g$.
(Usually we think of $N$ as a 
   countable elementary submodel of some~$H(\chi)$.)   When $C$ and/or
$\rvec$ are clear, we may just say ``$g$ covers $N$''. 
\ENDPROCLAIM




We let $\chi$ be a ``large enough'' regular cardinal as in
\chicon/. 
We will consider countable elementary submodels of $\<H(\chi), {\in}>$.
       



(The notions we will define below will depend on $\chi$,
but a careful examination (which we do will not carry out here) shows
that this dependence is only apparent.) 



\PROCLAIM\preservOne/Definition:  We
   say that the 
   forcing notion $Q$ {\bf almost  preserves} \rvec, if

  WHENEVER  $N\prec (H(\chi), {\in})$ is a countable model
containing $Q$, $\C$ and 
   $\rvec$,  $g$ covers $N$, $p\in Q \cut N$,   

  THEN  there exists an $N$-generic
   condition $q$ stronger than $p$,  such that $q \forces{} $``$g$
   covers~$N[G]$.'' 
\ENDPROCLAIM

\PROCLAIM\preserveCover/Fact: If  $Q$ almost preserves \rvec, then 
    $\forces_Q$``$\forall f \in V[G]\,\exists g \in V\,\, f \re g$''. 
\ENDPROCLAIM

Proof:  Assume not, so there is a condition $p$ and a name $\nf$
   such that $$ p \forces \hbox{there is no $g\in V$ such that $\nf
   \re g$.} $$ 

Let $N\prec H(\chi)$ be a countable model containing $\nf$ and $p$, and
   let $g$ ($\in V$) cover~$N$.  Then we can find a condition $q
   \stronger p $ forcing $\nf \re g$, a contradiction.

\PROCLAIM\ooExample/Example:   Let $\C=\fct$, and let  (for $f, g\in
   \fct$) $$f \re_n g  \ \liff\  \forall k\ge n\,    f(k)<g(k)$$
    and $f \re g$ iff for some $n$, $f \re_n g$.   All the $\re_n$ are closed
   and  transitive, and clearly for every countable set $a \subseteq
   \fct$ there is a $g$ such that $\forall f\in a\,\, f \re g$. 
\ENDPROCLAIM

   A forcing notion $Q$ is called $\fct$-bounding iff 
     $$ \forcess_Q \forall f\in \fct\cut V[G] \, \exists g\in
   \fct\cut V\,\, f \re g$$

Fact:   A proper forcing     notion $Q$ almost preserves $\rvec$  iff
   it is $\fct$-bounding.  (We will see later that we can omit the
   ``almost'' from  this statement.) 

Proof of the fact: If $Q$ preserves  $\rvec$, then $Q$ is
   $\fct$-bounding by \preserveCover/.   Conversely, assume that $Q$ is
   $\fct$-bounding, let $N \prec H(\chi)$, and assume that $g$ covers~$N$.
   Then $\forces \forall f\in N[G]\, \exists f'\in V: f \re f'$, so any
   $N$-generic condition $q$ forces 
      $ \forall f\in N[G] \exists f'\in N: f \re f'$.   Since for all
   $f'\in N$, $f'\re  g$ (and $\re $ is absolute and transitive), for any
   $N$-generic  $q$ we have $$q \forces \forall f \in N[G]: f \re g$$


\medskip

So this definition \preservOne/ achieves exactly what we want.
   However, it is not clear whether this condition by itself is
   preserved under iteration.  Before we give the definition we will
   actually use, we have recall the  concept of
   ``interpretation'': 

\PROCLAIM\interpret/Definition: Assume $Q$  is  a forcing notion,   $\nf_0$,
   \dots, $\nf_{k-1}$ are $Q$-names of functions in $\C$, $f^*_0$,
   \dots, 
   $f^*_{k-1}$  are 
   functions in $\fct$, $\sqn p $
   an increasing  sequence of conditions.   We will write $\bnffk$
   for  $\nffk$ and $\bffk$ for~$\ffk$.   A sequence $\nff {} k $ will
   be written as $\<\bnffk, \nf_k>$. 
\ENDPROCLAIM

We say that $\sqn p$
   interprets 
   $\bnffk $    as $\bffk$, if for all $i<k$, for all $n$,
        $p_n \forces \nf_i\on n  =  f^*_i\on n$.  


(So when we say that $\sqn p $ interprets $\bnffk$ as $\bffk$, it is
   understood that the sequence  $\sqn p$ is increasing, etc.)

\PROCLAIM\interCrem/Remark:  If $\sqn p$ interprets $\nf$ as $f^*$, where
   $\nf$ is a name for a function in $\C$, then $f^*$ is a function in~$\C$.   
\ENDPROCLAIM

Proof:  $\C = \{f: \forall n \, f\on n\in T\}$ for some tree~$T$.   If
   $f^*\notin \C$, then for some $n$ $f^*\on n \notin T$, so $p_n
   \forces \nf \on n \notin T$, a contradiction. 
\medskip

\PROCLAIM\inconDef/Definition: We say that  the sequence $\sqn p \in
   \pre{\omega}{Q}$ is
   inconsistent, if there is no condition $q$ such that $\forall n\, q
   \forces  p_n\in G$ or equivalently, $\forces_Q \exists n: p_n\notin G_Q$.
   Note that if $\<D_{Q,n}:n\in \omega>$ is a sequence of dense open
   sets with $\bigcap_n D_{Q,n} = \emptyset$ and $\forall n\, p_n \in
   D_{Q,n}$, then $\sqn p $ is inconsistent.
\ENDPROCLAIM

(By our assumption in \incon/, for every forcing notion
   $Q_\alpha$ that we consider there is a sequence $\<D_{Q,n}: n<
   \omega>$ as above.)

\PROCLAIM\preservDef/Definition:    We    say that the 
   forcing notion $Q$ {\bf  preserves} $(\rvec, \C)$, if for some~$x$: 

  WHENEVER  $N\prec H(\chi)$ is a countable model containing $Q$, $x$ and
   $\rvec$,  $g$ covers $N$, $p_0\in Q \cut N$,   and whenever  $\sqn
   p\in \erp Q^\omega \cut N$ (an increasing 
   sequence of conditions) interprets $\bnffk\in N$ as $\bffk$, such
   that for    all $i<k$ $\sf_i \re _{n_i} g$, 

 THEN there is a condition     $q\in   Q$  such that
\begindent
\item {{\bf (a)}}  $q \stronger p$. 
\item {{\bf (b)}} $q$ is $N$-generic.
\item {{\bf (c)}} $q \forces \forall f\in N[G] \cut \C\,\, f \re g$,
  i.e., $q \forces$``$g$ covers~$N[G]$.'' 
\item {{\bf (d)}}  $ \forall i<k$: $ q \forces \nf_i \re _{n_i} g$. 
\endent
\ENDPROCLAIM

Note that (a)--(c) just say that $Q$ almost preserves \rvec.    Also
   note that (c) is equivalent to 
\begindent
\item {{\bf (c')}} $\forall \nf \in N$:  If\  $\forces_Q \nf\in \C$, then
   $q \forces \nf \re g$. 
\endent
      

When $\C$ is clear from the context (or irrelevant), we may say ``$Q$
preserves \rvec'' instead of ``$Q$ preserves $(\rvec,\C)$''. 

We call $x=x_Q$ the ``witness'' for the statement ``$Q$ preserves
   \rvec.'' 

\bigskip

\PROCLAIM\composeCover/Lemma: If $Q_0$ preserves \rvec, and
   $\forces_{Q_0}$``$ \name Q_1$    preserves \rvec'', then
   $Q_0*\name Q_1$    preserves \rvec. 
\ENDPROCLAIM

{\it Idea of the proof:} To use the assumptions on $Q_0$ and $Q_1$, we
 have to find a $Q_0$-name $\name{\bar f}'$ that ``interpolates'' between
  $\bnffk$ and $\bsnffk$, i.e., $\bsnffk$ is an interpretation of
  $\name{\bar f}'$ which itself (in $V^{Q_0}$) is an interpretation
of~$\bnffk$.  

\medskip



Proof:  Let $x_0$ witness that $Q_0$ preserves \rvec, and
   $\forces$``$\name x_1$ witnesses that  $Q_1$ preserves \rvec''.
   $x:=\<x_0, \name x_1>$ will witness that $Q_0 * Q_1$ preserves \rvec. 

Assume $N$, $\sqn p$, $\bnffk$, $\bffk$, $n_0, \ldots, n_{k-1}$
   are as in \preservDef/, and $g$ covers~$N$.  Each $p_n$ is of the
   form $\<p_n(0), 
   p_n(1)>$, where $p_n(0)\in Q_0$ and $p_n(0) \forces_{Q_0} p_n(1)\in
   \nQ_1$.  We let $p_{-1}:= \<\emptycondition_{Q_0},
   \emptycondition_{\name Q_1}> $. 

Let $G(0) \subseteq Q_0$ be generic, then we can define functions
  $f'_i $ in $V[G(0)] $ and conditions $p'_n(1)$ in $Q_1$ for $i<k$ as
  follows:

\begindent
\item {} If for all $n\in \omega$ $p_n(0)\in G(0)$, then $f'_i:=\sf_i$,
   $n^* := \omega$, $p'_n(1):= p_n(1)$. 
\item{} Otherwise, let $n^*:=\max \{n\ge -1: p_n(0)\in G(0)\}$, and
  find a  sequence $\<p'_n(1): n\in \omega>\in \erp{Q_1}^\omega $ and
   functions $f'_i$ 
   for $i<k$ such that $p'_0(1)\ge p_{n^*}(1)$ and 
$$ \hbox {$\<p'_n(1): n<\omega>$ interprets $\bnffk$ as $\bpffk$} 
    		\eqno (*1) $$
\item{}   (Note that $(*1)$ will be true also if~$n^*=\omega$.) 
\endent


Then  $f'_i\on n^* = \sf\on n^*$: This is clear if~$n^*=\omega$.
   Otherwise,  $p'_{0}(1) \forces_{Q_1}$``$\nf_i\on n^* =
   f_i^*\on n^*$,'' so we also have  $p'_{n^*}(1)
   \forces_{Q_1}$~``$\nf_i\on n^* = 
   f_i^*\on n^*$.'' 

 Furthermore,  $p'_{n^*}(1) \forces$~``$\nf_i\on
   n^* = f'_i\on 
   n^*$'', so  $p'_{n^*}(1) \forces$~``$f'_i\on n^*=f_i^*\on n^*$.''

Coming back to $V$, we can find $Q_0$-names $\nf'_i$, $\np'_n(1)$,
   $\name n^*$   such that the
   above    is forced. In particular, $$p_n(0) \forces f'_i\on n =
   \sf_i\on n,\eqno(*0)$$    as $p_n(0) \forces \name n^*\ge n$. 

We can find these names $\nf'_i$ and $\name p'_n$ in~$N$.  Since $Q_0$
   preserves    \rvec, by $(*0)$  there is a generic $q(0)\in Q_0$ such
   that 
\begindent
\item {($\hbox{a}_0$)}  $q(0) \ge p_0(0)$. 
\item {($\hbox{b}_0$)} $q(0)$ is $N$-generic 
\item {($\hbox{c}_0$)} $q(0) \forces \forall f\in N[G(0)] \,\, f \re g$.
\item {($\hbox{d}_0$)}  $ \forall i<k$: $ q(0) \forces \nf'_i \re _{n_i}
   g$. 
\endent
Working again in $V[G(0)]$, where $q(0)\in G(0)$, we note that $N[G(0)]$
   is covered by $g$ and $n^*\ge 0$,  so since $Q_1$ preserves \rvec{}
   and by $(*1)$, we 
   can find a condition $q(1)\in Q_1$ such that       
\begindent
\item {($\hbox{a}_1$)}  $q(1)  \stronger p'_0(1) \stronger p_0(1)$. 
\item {($\hbox{b}_1$)} $q(1)$ is $N[G(1)]$-generic 
\item {($\hbox{c}_1$)} $q(1) \forces \forall f\in N[G(0)*G(1)] \,\, f \re g$.
\item {($\hbox{d}_1$)}  $ \forall i<k$: $ q(1) \forces \nf_i \re _{n_i} g$. 
\endent
\bigskip
We can find a name $\name q(1)$ such that the above is forced by~$q(0)$.
Now we let $q = \<q(0), \name q(1)>$.  Then 
   \preservDef/(a)--(d) holds. 
\medskip


Recall that 
  $P_\beta/G_\alpha = \{ p \in P_\beta: p\on \alpha \in G_\alpha\}$,
and that the map 
   $i:P_{\beta} \to P_\alpha * P_{\beta}/G_\alpha$, defined by $i(p) =
   \<p\on \alpha, p>$ is a dense embedding.  So  to each $P_{\beta}$
   name $\nf$ there is a naturally 
   corresponding $P_{\alpha }$-name for a $P_{\beta}/G_\alpha$-name,
   which we also call~$\nf$. 



\medskip

For the following, assume that  
 $\<P_\alpha,    Q_\alpha: \alpha<{\varepsilon}>$   is a countable
support iteration    \rvec-preserving forcing notions, i.e., for all
$\alpha< {\varepsilon}$, 
    $$ P_\alpha \forces \hbox{``$Q_\alpha$  preserves \rvec (witnessed
		by $\name x_\alpha$.''} $$
Also assume  that each $Q_\alpha$ adds a new sequence of ordinals.


Our goal is to show that $P_\varepsilon$ preserves $\rvec$ (witnessed
by~$x:=\<\nx_\alpha:\alpha<\varepsilon>$.   So we fix a countable
elementary model $N$ containing all relevant information. 

\medskip


\PROCLAIM\pInduction/Induction Lemma: Let $ \alpha\le{\beta} \le 
   \varepsilon$. Assume that  $\sqn {\name p} \in N$ is a
   sequence of $P_\alpha$-names for conditions in $P_{\beta}/G_\alpha$
   such that  
\begindent
\item {($\cdot$)}       
$\forces_\alpha \sqn {\name p}$ interprets $\bnffk $ as $\bsnffk$ 
\endent
(where $\bnffk=\<\nf_0, \ldots, \nf_{k-1} >$, $\bsnffk=\nff * k-1 $,
        the $\nf _i$ are 
   $P_\beta $-names in $N$, and the
   $\nsf_i$ are    $P_\alpha$-names).  Furthermore, assume that  $q\in
   P_\alpha $, and $\name n_0, \ldots, \name n_{k-1}$ are
   $P_\alpha$-names for integers such that for some $g$:  
\begindent\rightskip=0.1\rightskip
\item{(a)} $q\forces_\alpha{\name p}_0\on\alpha\in G_\alpha$.  (This 
   really follows from our assumption that $\forces_\alpha \np_0 \in
   P_{\beta}/G_\alpha$.) 
\item{(b)} $q\in P_\alpha$ is $N$-generic. 
\item{(c)} $q \forces \forall f\in N[G_\alpha] \,\, f \re g$.
\item{(d)}  $ \forall i<k$: $ q \forces \nsf_i \re _{\name n_i} g$. 
\endent


 Then there exists $q^+\in P_\beta$,  satisfying 
\begindent
\item{ ($+$) }      $q^+\on \alpha = q$
\item{\toplus(a)} ${q^+} \forces_\beta 
      {\name p}_0\on \beta\in G_{\beta} $.  
\item{\toplus(b)} ${q^+}\in P_\beta$ is $N$-generic (i.e., $q^+
   \forces_{\beta} $ ``$G_{\beta}\cut N$ is generic over $N$''.)
\item{\toplus(c)} ${q^+} \forces \forall f\in N[G_\beta] \,\, f \re g$.
\item{\toplus(d)}  $ \forall i<k$: $ {q^+} \forces \nf_i \re _{\name
   n_i} g$.  
\endent
\ENDPROCLAIM



The reason for considering $\rvec$-preserving forcing notions is the
following corollary: 

\PROCLAIM\mainCor/Corollary: If $\forall \alpha \,\,
   \forces_{ P_\alpha}{}$``$Q_\alpha$  preserves \rvec'', then
   $P_\varepsilon $ 
   preserves \rvec.   
\ENDPROCLAIM

 Proof of the corollary:  Use the induction lemma with with
   $\alpha=0$, ${\beta}=\varepsilon$,~$q=\emptycondition_{P_0}$.  We
   can find $q^+\in P_\varepsilon$ satisfying \toplus(a)--\toplus(d).
   Since $q^+  \forces p_0\in G_\varepsilon$, there is a condition
   $q^{++} \stronger q^+$, $q^{++} \stronger p_0$.  Then $q^{++} $
   will satisfy \preservDef/(a)--(d). 

\medskip


To prove the case ``${\beta}$ limit'' of the  induction lemma, we will
need the following  lemma.   (Note that, as in the preliminary lemma
for the proof of preservation of    properness, this lemma does not
mention properness,    \rvec-preservation, etc. --- not  even
countable models.)




\PROCLAIM\pPrelim/Preliminary lemma:  Assume $\alpha_1 < \alpha_2 \le
   {\beta}$,  $\sqn {\np^1} $ is a sequence of $P_{\alpha_1}$-names for
   conditions in~$P_{\beta}/G_{\alpha_1}$.  Let $D
   \subseteq    P_{\beta}$ be a dense open set, $j\in \omega$. 


Assume $\<\bnffk, \nf_k> =  \nff {} k $ are $P_{\beta}$-names, and
   $\bOnenff = \nff 1 k-1 $ are 
   $P_{\alpha_1}$-names, and 
\begindent
\ite 1  $\forces_{\alpha_1}$ $\sqn {\np^1}$ interprets $\bnffk $ as
   $\bOnenff  $. 
\ite 2  
 $\forces_{\alpha_1} \<\np^1_n(\alpha_1):n<\omega>$ is
   inconsistent. 
\endent




THEN there are: $P_{\alpha_2}$-names $\<\bTwonff, \nf^2_k> = 
   \nff 2 k $ and a sequence $\sqn
   {\name p^2}$ of $P_{\alpha_2}$-names for conditions in
   $P_\beta/G_{\alpha_2}$ such that  
\begindent\rightskip=2\rightskip
\item{\toplus(1)}\vtop{\def\\#1{\advance\hsize by
  -#1\relax#1=0cm\relax}
  \\\parindent\\\leftskip\\\rightskip\advance\rightskip by 0cm plus 1
  cm minus 1 cm
  \hangindent=1cm\hangafter=1 $\forces_{\alpha_2}$``$\sqn {\name p^2}$ 
  interprets     
   $\<\bnffk, \nf_k> $ as 
   $\<\bTwonff, \nf^2_k>$'' and $\forces_{\alpha_2}$``$\name p^2_0 $
   decides $\nf _0\on j, \ldots, \nf_{k} \on j$.''}
\item{\toplus(2)} 
 $\forces_{\alpha_2} \<\np^2_n(\alpha_2):n<\omega>$ is
   inconsistent. 
\item{\toplus(3)} $\forces_{\alpha_1} \< \np^1_n\on
   \alpha_2:n<\omega>$ interprets 
   $\bTwonff  $ as    $\bOnenff  $. 
\item{\toplus(4)} $\forces_{\alpha_2} $ If $\np^1_n\on
   \alpha_2\in G_{\alpha_2}$, 
   then $\name p^2_0 \stronger \np^1_n$. 
\item{\toplus(5)} $\forces_{\alpha_2} \name p^2_0\in D$. 
\endent
\ENDPROCLAIM



\medskip



\begingroup
\midinsert
\def\sm#1 {\hfill$\smash{{}_{#1}}$\hfill}
\offinterlineskip
\medskip
\def\marker{\vrule height 2pt depth 2pt}
\def\rul{\omit\hrulefill}
\def\rula{\omit\hfill\hrulefill}
\def\rulo{\omit\hrulefill\hfill}

\def\skp#1 {\noalign{\vskip #1 true pt\relax}}
$$\hbox{\vtop{
\ialign{#&\hidewidth$#$\hidewidth&
          #&
          \hidewidth$#$\hidewidth&
                         #&
             \hidewidth$#$\hidewidth\cr          
\omit\vphantom{$\bTwonff$}\cr
\skp10
\omit\vphantom{\hbox to 1pt{\hrulefill}}\cr
\skp13
&\bOnenff&\multispan3{\sm p^1_n }  &\bnffk\cr
\skp 10
&\rula&\rul&\rul&\rul&\rulo\cr
\skp40
\hrulefill&\omit\hrulefill\marker\hrulefill&\omit
\hrulefill&\omit\hrulefill\marker\hrulefill&\omit
\hrulefill&\omit\hrulefill\marker\hfill\cr
\skp 7
&\alpha_1&&\alpha_2&&{\beta}\cr
\omit\quad&\omit\quad&
       \omit\qquad\qquad\quad&
          \omit\quad&
       \omit\qquad\qquad\quad&
\omit\quad\cr
}}\qquad \lower 20pt\hbox{$\Longrightarrow$}\ \vtop{
\ialign{#&\hidewidth$#$\hidewidth&
          #&
          \hidewidth$#$\hidewidth&
                         #&
             \hidewidth$#$\hidewidth\cr          
&&&\bTwonff, \nf^2_k&\sm p^2_n &\bnffk,\nf_k\cr
\skp 10
&&&\rula&\rul&\rulo\cr
\skp 13
&\bOnenff &\sm p^1_n\on\alpha{} &\bTwonff\cr
\skp 10
&\rula&\rul&\rulo\cr
\skp40
\hrulefill&\omit\hrulefill\marker\hrulefill&\omit
\hrulefill&\omit\hrulefill\marker\hrulefill&\omit
\hrulefill&\omit\hrulefill\marker\hfill\cr
\skp 7
&\alpha_1&&\alpha_2&&{\beta}\cr
\omit\quad&\omit\quad&
       \omit\qquad\qquad\qquad\quad&
          \omit\quad&
       \omit\qquad\qquad\qquad\quad&
\omit\quad\cr
}}}$$
\endinsert
\endgroup





      

{\bf Proof of the preliminary lemma:}

We will work in~$V[G_{\alpha_2}]$.   
We write $p^1_n$ for~$\np^1_n[G_{\alpha_1}]$.  Let $p^1_{-1}:=
   \emptycondition_{P_{\beta}}$. 
Let ${n^*}$ be  defined by 
\begindent
\ite i  $n^* := \max\{n\ge -1: \np^1_n[G_{\alpha_1}]\on \alpha_2 \in
   G_{\alpha_2} \}$. 
\endent

(By \pPrelim/(2), not all $p^1_n\on \alpha_2$ can be in~$G_{\alpha_2}$.) 	

Let $p^2_{-1} = p^1_{{n^*}}\in P_{\beta}/G_{\alpha_2}$.   By
   assumption on $Q_\alpha$, there is a 
   sequence $\sqn E $ of dense open subsets of $Q_{\alpha_2}$ such
   that $\bigcap_n E_n$ is empty.  Let $\bar E_n:=\{r\in
   P_{\beta}/G_{\alpha_2}: r({\alpha_2})\in E_n\}$.  Then $\bar E_n $ is
   a dense open subset of $P_{\beta}/G_{\alpha_2}$, and $\bigcap_n
   \bar E_n$ is empty. 
      

For each $n$, let $$ D^n := D \cut \bar E_n \cut\{r\in
   P_{\beta}/G_{\alpha_2} : r    \hbox{ decides } 
   \nf_0\on \max\{n,j\}, \ldots, \nf_k\on\max\{ n,j\}\}.$$
   Then $D^n$ is
   open dense   in~$P_{\beta}/G_{\alpha_2}$.  By induction we can
   now find a 
   sequence of conditions  $p^2_n$ in $P_{\beta}/G_{\alpha_2}$
   such that for all    $n\in \omega$:  
\begindent  
\ite ii  $p^2_n$ in $P_{\beta}/G_{\alpha_2}$
\ite iii $p^2_{n-1} \weaker p^2_n$. (So if $p^1_n\on \alpha_2\in
   G_{\alpha_2}$, 
   then   $p^1_n \weaker p^1_{n^*} = p^2_{-1} \weaker p^2_n$.)
\ite iv  $p^2_n\in D^n$. 
\endent
Since $D^n \subseteq E_n$,  (iv) implies that
   $\<p^2_n({\alpha_2}):n<\omega>$ is    inconsistent.

      

By (iii) and (iv),  there are  functions $f^2_i$ such that  for all
   $i\le k$, all $n$: 
\begindent
\ite  v  $p^2_n \forces_{\alpha_2,{\beta}}\nf_i\on \max\{n,j\} = 
   f^2_i\on \max\{n,j\}$. 
\endent

Coming back to $V$, we can find $P_{\alpha_2}$-names $\np^2_n$,
   $\nf^2_i$, $\name n^*$ 
   such that (i)--(v) are forced by the empty condition of~$P_{\alpha_2}$.   

Note that (v) implies that \pPrelim/\toplus(1) will be satisfied, (iv)
  implies \pPrelim/\toplus(2) and \pPrelim/\toplus(5), and (iii)
  implies \pPrelim/\toplus(4).

To show \pPrelim/\toplus(3), let $G_{\alpha_1} \subseteq P_{\alpha_1}
  $ be any generic filter, $n\in \omega$,~$i<k$.  We will write $p^1_n
  $ for $\np^1_n[G_{{\alpha_1}}]$, $f^1_i$ for $
  \nf^1_i[G_{\alpha_1}]$.


 We claim that $$V[G_{\alpha_1}] \thinks 
       p^1_n\on \alpha_2 \forces_{\alpha_1,\alpha_2} 
       \nf^2_i\on n = f^1_i\on n$$

Proof of the claim: Let $H \subseteq P_{\alpha_2}/G_{\alpha_1}$ be a
   $V[G_{\alpha_1}]$-generic filter containing $p^1_n\on \alpha_2$.
   Then $H\cut P_{\alpha_1} =  G_{\alpha_1}$, and $H$ is generic for
   $P_{\alpha_2}$ over $V$, so we will write $G_{\alpha_2} $ for~$H$.
   Let $f^2_i = \name f^2_i[G_{\alpha_2}]$. 

 We have to check $V[G_{\alpha_2}] \thinks  f^2_i\on n = f^1_i\on n$.
   It is enough to show  that 
 $$ V[G_{\alpha_2}] \thinks p^2_n \forces_{P_{\beta}/G_{\alpha_2}}
     f^2_i\on n = \nf_i \on n = f^1_i\on n.$$

The first equality is clear by the definition of~$\nf^2_i$.   To prove
   the second, let $G_{\beta}$ be a $V[G_{\alpha_2}]$-generic filter
   on $P_{\beta}/G_{\alpha_2}$ containing~$p^2_n$. Again, $G_{\beta}
   \supseteq    G_{\alpha_2}$ is also generic for $P_{\beta}$ over
   $V$, and it contains~$p^1_n$. (Remember that $p^1_n\on \alpha_2 \in
   G_{\alpha_2}$, so by \pPrelim/\toplus(4), $p^2_n \ge p^1_n$.)
   Hence $V[G_{\beta}] \thinks
   \nf_i[G_{\beta}]\on n = f^1_i\on n $. 




\bigskip


{\bf Proof of the induction lemma:}  We proceed by
   induction on~${\beta}$.   

The successor step is similar to the proof of  \composeCover/: 

Assume $\<\np_n:n\in \omega>$ is a sequence of $P_\alpha$-names for
conditions in $P_{\beta+1}/G_\alpha$, interpreting $\bnffk$ as
$\bsnffk$ in~$V[G_\alpha]$.  (I.e., $\bsnffk$ is a $P_\alpha$-name,
and $\bnffk$ is a $P_{\beta+1}$-name which we identify with the
corresponding $P_\alpha$-name for a $P_{\beta+1}$-name.)

Working in $V_{\beta}$, we can define $\bpffk$, $n^*$, 
$\<p'_n:n\in \omega>$ such that the following hold: 
\begindent
\item {$\cdot$} $n^* = \sup(\{n\in \omega:p_n\on {\beta}\in G_{\beta}\}
              \cup \{-1\})$   (also $n^*=\omega$ is possible)
\item {$\cdot$} $\<p'_n:n\in \omega>$ is an  increasing sequence of
              conditions in $Q_{\beta}$, interpreting $\bnffk$ as~$\bpffk$. 
\item {$\cdot$}  If $n^*\in \omega $,  then $p'_0 \stronger
              p_{n^*}({\beta})$.
\item {$\cdot$}   If $n^* = \omega$, then $\bpffk = \bsnffk $. 
\endent
      
Coming back to $V$, we can find $P_{\beta}$-names $\name n^*$, etc.
   Now    $\<\np_n\on {\beta}:n\in \omega>$ is a sequence of names for
   conditions in $P_{\beta}/G_\alpha$ forced to interpret $\name{\vec
   f}'$ as $\bsnffk $, and $\<\np'_n:n\in \omega>$ is a sequence of
   $P_{\beta}$-names for conditions in $Q_{\beta}$ forced to interpret
   $\bnffk $ as $\name{\vec f}'$.  
   So we can use the induction hypothesis on $\alpha, {\beta}$  and
   the assumption on $Q_{\beta}$ to obtain $q^+\on {\beta}$ and
   $q^+({\beta})$, respectively.   

This ends the proof of the successor case. 

\medskip 





  Let $\beta $ be  a limit ordinal. 

  Let $\sqn D$ enumerate all dense open subsets of $P_\beta$ that are
   in $N$, where $D_0 = P_{{\beta}}$.  Let ${\delta} := \sup(N\cut
   {\beta})$, ${\delta} = \bigcup_j \alpha_j$,
   $\alpha=\alpha_0<\alpha_1<\cdots\,$, $\<\alpha_j:j\in \omega> \in N$.
   Fix $P_{\beta}$-names $\bnffk=\nff {} k-1 $ of functions.
   

Assume that
 $$\forces_{\alpha} \hbox{$\sqn {p} \in
   \erp\left(P_{\beta}/G_\alpha\right)^\omega$ interprets $\bnffk $ as
  $\bsnffk$ } \leqno(1)_0$$
 and let for $i<k$ $\name n_i$ be names of integers such that
   $\forces_\alpha \nf_i \re _{\name n_i} g$. 



First claim: wlog we may assume that 
 $$ \forces_{\alpha} \hbox{``$\<p_n(\alpha):n<\omega>\in
   \erp Q_\alpha^\omega$ is inconsistent''}
\leqno(2)_0$$
{\bf [%]
}Proof of first claim:  It is enough to find a sequence
   $\<p'_n:n<\omega>$ satisfying $(1)_0$ and  $(2)_0$ such that for
   all $n$, $\forces_\alpha p'_n \stronger^* p_n$.  

To find this sequence, we  work in~$V_\alpha$. If
   $\<p_n(\alpha):n<\omega>$ is inconsistent, we let~$p'_n:=p_n$.
   Otherwise, let $r_0\in Q_\alpha$ be a condition such that for all
   $n$, $r_0 \stronger^* p_n(\alpha)$, and let $r_0\le r_1 \le \cdots$
   be an increasing inconsistent sequence in~$Q_\alpha$.   Now let
   $p'_n := p_n\land r_n$, i.e., 
      $$ p_n'({\gamma}) = \cases{r_n&if ${\gamma} = \alpha$\cr
		   p_n({\gamma})& if ${\gamma} \not= \alpha$}$$
   Then $\<p_n':n<\omega> $ satisfies the requirements.  This proves
   the first claim.{%[
\bf]}
\medskip

 
Let $\sqn {\nf}$ enumerate all 
    names $\nf$ in $N$ satisfying
   $\forces_\beta \nf\in \C$.


We will construct sequences $\<{\<\np^j_n:n< \omega>}:j< \omega>$
 and 
  $\<{\<\nf^j_i:i<k+j>}: j<\omega>$ satisfying the following for all $j\in
   \omega$:  

\begindent
\def\phan{{\phantom{j+1}}}
\openup 2pt\relax
\item {$(\star)_\phan$} $\np^j_n$ is a  $P_{\alpha_j}$-name for an element of
         $P_\beta/G_{\alpha_j}$
\item {$(*)_\phan$} $\nf ^j_i$ a $P_{\alpha_j}$-name  for an element of $\fct$
\item{$(0)_{\phantom{j+1}}$}  $\<\np^0_n: n< \omega> = \<\np_n: n<
  \omega>$, $\<\nf^0_i:i<k> =    \<\nf_i:i<k>$. 
\def\ite#1 {\item{$(#1)_{j+1}$}}
\ite 1 $\forces _{\alpha_{j+1}}$
        ``\breaklines($\sqn {\np^{j+1}} \in
   \erp(P_{\beta}/G_{\alpha_{j+1}})^\omega $ interprets $\nff {}
   k+{j} $ as &
   $\nff {j+1} k+{j} $, and $\np^j_0$ decides $\nf_0\on j$, \dots,
    $\nf_{k+j}\on j$'')
\ite 2 $\forces_{\alpha_{j+1}} \<p^{j+1}_n(\alpha_{j+1}): n<\omega>$
   is inconsistent.
{\spaceskip=0.5em plus 1em minus 0.1em\advance\rightskip by 0pt plus
1cm minus 1cm\relax
\ite 3 $\forces_{\alpha_j}$ $\<\np^j_n\on \alpha_{j+1}: n < \omega> 
     \in \erp(P_{\alpha_{j+1}} /G_{\alpha_j})^\omega$
   interprets   $\nff j+1 k+j-1 $ as $ \nff j k+j-1 $.\vskip0cm}
\ite {4} $\forces_{\alpha_{j+1}} $ If $\np^{j}_0\on \alpha_{j+1}\in
   G_{\alpha_{j+1}}$,    then $\np^{j+1}_0 \stronger \np^{j}_0$.  
\ite 5 $\forces_{\alpha_{j+1}} \np^{j+1}_0\in D_{j+1}$  
\endent
       

Note that the statements $(1)_0$ and $(2)_0$ mentioned at the
  beginning of the proof are exactly $(1)_{j+1}$ and $(2)_{j+1}$ for~$j=-1$. 

We can obtain the sequences $\sqn {\np^{j+1}}$ and
   $\<\nf^{j+1}_i:i<k+j+1>$ 
   from the given sequences $\sqn {\np^{j}}$,
   $\<\nf^{j}_i:i<k+j+1>$ and $D_j$ by applying the preliminary
   lemma in $N$, so each $\<\np^j_n:n\in \omega>$ will be in~$N$. 

\medskip

Now we construct sequences $\<q_j:j<\omega>$ (where each $q_j$ is an
   $N$-generic 
   condition in $P_{\alpha_j}$) and $\<\name n_j:j<\omega>$ ($\name n_j$ a
   $P_{\alpha_j}$-name for an integer)  satisfying 
\begindent
\ite $\bullet$ $ \forces_{\alpha_{j+1}}$: If $\exists n\, \nf_{k+j}^j
   \re _{n} g$,    then $ \nf_{k+j}^j \re _{\name n_{k+j}} g$.  
\ite $+$ $q_{j+1} \on \alpha_j = q_j$. 
\ite A $q_{j+1} \forces  \name p^{j}_0\on   \alpha_{j+1}\in
   G_{\alpha_{j+1}}$. 
\ite B $q_{j+1}\in P_{\alpha_{j+1}}$ is $N$-generic. 
\ite C $q_{j+1} \forces \forall f\in  N[G_{\alpha_{j+1}}] \,\, f \re g$. 
\ite D $q_{j+1} \forces \forall i<k+{j+1}: \nf_i \re _{\name n_i} g$. 
\endent
      
We let $q_0 = q$. $\name n_0, \ldots, \name n_{k-1}$ are already defined. By
   assumption (a)--(d) of the induction lemma, (A)--(D) are now
  satisfied for~$j=-1$.  

       
Given $q_j$ and $\name n_0, \ldots, \name n_{k+j-1}$, we can easily find
   $\name n_{j+k}$ by requirement~$(\bullet)$.    Now apply the
   induction    assumption to the sequences $\sqn {p^j} $,
   $\<\nf_i:i<k+j>$, $\<\nf^j_i:i<k+j>$ 
 to get~$q_{j+1}$.   This will show that
   $q_{j+1} $    satisfies $(+)$, (A),  (B), (C).   The
   induction assumption    also implies 
   that  $q_{j+1}$  will satisfy  (D) for all~$i<k+j$.
   Finally, ($\bullet$) and (C) imply that (D) is also satisfied for~$i=k+j$.  

Note that $q_{j+1} \forces \name p_0^j \on \alpha_{j+1} \in
   G_{\alpha_{j+1}}$, so by ({4}), 
     $$ q_{j+1} \forces \name p_0^{j+1}  \stronger\name p^j_0$$

\bigskip\bigskip



To conclude the proof of the Induction Lemma, let $q=\bigcup_j q_j$.
  Then $q\in P_{\delta} \subseteq P_{\beta}$.
   We have to check that this works.   

Let $G_{\beta}$ be any generic filter containing~$q$.   We write
   $p^j_n$ for $\np^j_n[G_{\alpha_j}]$, etc. 

Clearly $\<p^j_0: j < \omega> $ is an increasing sequence of
   conditions.   First we claim that $p^j_0\in D_j\cut N $.  By
    (5), $p^j_0 \in D_j$, and since $q_j$ 
   is generic, $p^j_0  =  \name p^j_0 [G_{\alpha_j}]\in N$.   


   Next we note that for all $k$, $p^k_0\on \alpha_k \in
   G_{\alpha_k}$.    Since $p^j_0 \weaker p^k_0$ for $j
   \le k$, $p^j_0\on \alpha_k \in G_{\alpha_k}$ for all $k\ge j$,
   hence $p^j_0\in G_{{\delta} }$. Since $p^j_0\in N$, $\dom(p^j_0)
  \subseteq {\delta}$.    So $p^j_0 \in G_{\beta}$. This shows
  $G_{\beta} \cut D_j
   \cut  N\not= \emptyset$.   So   $q$ is generic. 




\bigskip

For any $i$, $f^j_i\on j = f_i\on j$ (by the second clause in (1)).
    So $f_i =  \lim\limits_{j<\omega} f^j_i$.  Since for all $j$,
    $f^j_i \re _{n_i}    g$, and $\{f:f \re _{n_i} g\}$ is closed, $f_i
    \re _{n_i} g$.  So $g$    covers~$N[G_{\beta}]$. 

In particular, for $i<k$, $f_i \re _{n_i} g$, thus showing condition
    \preservDef/(d).    

So we also finished the limit case. 



%%% end of pres_theorem

%------------------------------------------------------
%           ****** 7: applications  ********
%------------------------------------------------------		
%%%%  pres_examples.tex (from examples.tex, thesis version) 
\def\Rmea{\re ^{\rm Cohen}}
\def\rmeavec{\hbox{$\rvec^{\rm Cohen}$}}
\def\Rout{\re ^{\rm random}}
\def\routvec{\hbox{$\rvec^{\rm random}$}}
\def\Rbd{\re ^{\rm bound}}
\def\rbdvec{\hbox{$\rvec^{\rm bound}$}}
\def\Cmea{\C^{\rm Cohen}}
\def\Cout{\C^{\rm random}}


\def\smallsection#1\par{\bigskip\goodbreak\bigskip{\bf
                   #1}\nobreak\medskip\nobreak} 
\def\infof #1 #2 #3 {\bigcap_{#1} \bigcup_{#2 \ge #1} #3_{#2}}
\def\infoff #1 #2 #3 {\bigcap_{#1} \bigcup_{#2 \ge #1} #3(#2)}

\neusection
\beginsection \printchapternumber6\quad  Applications

%%%%%%not adding random reals: see Cichon's diagram, ask Tomek.


The general strategy for preserving a property in limit stages of a
countable support iteration is as follows: 
\begindent
\ite 1  Find a stronger property that can be written as $Q \forces
        \forall f\in V[G]\,\exists g\in V$ $f \re g$ for a ${\Sigma}^0_2$
        relation~$\re $.  Let $\re =\bigcup_n \re_n$, where each $\re_n$ is
        closed. 
\ite 2  Prove that all $Q_\alpha$ preserve $\<\re_n:n\in \omega>$. 
\endent
      
Then by the preservation theorem, for all $\alpha$, $P_\alpha \forces
        \forall f\in V[G_\alpha ] \, \exists g\in V\,\, f \re g$, and
        hence $P_\alpha$ has the property we wanted to preserve. 

%%%%%% Jan 28  ---- can this be used? 
%Note that if $S$ is a $\Pi^0_3$-relation, say $f Sg$ iff $\forall i \,
%  \exists j \forall k \,\, \varphi(f\on k,g\on k,i,j,k)$ and $\varphi$
%  is recursive, then 
%    $$ \forall f\in V[G]\, \exists g\in V: fSg$$
%is equivalent to 
%$$ \forall f\in V[G]\, \exists g\in V: f \re g$$
%with $f \re g :\liff \exists j \,\forall k \,\, \varphi(\bar f\on k, g\on
%  k, f(0), j,k)$,  and $\bar f$ is the function defined by $\bar
%  f(n)=f(n+1)$. 


\PROCLAIM\clopen/Fact:  If for all $g$ and all $n$,  the set $\{f: f \re_n
  g\}$ is closed {\bf and open}, then:  
$$ \hbox{$Q$ almost preserves $ \rvec $} \quad \liff \quad
   \hbox{$Q$  preserves $\rvec$} $$
\ENDPROCLAIM

Proof: $\repl$ is clear. 

$\limpl$: Assume that $g$ covers the countable elementary model $N$,
  $\bar p:=\<p_n:n\in \omega>$ is an increasing sequence of conditions
  interpreting $\bnffk = (\nf_0, \ldots, \nf_{k-1} )\in N$ as $\bsffk
  = (f^*_0, \ldots, f^*_{k-1})$, and let $f^*_i \re _{n_i} g$ for all~$i<k$. 

  Fix~$i<k$. Since the set $A_i:= \{f: f \re _{n_i} g\}$ is open, there
  exists  an integer $n^*_i$ such that $[f^*_i\on n^*_i] \subseteq
  A_i$.   

 Let $n^*:= \max\{n^*_i: i<k\}$.  As $Q$ almost preserves $\rvec$, we
  can find a generic condition $q \stronger p_{n^*}$, satisfying
  \preservDef/(a)--(c).   

 For each $i$, we have $q \forces \nf_i\on n^* = f^*_i\on n^*$, thus 
  $$ q \forces \nf_i \in [f^*_i\on n_i ] \subseteq \{f: f \re _{n_i}
  g\}$$ so $q$ also satisfies \preservDef/(d). 




\medskip
In general, ``$Q$ preserves \rvec'' and ``$Q$ almost preserves \rvec''
are not equivalent, as can be seen from the following example: 


\PROCLAIM\counterex/Example:  Let $\rvec = \<\re_n:n\in \omega>$ be
defined by $f \re_n g \liff \forall k\ge n: f(k)<g(k)$, assume that $Q$
is \oob/ (and thus preserves \rvec, see \boundlemma/, below). 

Let $\re '_n = \re_n $ for $n>0$, and let $f \re '_0 g $ iff for all $k$,
$f(k)=0$, and $\re '=\bigcup_n \re '_n$.      Then for any  $f,g$:  $f \re 
g $ iff $f \re ' g$, hence for any model  $N$: 
$$ \hbox{$g$ \rvec-covers $N$ \ iff \ $g$ $ \rvec '$-covers $N$}$$
and thus:  $Q$ almost preserves $\rvec$ iff $Q$ almost preserves
$\rvec'$. 

Claim:  If $Q$ adds reals, then $Q$ does not preserve~$\rvec'$.  (But
if $Q$ is \oob/, then $Q$ almost preserves~$\rvec'$.)
\ENDPROCLAIM

Proof: Let $\nx$ be a name such that $\forces_Q \nx\in \fct \logand
    \nx\notin V$.  Let $\bar p:=\<p_n:n\in \omega>$ be an increasing
    sequence of conditions interpreting~$\nx$.  Then
    $$ \forces_Q \exists n : p_n\notin G$$
Define a name $\nf\in \zerooneseq$ by requiring
    $\forces_Q$``$\nf(n)=0\liff p_n\in G_Q$.''  Let $f^*$ be the
    function with $\forall n f^*(n)=0$.

Then: $f^* \re '_0 g$, and $\<p_n:n\in \omega>$ interprets $\nf$ as $f^*$, but
$\forces_Q \exists n \nf(n)\not=0$, thus $\forces_Q \lnot(\nf \re '_0
g)$.  

Hence there is no condition satisfying \preservDef/(d). 



\smallsection Application 1:  Preservation of \oob/

\PROCLAIM\ooDef/Definition:  
   A forcing notion $Q$ is called $\fct$-bounding iff 
     $$ \forcess_Q \forall f\in \fct\cut V[G] \, \exists g\in
   \fct\cut V\,\, \forall n \,\, f(n)<g(n)$$
\ENDPROCLAIM


There is a natural way to translate this property into the framework
   of the ``preservation theorem'' in \preservDef/: 

\PROCLAIM\ooR/Definition:  
We let (for $f, g\in \fct$) $$f \Rbd_n g  \ \liff\  \forall k\ge n\,
   f(k)<g(k)$$
\ENDPROCLAIM


This is a closed relation.  Letting $\Rbd = \bigcup_n \Rbd_n$, clearly $Q$ is
   $\fct$-bounding iff 
     $$ \forcess_Q \forall f\in \fct\cut V[G] \, \exists g\in
   \fct\cut V\,\, f\Rbd g$$



\PROCLAIM\boundlemma/Lemma: A proper forcing 
   notion $Q$ preserves $\rbdvec$  iff it is $\fct$-bounding. 
\ENDPROCLAIM

Proof: Assume $Q$ preserves~$\rbdvec$.  Then for any name $\nf$ and any
   condition $p$, let $N$ be a model containing $\nf$ and~$p$. Let $g$
   cover~$N$.  We can find a condition $q \stronger p$ forcing that
   $\nf \Rbd  g$.  Now $g$ is in the ground model, so $Q$ is
   $\fct$-bounding.

Conversely, assume that $Q$ is $\fct$-bounding, and consider a model
   $N$ and a 
   sequence $\sqn p $ as in the hypothesis of \preservDef/.  We also have 
   names  $\nf_0, \ldots, \nf_{k-1}$,  and  functions  $f_i^*$ such
   that $p_n \forces \nf_i\on n = f_i^* \on n$ for all~$i<k$. 


First we note that any $N$-generic $q$ will force 
   $$ \forall f \in N[G] \, \exists f'\in N \, \forall n \,\,
       f(n) < f'(n)$$
Since any such $f'$ is eventually bounded by $g$, $q \forces \forall
   f\in N[G] \,\, f \Rbd  g$. 

We still have to deal with our fixed names~$\nf_i$.   Assume
   $f_i^*\Rbd _{n_i}  g$. For each $n$ we can find a condition $p'_n
  \stronger p_n $ and
    functions
   $f_{i,n}'\in N$ ($i<k$) such that $p_n' \forces \forall k \,\,
   \nf_i(k)<  f'_{i,n}(k)$.   Let for all $i<k$ 
   $f'_i $ be defined by 
      $$ f'_i(k) = \max\{f'_{i,n}(k) : n \le k \} +1$$ 
   We can find these sequences $\<p_n':n<\omega>$ and $\<f'_{i,n}:i<k,
   n<\omega>$ in $N$, so there are $n_i'$ such that  $f'_i \Rbd _{n'_i}
   g$, $n'_i \ge n_i$.  Let $n^*\ge n'_i$ for all 
   $i$, and let  $q \ge p_{n^*}'$ be a generic condition.  Then  
   $$ \eqalign{ q \forces & \forall k \ge n^* \,\, \nf_i(k) < f'_{i,n^*}(k)<
   f'_i(k) <   g(k)\cr 
    q \forces& \forall k \in (n_i, n^*)\,\, \nf_i(k) = f_i^*(k)<
					   g(k)\cr}$$
   so $q \forces \nf_i \Rbd _{n_i} g$.  

\PROCLAIM\boundCor/Corollary: The  countable support iteration  of proper
  \oob/ forcing notions is (proper and) \oob/. 
\ENDPROCLAIM


\smallsection {Application 2:  Preserving outer measure one}

Let $\Omega$ be the set of clopen subsets of~$\zerooneseq$.  $\Omega$
  is a countable set.  We will consider functions $f\in
  \pre{\omega}{\Omega}$ and functions $g\in \zerooneseq$. 

$\mu(A)$ is the Lebesgue measure of any measurable set $A \subseteq
  \zerooneseq $, and we let $\mu^*(A)$ be the outer Lebesgue measure
  of any set $A \subseteq \zerooneseq$.

We let $$\Cout:=
 \{f\in\pre{\omega}{\Omega}: \,
           \forall n  \in \omega\, \mu(f(n)) \le 2^{-n}\}$$

This is a closed set (in the product topology of
  $\pre{\omega}{\Omega}$, where $\Omega$ is equipped with the discrete
  topology). 

For $f\in \Cout$, we let $$A_f:= \bigcap_{n\in    \omega}\bigcup_{k\ge n}
f(k) $$



\PROCLAIM\nullSet/Fact:  
\begindent
\ite 1 If $f\in\Cout$, then $A_f \subseteq \zerooneseq$ is a set of
   measure zero.  
\ite 2 If $H\subseteq \zerooneseq$ has measure zero, then there is
   $f\in \Cout$ such that $H\subseteq  A_f$. 
\endent
\ENDPROCLAIM

Proof: (1) follows from $\displaystyle\mu\big(
  \bigcup_{k\ge n} f(k)\big) \le 2^{-n}+ 2^{-n-1} + \cdots =
  2^{-n+1}$.  

(2): Let $\Gamma: \omega\times \omega \to \omega$ be a monotone
   bijection.   For each $m$, $H$ can be covered by an open set of
   measure $<2^{-{\Gamma} (m,0)}$, say
   $$ H \subseteq \bigcup_{k\in \omega} [s^m_k]\qquad s^m_k\in
   \finzerooneseq\qquad
    \mu\big(\bigcup_{k\in \omega} [s^m_k]\big)\le 2^{-{\Gamma}(m,0)}$$


For each $m$, we can find a sequence $0=k^m_0 <k^m_1 < \cdots\,$ of
integers satisfying 
  $$ \mu\big(\bigcup_{k\ge k^m_j} s^m_k\big) < 2^{-\Gamma(m,j)}$$  
for all $j\in \omega$. 

Define $f$ by 
   $$ f({\Gamma}(m,j)) =\bigcup \{[s^m_k]: k^m_j\le k  k^m_{j+1}\}$$
This is a finite union of basic clopen sets, hence clopen.  Also,
$$\mu(f({\Gamma}(m,j)))\le \mu\big(\bigcup_{k\ge k^m_j}
s^m_k\big) \le  2^{-{\Gamma}(m,j)}$$   so~$f\in\Cout$.  


 Note that for all $m$,   $\bigcup_{j\in \omega} f({\Gamma} (m,j)) =
   \bigcup \{[s^m_k]: k\in \omega\} \supseteq H$.    For all $n\in
   \omega $  there is $m\in 
   \omega$ such that $\forall j:{\Gamma}(m,j)>n$, so 
   $$ \forall n\, \exists m \,\, H \subseteq \bigcup_{j\in \omega}
   f({\Gamma}(m,j))  \subseteq \bigcup_{k\ge m} f(k)$$
so $H \subseteq        \displaystyle\bigcap_{m\in
   \omega}\bigcup_{k\ge m} f(k) $. 



\PROCLAIM\outRdef/Definition:  
For $f\in\Cout$, $g\in \zerooneseq $, $n\in \omega$ we let $f \Rout _n g$ iff
   $\forall k\ge n \,\,g \notin f(k)$. 
\ENDPROCLAIM

   This is a closed relation
   since (for fixed $k$), ``$g\in f(k)$'' is clopen. 


\PROCLAIM\frggaf/Fact:  $f \Rout  g  $ iff $g\notin A_f$. 
\ENDPROCLAIM


\PROCLAIM\outerFact/Fact:  For a countable model $N$ of $ZFC$: 
$$
    \hbox{$g$ \routvec-covers $N$} \quad \liff \quad 
           \hbox{$g$ is random over  $N$}$$ 
\ENDPROCLAIM

 Proof: Assume that $g$ is random over~$N$.  Fix a function $f\in \Cout$.  Then
   as  $g$ is not an element of the null set $  A_f $,  we have $f\Rout g$. 

Conversely, assume that $\forall f\in N\,\, f \Rout  g$.  Then for any
   measure zero set $H$  in  $N$ we can find a sequence $f\in\Cout$ such that
   $H \subseteq A_f $.  Since  $f\Rout g$, $g\notin A_f$, so $g\notin H$. 


\PROCLAIM\applynull/Fact:  If $Q$ preserves \routvec, then $\forces _Q
\mu^*(V\cut \zerooneseq) = 1 $.  
\ENDPROCLAIM


Proof:  Assume $p \forces \mu(V \cut \zerooneseq)=0$.   Then there
is a name $\nf$ such that $p \forces \nf\in \Cout\logand V \cut \zerooneseq
\subseteq A_{\name f}$.  Take any countable elementary model $N$
containing $p$ and $\nf$, and let $g$ cover~$N$.  Then $p \forces g
\in A_{\name f}$,     but there is a condition $q \stronger p$, $q
\forces {}$``$g$ covers     $N[G]$,'' so $q \forces g\notin A_{\name
f}$, a contradiction.




This fact justifies the following definition: 


\PROCLAIM\randDef/Definition:  We say that a forcing notion $Q$
   ``preserves outer measure one'' iff $Q$ preserves~$\routvec$. 
\ENDPROCLAIM


\medbreak\medskip

In [\KunenMiller], the following property of forcing notions was
  considered: 


\PROCLAIM\starfour/Definition:  A forcing notion $Q$ satisfies $*_4$ if
  for every countable $N\prec H(\chi)$, if $P\in N$, $\<p_n:n\in
  \omega>\in N$, each $p_n$ in $P$, and $\<\name A_n:n\in \omega>\in
  N$, each $\name A_n$ a $P$-name, for every $n$, 
  $p_n \forces$``$\name A_n$ is a Borel set and $\mu(\name
  A_n)<\varepsilon_n$'' and $\lim_{n\to \infty} \varepsilon_n = 0$ and
  $g\in \zerooneseq$ is random over $N$ then there exists $q\in P$
  such that 
\begindent
\ite i $q$ is $(N,P)$-generic.
\ite ii $q \forces $``$g$ is random over~$N[G_Q]$.''
\ite iii there exists $n$ such that $q \stronger p_n $ and $q
  \forces$``$x\notin \name A_n$.'' 
\endent
\ENDPROCLAIM
[\KunenMiller] also showed that Laver forcing has the property~$*_4$.       


\PROCLAIM\outerClaim/Lemma:  If $Q$ satisfies $*_4$, then $Q$
   ``preserves outer measure one.''  
\ENDPROCLAIM

Proof:  Let $\<p_n:n\in \omega>$, $\bnffk=\nff {} k-1 $ be as in
  \preservDef/, let $N$ be a countable elementary model, and let $g$
  cover~$N$.  Then $g$ is random over~$N$.   

Define $Q$-names $\name A_n$ such that 
$$ \forces \name A_n  = \bigcup_{i<k} \bigcup_{m \ge n} \nf_i(m)$$
Then $\forces \mu(A_n) \le \varepsilon_n$, where $\varepsilon_n:=
  k \cdot 2^{-n+1}$. 

Let $\<p_n:n\in \omega>$ interpret $\bnffk$ as $\bsffk$, and assume
  $f_i^* \Rout _{n_i} g$. Let $n^*:= \max\{n_i:i<k\}$.   Applying $*_4$ to
  the sequence $\<p_n: n^*\le n < \omega>$, we can find an $n^{**} \ge n^*$
  and a generic condition $q \stronger p_{n^{**}}$ such that $q \forces
  $``$g$ is random over $N[G]$,'' and $q \forces g \notin A_{n^{**}}$.
  
As $g$ is random over $N[G]$ iff $g$ covers $N[G]$, $q$ satisfies
  \preservDef/(a)--(c).   

For each $i<k$ we have  $q \forces g \notin \bigcup_{m \ge n^{**}}
  \nf_i(m)$.
   So to get \preservDef/(d), it suffices to show 
    $$ q \forces g \notin \bigcup_{n_i\le m < n^{**}}\nf_i(m)$$
This follows easily from $q \stronger p_{n^{**}}$, as $$p_{n^{**}} \forces
  g\notin  \bigcup_{n_i\le m < n^{**}} f^*_i(m) = 
  \bigcup_{n_i\le m < n^{**}} \nf_i(m) $$

\bigskip


Thus (by [\KunenMiller]) the Laver forcing ``preserves outer measure one.''  


\PROCLAIM\randomrandom/Lemma:  The random real forcing notion ``preserves
outer measure one.'' 
\ENDPROCLAIM

To prove this lemma, we first show the following claim: 
\PROCLAIM\helprandom/Claim: 
Let $Q$ be the random real forcing, and let $\name A$ be a $Q$-name
   for a subset of $\R$, 
   $p\in Q$, and assume that for some real $c$, $p \forces \mu^*(\name
   A) < c$.   Then, letting 
       $$ A(p):= \{x\in \R: p \forces x\in \name A\},$$
   we have $\mu^*(A(p))\le c$. 
\ENDPROCLAIM

Proof of the claim:  Let $\name B $ be the name of a Borel set such
   that $p \forces{} $``$\name A \subseteq \name B \logand \mu(\name B) <
   c$.    


Notation: For any  set $C \subseteq \R^2$, $t\in \R$, we  let 
$$ \eqalign{C^t:=& \{x\in \R: (x,t)\in C\}\cr
            C_t:=& \{y\in\R: (t,y) \in C\}\cr}$$


There is a Borel set $C \subseteq \R^2$ such that 
    $p \forces \name B = C_r$, where $r$ is the canonical name of the
   random real.   Wlog $C \subseteq p \times \R$.  In $V$ we have for
   almost all $x$ $\mu(C_x) \le c$, so $\mu(C)\le c\cdot \mu(p)$. 

Let $D:= \{y: C^y =^* p\} = \{y: p \subseteq^* C^y\}$.    (We write
  $X \subseteq^* Y$ iff $\mu(X-Y) = 0$.)   

We claim~$D=B(p)$.  Proof: 
We have $y\in B(p) \liff p \forces y\in B \liff p \forces y \in C_r
   \liff p \forces 
   (r,y)\in C \liff p \forces r\in C^y \liff \mu(p-C^y)=0$.   

Clearly $\mu(C) \ge \mu(D)\cdot \mu(p)$, so $\mu(D) \le 
   {\displaystyle\mu(C)\over \displaystyle\mu(p)} \le c$. 

This ends the proof of \helprandom/. 



{\bf Proof of \randomrandom/:}

  We first show that  $Q$ almost 
preserves 
   $\routvec$ and in fact any condition in $N$ is generic and forces
   ``$g$ is random over $N[G]$,''  if $g$ is random over~$N$. 


Every condition is generic, because $Q$ satisfies ccc.   Now assume
   that $\ \notforces $   ``$g$ is random over~$N[G]$.''   Then  for
   some condition $q$, and some $\name B\in N$, $\forces_Q$``$\mu(\name
   B)=0$'' and $q \forces_Q  $``$g\in \name B$.''  Let $C\in N$ such
   that $\forces$``$\name B = C_r$.'' So $q \forces r\in C^g$, which
   is impossible, since $C$ is a set in $N$ of measure zero, so $C^g$
   has measure zero.   This shows that random real forcing almost
  preserves    $\routvec, \Cout$. 

Assume $f_i^* \Rout _{n_i} g$, $p_n \forces \nf_i\on n = f_i^*\on n $.  

In $N$ we can define a sequence $\sqn B $ as follows: 
 $$ B_n:=\big\{x\in \R : p_n \forces x \in
   \bigcup_{i<k}\big(\bigcup_{m\ge n}\nf_i(m) \big)\big\}$$
By \helprandom/, $$\mu^*(B_n)\le k\cdot \sum_{m\ge n} 2^{-m}\le
   {2k\over 2^n}$$
Since $\<B_n:n\in \omega>\in N$, and $g$ is random over $N$, $g\notin
  \bigcap_n B_n$. So  there
   exists a $n^*\ge \max(n_0, \ldots, n_{k-1})$ such that $g\notin 
   B_n$.  There exists a condition $q \stronger p_{n^*}$, 
  $$ q \forces \forall i<k : g\notin \bigcup_{m\ge {n^*}}\nf_i(m)$$
Since for all $i<k$, $$q \forces  g \notin \bigcup_{n_i<m<{n^*}}
   f^*_i(m) = \bigcup_{n_i<m<{n^*}} \nf_i(m)$$
we have $q \forces \forall i<k \, \nf_i \Rout _{n_i} g$. 

\medskip

A similar proof shows that random real forcing satisfies $*_4$,
    proving a  conjecture of Miller. 



\smallsection Application 3:  Preserving nonmeager sets

We consider functions $f$ from $\finSeq$ to $\finSeq$, and functions
   $g$ from $\omega $ to $\omega $. 


\PROCLAIM\ismeager/Fact: 
\begindent
\ite 1       
For any $f:\finSeq \to \finSeq$, the set 
    $$ A_f := \{g: \forall n \, g\on n \extend f(g\on n) \not
   \subseteq g\}$$
is closed nowhere dense. 
\ite 2 Conversely, for  every closed nowhere dense set $H$ there is a
   function $f$ such that $H \subseteq A_f$. 
\endent
\ENDPROCLAIM

Proof: For every $n$, the set $ \{g: g\on n \extend f(g\on n)
   \subseteq g\}= \bigcup_{\eta\in \pre n \omega} [\eta\extend
   f(\eta)]$ is clopen, so $A_f$ is closed. $A_f$ cannot contain any
   basic interval 
   $[\eta]$, since $A_f$ is disjoint from $[\eta\extend f(\eta)]$. 

Conversely, let $H$ be a closed nowhere dense set in~$\fct$. Then as
   $H$ is closed, 
   there is a    tree $T \subseteq \finSeq$ such that $H = \{f\in
   \fct: \forall n \, f\on n \in T\}$.  As $H$ is nowhere dense, for
   every $\eta\in \finSeq$ there is an extension $\eta\extend f(\eta)$
   such that $H \cut [\eta\extend f(\eta)] = \emptyset$. 



\PROCLAIM\meagerRdef/Definition:    We let $\Cmea$ be the set of all
functions from $\finSeq$ to~$\finSeq$. 

We define \rmeavec{} by $f \Rmea _k g$ iff 
\begindent
\item {} $f:\finSeq \to \finSeq$.
\item {} $g: \omega \to \omega$. 
\item {} $\exists n\le k: g\on n \extend f(g\on n) \subseteq g$. 
\endent
\ENDPROCLAIM

\PROCLAIM\xy/Fact:  $f\Rmea g$ iff $g\notin A_f$. 
\ENDPROCLAIM

\PROCLAIM\meagerfact/Fact: $g$ \rmeavec-covers $N$ iff $g$ is Cohen over~$N$. 
\ENDPROCLAIM

Proof:  Recall that $g\in \zerooneseq$ is Cohen over a model, iff it
not contained in any meager set coded in the model, iff it is not
contained in any closed nowhere dense set coded in the model. 

 Assume that $g$ is  Cohen over~$N$.  Fix a function $f\in \Cmea$.
Then as $g$ is Cohen,   $g$ is not an element of the meager set
   $A_f$,    so there is     an $n$ such that $f \Rmea _n g$. 

Conversely, assume that $\forall f\in N\,\, f \Rmea  g$.  Then for any
   closed nowhere dense  set $H$  in  $N$ we can find a sequence
$f\in\Cmea$ such that 
   $H \subseteq A_f $.  Since there is some $n$ such that $f
   \Rmea _n g$, $g\notin H$. 






\PROCLAIM\applymeager/Fact: If $Q$ preserves \rmeavec, then $Q \forces$``$
V\cut \fct$ is    not meager''.
\ENDPROCLAIM

Proof:  Assume $p \forces V \cut \zerooneseq$ is meager.  Then there
is a name $\nf$ such that $p \forces V \cut \zerooneseq \subseteq
A_{\name f}$.  Take any countable elementary model $N$ containing $p$
and $\nf$, and let $g$ cover~$N$.  Then $p \forces g \in A_f$, a
contradiction. 

In [\ProperImproper, ch.18], a converse to this theorem is proved: 

\PROCLAIM\whenpreserveCohen/Theorem: Assume that $(Q, \le)$ is a Souslin
proper forcing notion (see section 7), and 
$$ (*) \qquad  \qquad  \forces_Q V\cut \fct \hbox{ is not meager
}$$
and moreover, $Q$ has property $(*)$ in any extension of $V$ (by set
forcing).   Then  $Q$ preserves \rmeavec. 
\ENDPROCLAIM

\medskip
\PROCLAIM\meagerEx/Example: Cohen forcing preserves \rmeavec. 
\ENDPROCLAIM

Proof: Note that each relation $\Rmea _n$ is clopen.  By \clopen/, it is
enough to show that Cohen forcing almost preserves \rmeavec. 

We claim that if $g$ covers $N$, then {\bf any} condition forces ``$g$
covers~$N[G]$.''  The proof is exactly the same as the proof in the
previous section, with ``measure zero'' replaced by ``meager'',
``random'' replaced by ``Cohen'', etc. 




\bigskip





\smallsection Application 4: The Laver property



From now on until the end of this section, $n$ will be a variable
  ranging over {\bf positive} natural numbers. 




\PROCLAIM\coneDef/Definition:  
For a function $h:\omega \to \omega$, an ``$h$-cone''
 is a sequence $\<A_m:m\in \omega>$ of finite subsets of
   $\omega$ with $|A_n| \le h(n)$ for all~$n>0$. 
\ENDPROCLAIM


If $h,H:\omega\to \omega$, $\bar A $ an $h$-cone, we say that $\bar A$
   is bounded by $H$ if for all $n>0$, $A_n \subseteq H(n)$. 

$\Q_+$ is the set of nonnegative rationals.  For $r\in \Q_+$, an $r$-cone
is an $h$-cone where $h(m) = \lfloor 2^{mr}\rfloor$.   ($\lfloor
  x\rfloor$ is the greatest integer~$\le x$.) 


A ``cone'' is a sequence $\<A_m:m\in \omega>$ of finite subsets of
   $\omega$ with $|A_n| \le 2^n$ (i.e., a $1$-cone). 

We say that $\bar A = \<A_m:m\in
   \omega>$    ``covers'' $f\in \fct$ if for all $n>0$ $f(n)\in A_n$. 

If $f\in \pre{\omega}{\left(\finSet\right)}$, we say that $\bar A$
covers $f$ iff for all $n>0$ $f(n) \subseteq A_n$. 


\def\ph{{\textstyle \prod H}}

For a function $H\in \fct$, we write $\ph$ for the set $\{f\in \fct:
  \forall n>0\,\, f(n) < H(n)\}$.  This is a closed subset of~$\fct$. 

 \PROCLAIM\LaverProp/Definition:   A forcing notion $Q$ is said to have 
   the {\it Laver Property\/} iff for every $H:\omega \to \omega$ in
   $V$, $$ \forces_Q \hbox{``$\forall f\in \ph\cut V[G]: \exists 
   \bar A\in V$, $\bar A$ is a cone covering $f$}\leqno \hbox{\qquad
  (Laver)}_H$$ 
\ENDPROCLAIM
   

Note that if $\forall n>0 \, H(n)\le H'(n)$, then $\prod H \subseteq
  \prod H'$, so $\hbox{(Laver)}_{H'}$ implies~$\hbox{(Laver)}_H$.  So
  without loss of generality we may restrict ourselves to some
  dominating family of functions $H$, e.g. all increasing functions in
    $\pre{\omega}{(\omega - \{0\})}$. 


\PROCLAIM\LaverEq/Fact:  The following are equivalent for
   any two    universes $V_0 \subseteq V_1$: 

\begindent
\ite 1 For all $H \in \fct\cut V_0$: If $f\in \fct\cut V_1$ is bounded by $H$,
   then $f$ is covered by some cone of~$V_0$. 
\ite 2 For all $H \in \fct\cut V_0$, for all functions $ h_0\in \fct
   \cut V_0$ that diverge to infinity:  
\itemitem {}  If $f\in \fct\cut V_1$ is bounded by $H$, then $f$ is covered by
   some $h_0$-cone of~$V_0$. 
\ite  3  For all $H \in \fct\cut V_0$: For all $ h_0, h_1\in \fct\cut
   V_0$: If for all $n$, $h_0(n)\le h_1(n)$, and $h_0(n)=o(h_1(n))$,
   i.e., $\displaystyle 
   \lim\limits_{n\to \infty} {h_1(n)\over 
   h_0(n)} = \infty$, then for all $h_0$-cones $ f\in V_1$: 
\itemitem {}  If \ $f$ is bounded by $H$,  
 then $f$ is covered by some $h_1$-cone $F\in V_0$. 
\endent
\ENDPROCLAIM




We will give the proof of this fact (a routine computation) below.



\PROCLAIM\LaverEqDef/Definition:  
If any/all of  these conditions are satisfied, we say that $V_1$ has the
   Laver property over~$V_0$.
\ENDPROCLAIM


Note that by (1),  a forcing notion $Q$ has
   the Laver property iff 
     $$ Q \forces \hbox{$V[G]$ has the Laver property over $V$}$$





\def\LaverH,#1,#2 {\hbox{(Laver)}_{H,{#1},{#2}}}


\PROCLAIM\hNotation/Notation:    Fix some (recursive) map $c$ from
   $\finSet$ onto  the set of rational numbers in [0,1). 
    If $c(x)=r$  we say  ``$x$ codes~$r$.''
\ENDPROCLAIM



\PROCLAIM\ChDef/Definition:  Let $$\C^H := \{f%\}
\in \fctfin: \hbox{If $f(0)$
   codes $r_0$, then \vtop{\hbox{\strut$\forall n >0: f(n) \subseteq
  H(n)$}\hbox{\strut  and   $|f(n)|\le 2^{n r_0}%\{
\}$}}}$$ 
\ENDPROCLAIM


\PROCLAIM\RhDef/Definition:  Let $\rvec^H = \<\re ^H_k:k< \omega>$  be defined by
   $f \re ^H_k g$ iff  
\begindent
\item {} $g$ is a cone bounded by~$H$.
\item {} $f(0)$ codes some~$r_0$. 
\item {} $f\in \C^H$  (so $\forall n>0\,\, |f(n)| \le 2^{nr_0}$)
\item{} $\forall n> k\,\, f(n) \subseteq g(n)$. 
\endent
We let $\re ^H  = \bigcup_k \re ^H_k$. 
\ENDPROCLAIM


Clearly  the set $\{f: f \re ^H_k g\}$ is closed for all $g$, and for any
   countable set $a$ there is
   $g$ such that $\forall f\in a\cut \C^H\,\, f \re ^H g$. 



\PROCLAIM\hrsdef/Definition:   Let $Q$ be a forcing notion.  If $H\in
\fct$, $0\le r < s$, we write $\LaverH,r,s $ for the statement: 
$$  \forcess_Q \vtop{
  \hbox{\strut``Every $r$-cone $f$ in $V[G] 
$ that is bounded by $H$}\hbox{\qquad\qquad\strut is
   covered by some $s$-cone $F\in V$''}}\leqno\LaverH,r,s  $$
\ENDPROCLAIM

Thus, (Laver)$_{H}$ from \LaverProp/ is equivalent to $\LaverH,0,1 $. 



\smallbreak


\PROCLAIM\SLlemma/Lemma:  Assume $Q$ is a proper forcing notion.  Then 
the following are equiavlent: 
\begindent
\ite 1  $Q$ satisfies the Laver property.
\ite 2 For all $H\in \fct$, all $0\le r<s$, $Q$ satisfies
       $\LaverH,r,s $. 
\ite 3 For all $H\in \fct$, all $0\le r<1$, $Q$ satisfies
       $\LaverH,r,1 $. 
\ite 4 For all $H\in \fct$,  $Q$ satisfies $\LaverH,0,1 $. 
\ite 5 For all $H$, $Q$ preserves~$\rvec^H$. 
\ite 6 For all $H$, $Q$  almost preserves~$\rvec^H$. 
\endent
\ENDPROCLAIM
      
Proof:  We will show \vtop{\ialign{&\hfil$# $\hfil\cr
(1) & \limpl & (2) & \limpl  & (3) & \limpl & (4) & \limpl & (1).\cr
    &        & \Downarrow&&\Uparrow\cr
    &        & (5) & \limpl & (6)  \cr}}
\medskip
(1) $\limpl $ (2) follows from the characterisation \LaverEq/(3),
       using the functions $h_0(n) = 2^{r n}$, $h_1(n) = 2^{s n}$. 

(2)  $ \limpl $  (3)  $ \limpl $  (4)  $ \limpl $  (1) is clear, and
       also (5)  $ \limpl $  (6) is clear. 

(6)  $ \limpl $  (3) follows from \preserveCover/.  (Note that in (3)
       we can restrict ourselves to {\bf rational} numbers~$r$.)


So it remains to show (2) $\limpl  $ (5). 





Assume that $Q$ satisfies $\LaverH,r,s $ for all $0\le r < s$.   Let
$N$ be a countable elementary 
   model, $H\in N$, and assume that $g$ covers~$N$. 

Claim:  If $G$ is generic over $V$, and $G\cut N$ is generic over
   $N$, then $g$ covers~$N[G]$. 

\begingroup\advance\leftskip by 0.5cm
Proof of the claim: Let $f\in \C^H\cut N[G]$, and let $f(0)$ code~$r_0$.
Let $t_0 := (r_0 + 1 ) / 2$.  

So $\forall n>0$ $f(n) \subseteq H(n)$ and $|f(n)| \le 2^{n r_0}$.
  By $\LaverH,r_0,t_0 $, there is $F\in V$,
       $\forall n>0$ 
   $|F(n) | \le 2^{n t_0}$ and $f(n) \subseteq F(n) \subseteq H(n)$.
  Since $G\cut N$ is generic over $N$, we can   find this $F$ in~$N$. 
    We may assume that $F(0)$ codes~$t_0$. (So $f\in \C^H\cut N$.)

   Since $g$ covers $N$, there is a $k$ such that $F \re ^H_k g_s$.  So for
   all $n\ge k$, $f(n) \subseteq F(n) \subseteq g_s(n)$.  This ends
   the proof of the claim. 

\endgroup
  So every generic condition will force \preservDef/(a)--(c). 

We still have to deal with condition (d) of \preservDef/.  So assume that 
   $\sqn p $ 
   interprets $\nffk $ as $\ffk$, and assume $ \forall i<k\,\, f_i^*
   \re _{n_i} g$. Let $f^*_i(0) $ code $r_i$, and let $s_i$, $t_i$
   be rationals such that $r_i<s_i < t_i < 1$.  


By $\LaverH,r_i,s_i $,  for  all $n>0$ we can find a condition $p'_n \ge
  p_n$ such 
   that for all 
   $i<k$ there exists a function $F_{n,i}$ with $F_{n,i}(m)
   \subseteq H(m)$ and $|F_{n,i}(m)| \le 2^{ms_i}$ for all $m$, and 
   $$ p'_n \forces \forall m>0 \,\,\nf_i(m) \subseteq F_{n,i}(m)$$
 We can find these sequences  $\<p_n':n<\omega> $ and
   $\<F_{n,i}:n<\omega,i<k>$     in~$N$.  

   Now define for $i<k$ $F_i$ as follows:  $F_i(0)$ codes $t_i $, and
       for $n>0$ let  
      $$ F_i(n) = \bigcup\{ F_{m,i}(n): {m\le 2^{n(t_i - s_i)}}\}  $$ 
   Then $F_i(n) \subseteq H(n)$, and $|F_i(n)| \le 2^{nt_i}$. 
   
   Furthermore,  we have $F_{m,i}(n) \subseteq F_i(n)$, if
   $m\le 2^{n(t_i-s_i)}$.  

Let $m_0$ be so large that 
\begindent
\ite i For all $n \ge m_0$, all $i<k$,
   $2^{n(t_i-s_i)} >n$.   
\ite ii  For all $i<k$, $F_i \re ^H_{m_0} g$. 
\ite iii For all $i<k$, $m_0>m _i$ (so  $f^*_i \re ^H_{m_0} g$.) 
\endent
      
We now claim that for any generic $q \ge p'_{m_0} $, 
   $$ q \forces \forall i<k \,\, \nf_i \re _{n_i} g$$


Proof:   Let $G$ be a generic filter containing $q$,
   fix some $i<k$, and let  $f_i=  \nf_i[G]$. 

   For $n \in [n_i, m_0) $ we have $f_i(n) = f^*_i(n)$ because $q
   \stronger p_{m_0}$, and $f^*_i(n) \subseteq  g(n)$ because
   $f^*_i \re ^H_{n_i} g$. 

   For $n\ge m_0$, we have
   \begindent 
      \item {}  $f_i(n) \subseteq F_{m_0, i}(n)$ because   $p_{m_0}
          \in G$,
      \item {}  $  F_{m_0, i}(n) \subseteq F_i(n)$ because $m_0 \le n
          \le    2^{n(t_i - s_i)}$, and  
      \item {} $ F_i(n) \subseteq g_{s_i}(n) $ because
          $F_i \re ^H_{m_0} g$. 
   \endent
  Hence for all $n\ge n_i$, $f_i(n) \subseteq g_{s_i}(n)$, so $f_i
   \re _{n_i} g$. 
     

\PROCLAIM\Hcor/Corollary:  The Laver property is
   preserved under countable support iteration of proper forcing
   notions. 
\ENDPROCLAIM


{\bf Proof of \LaverEq/:}


Clearly (3) $\limpl$ (2)
   $\limpl$  (1). 

To show that (1) $\limpl $ (3), fix $h_0$, $h_1$ in $V_0$ and $f$ in
   $\prod\limits_n [\omega]^{\lless h_0(n)}\cut V_1$.   We can find a
   function $\ell\in \fct \cut V_0$ such that for all $n$ 
   $\ell(\lfloor\log
   {h_1(n)\over h_0(n)}\rfloor)> n$. ($\log$ is the logarithm to 
   base~$2$.) 
 
   Let $i$ be a bijection between $HF$ (the hereditarily finite sets)
  and~$\omega$. 

    Let $H'(k) =1+
   \max\{i(\eta)(k): |\eta|\le \ell(k), \forall n \, \eta(n)<H(n)\}$
   and define $f'\in \fct$ by $f'(k)=i(f\on \ell(k))$. 
   Then $H'\in V_0$, and~$f'(k)<H'(k)$.  Using (1) on $f'$, we can get
   $F'\in V_0$, such that 
   $\forall k \, f'(k)\in F'(k)\logand |F'(k)| \le 2^k$.
   Clearly we  may assume $i(\eta)\in F'(k) \limpl  \forall n\in \dom(\eta)\,
   |\eta(n)| \le h_0(n)$. 

   Let $\displaystyle F(n) = \bigcup\{\eta(n): {i(\eta)\in
   F'(\big\lfloor\log(h_1(n)/h_0(n))\big\rfloor)} \}$.  So $|F(n)| \le
  h_0(n)\times {h_1(n)\over h_0(n)} \le    h_1(n)$.  

   Now we claim that for all $n$, $f(n) \subseteq F(n)$. 

   Proof:  Fix
   $n$, and let $\displaystyle k= \Big\lfloor\log{h_1(n)\over
               h_0(n)}\Big\rfloor$,~$\eta=f\on\ell(k)$.  Then
$\ell(k)>n$, so  $n\in \dom(\eta)$.  

  Since $i(\eta)= f'(k)\in F'(k)$, $f(n)=\eta(n) \subseteq F(n)$. 
\bigskip


\smallsection Application 5: The Sacks Property


\PROCLAIM\SacksDef/Definition:   A forcing notion $Q$ is said to have 
   the {\it Sacks Property\/} iff 
     $$ \forces_Q \hbox{``$\forall f\in \fct\cut  V[G]: \exists 
   \bar A\in V$, $\bar A$ is a cone covering $f$}$$
\ENDPROCLAIM



\PROCLAIM\SacksEq/Fact and Definition:  The following are equivalent for
   any two    universes $V_0 \subseteq V_1$: 

\begindent
\ite 1 Every $f\in V_1$  is  covered by some cone of~$V_0$. 
\ite 2  For all functions $ h_0\in \fct    \cut V_0$ that diverge to
   infinity:   
\itemitem {}  Every $f\in V_1$ is covered by some $h_0$-cone of~$V_0$. 
\ite  3  For all $ h_0, h_1\in \fct\cut
   V_0$: If for all $n$, $h_0(n)\le h_1(n)$, and $h_0(n)=o(h_1(n))$,
 then for all $h_0$-cones $ f\in V_1$ there is an $h_1$-cone $F\in
   V_0$ covering~$f$. 
\endent
\ENDPROCLAIM




 If any/all these conditions are satisfied, we say that $V_1$ has the
   Sacks property over~$V_0$.   We say that a forcing notion $Q$ has
   the Sacks property iff 
     $$ Q \forces \hbox{$V[G]$ has the Sacks property over $V$}$$



    Define $H^\infty(n)=\omega$ for all
   $n$, then  all proofs about the Laver property can be translated
   into proofs for the corresponding facts about the Sacks property,
   by letting $H$ range over $\{H^\infty\}$ instead of over all
   increasing functions. 

In particular we get 
\begindent
\ite 1    $Q$ has the Sacks property \ iff \  $Q$ satisfies
   $\LaverH,r,s $ (where $H=H^\infty$) for all $r<s$ \ iff \ $Q$
       preserves~$\rvec^{H^\infty}$.
\ite 2  The Sacks property is    preserved under countable support
   iteration of proper forcing    notions. 
\endent



(Alternatively, the fact that the Sacks property is preserved by
countable support iteration follows fron the fact that $Q$ has the
Sacks property iff $Q$ has the Laver property and is \oob/.) 



%%  end of pres_examples.tex
%

\bigbreak
\bigskip\bigskip

{\bf  Application$^{\bf 2}$ ---  An Example:}




We continue the example from the introduction. 

Recall that we are trying to build a model where every set of $<\c$
many functions is bounded, the set of reals cannot be covered by $<\c$
many null sets, but there is a nonmeasurable set of size~$<\c$. 


Starting in $L$ we construct an countable support iteration
  $\<P_\alpha, Q_\alpha:\alpha<\omega_2> $ by requiring 
\begindent
\ite 1 If $\alpha $ is even, then $\forces_\alpha$``$Q_\alpha =
	\hbox{random real  forcing}$''. Let $r_\alpha$ be the name of
	the random real added by~$Q_\alpha$. 
\ite 2 If $\alpha $ is odd, then $\forces _\alpha Q_\alpha =
	\hbox{Laver real forcing}$.  Let $f_\alpha$ be the name of the
	Laver real added by~$Q_\alpha$. 
\endent
Then we have:  
\begindent
\ite 1 If $\name B$ is a $P_\beta$-name for a (code of a) Borel null
	set, and $\alpha>{\beta}$ is even, then 
$$ \forces_\varepsilon r_\alpha \notin \name B$$
\ite 2 If $\name f$ is a $P_\beta$-name for a function in $\fct$, and
	$\alpha>{\beta}$ is odd, then  
	$$ \forces_\varepsilon \name f <^* f_\alpha$$
\endent

(Note that $P_{\omega_2} $ is proper and satisfies the $\aleph_2$-cc,
  so no cardinals are collapsed.)


By \nonew/ we know that every real in $V[G_{\omega_2} ]$ in fact
	appears in some $V[G_{\beta}]$, for some ${\beta} <\omega_2$.
	So in $V_{\omega_2}$, no set of size $\aleph_1$ of functions
	is unbounded, and no family of Borel null sets of size
	$\aleph_1$ covers all reals numbers.

Hence $V_{\omega_2} \thinks \b=\d\ + \ \Cov(\measure0)$. 

To conclude this example, we claim that 
$$ V_{\omega_2} \thinks  \hbox{$\R \cut V_0$ is not of measure zero}$$

To prove this claim it is by \applynull/ enough to show that
  $P_{\omega_2}$ preserves \routvec.   By the general preservation
  theorem it is enough to show that for all $\alpha<\omega_2$ we get 
  $\forces_\alpha
  \hbox{$Q_\alpha$ preserves \routvec}$. 

But we remarked already that both random forcing and Laver forcing
  preserve \routvec{} (see \randomrandom/ and [\KunenMiller]). 

This finishes the application$^2$. 

%%  end of pres_examples.tex

%------------------------------------------------------
%           ****** 7: souslin proper  ********
%------------------------------------------------------		

%%%%%%%% pres_souslin.tex (started April 5, 1991)
%%%%%%%%%%%   file sous.tex (thesis? version) start %%%%%%
%%%%  (updated 19.10., better proof for stationary sets.)



\def\epd{{\sl epd}}

\neusection
\beginsection  7. Souslin Proper forcing


We review the basic facts about iteration of Souslin proper forcing
notions (from [\SouslinForcing] and [\pmbc]). 




\PROCLAIM\Souslinforcingdef/Definition:   Assume that $(Q, \le)$ is a
forcing notion. We say that $Q$ is a {\bf Souslin} forcing notion iff
$Q$, $\le$, and the incompatibility relation 
$\perp_Q$ are analytic sets.
\ENDPROCLAIM




(Note that in general incompatibility is a $\Pi^1_1$-relation (if
$\le$ is analytic), so the demand on $\perp$ really says that
incompatibility is a Borel relation.)


\PROCLAIM\univNot/Notation:  Using a universal $\Sigma^1_1$-set, we can
   associate with each real $d$ two $\PA$ relations $\le_d$ and
   $\perp_d$ (subsets of $\R \times \R$) such that every analytic pair
   $\le, \perp$ appears as some $\le_d, \perp_d$, and the relations $x
   \le_d y$ and $x \perp_d y$ are~$\Sigma^1_1$.
\ENDPROCLAIM





\PROCLAIM\ssfDef/Definition: We say that ``$d$ codes a   Souslin
   forcing'' iff
   \begindent
   \ite 1 $Q_d:= \<\field(\mathord{\le_d}), \mathord{\le_d}>$ is
          a partial
          quasiorder.  (We also write $Q_d$ for the underlying set
                  $\field(\mathord{\le_d})$) 
   \ite 2 For all $x,y\in Q_d$: $x \perp_d y \liff \lnot \exists z\in Q_d:
          x \weaker_d z \logand y \weaker_d z$, i.e., $\perp_d$ is
          equal to $\perp_{(Q_d,\le_d)}$,  the incompatibility
          relation for the forcing notion~$Q_d$.  
   \endent
\ENDPROCLAIM





\PROCLAIM\sfRem/Remark: 
  Clearly these are $\Pi^1_2$ conditions on~$d$. 
\ENDPROCLAIM



      




\PROCLAIM\genDef/Definition:  Assume  that $d$ codes a Souslin forcing
   $Q_d$, and $M$ is a transitive model  model of ZFC* that
     contains~$d$.    
   \begindent
   \ite 1  We let  $Q_d^M$ be the Souslin forcing coded by $d$ in~$M$. 
   \ite 2 If $p\in Q_d^M$, $q\in Q_d$, we say that $q$ is
	   $(p,M)$-generic,    iff 
	$$ q \forces_{Q_d}`` G_{Q_d}\cut M \hbox{ is $Q_d^M$-generic over
	   $M$ and contains~$p$.''}$$
   \ite 3  We say that ``$Q_d$ is a  Souslin Proper forcing'' or ``$d$
	   codes a  Souslin Proper forcing'' if $d$ codes a Souslin
		forcing, and  
    $$ \vcenter{\hsize=0.7\hsize\parindent=0cm 
            for all countable $M$ as above,  every $p\in Q_d^M$
         there exists a $(p,M)$-generic $q\in Q_d$}\leqno\qquad(*)$$
\endent

The property that $\perp$ is analytic is sometimes not
          necessary.  We say that $(Q, \le)$ is weakly Souslin, if
          $\le$ (but not necessarily $\perp_Q$) is analytic.
Similarly, we say that $(Q, \le)$ is 
          weakly Souslin proper if in addition, (3)($*$) holds.  
 % See           also \SouslinPlus/. 
\ENDPROCLAIM









\PROCLAIM\spfRem/Remark: (1)  ``$d$ codes a Souslin proper forcing'' is a
   $\Pi^1_3$ statement about~$d$.  Hence (by Shoenfield's absoluteness
   theorem) if it holds in $V$, it holds
       in  every submodel that contains all countable ordinals. 

(2) If $(M,\eps)$ is a transitive model of a sufficiently large part
   of ZFC ($M$ may be a class), and  $M \thinks$``$\chi:=\beth_\omega^+$
   exists, and $M_0:=H(\chi)^M$ is  countable, 
   then $M_0$ is a countable model of ZFC*, and $q$ is $(p,M)$-generic
   iff $q$ is $(p,M_0)$-generic.   So for all practical purposes we
   can pretend that $M$ is countable. 
   (In particular this is true if $\omega_1$ is a  
   inaccessible  cardinal in~$M$.)
\ENDPROCLAIM






Proof: (1)  Every countable model $M$ is isomorphic to some
   well-founded~$(\omega,R)$.
   If $x\in \R^M$, we also write $x$ for its image under this
   isomorphism. 

It is enough to show that ``$d$ codes a  Souslin Proper
         forcing notion'' is a $\Pi^1_3$ statement. 

$d$ codes a  Souslin proper forcing iff 
 \underbar{for all} $R
   \subseteq \omega\times \omega$
\begindent
\item {} Either $(\omega,R)$ is not well-founded (i.e., \underbar{there
                                 exists} an $R$-descending sequence)
\item {} or $(\omega,R)\not \thinks ZFC^*$ (this is $\Delta^1_1$)
\item {} or $d\notin (\omega,R)$
\item {} or for all $p\in Q_d^M$ \underbar{there is} $q\in Q_d$ such
   that \underbar{for all} $r \stronger q$ 
          \begindent
          \ite i  for all $D$ such that $(\omega,R)\thinks $
                  ``$D$ is open dense in~$Q_d$'', there
                  is an $i$, $(\omega,R)\thinks i\in D$,
                  $r\not\perp i$   
          \ite ii $r \not\perp p$. 
          \endent
\endent
((i) implies that $q \forces G \cut D \not= \emptyset$, and (ii)
                         implies that $q \forces p\in G$.)

Proof of (2):  $M$ and $M_0$ contain the
   same dense sets of~$Q_d$. 




\PROCLAIM\setUp/Context:  In this whole section, ${\varepsilon}$ will be
   an  ordinal 
   $\le \omega_2$. 
   $S$ will be a countable subset of $\omega_2$ that is
    closed under immediate successors and predecessors, where the
                       order  type of $S$  is in~$M$.
   $\alpha $  and $\gamma$ will stand for  ordinals $\le
   {\varepsilon}$ in~$S$.  
   $M$ will be a  countable transitive model of ZFC* (= a large enough
   fragment    of ZFC), or an ``essentially'' countable model as in
   \spfRem/(2). 


  For $\alpha\in S$, let
   $\alpha^S $ be the  order type of $\alpha \cut S$.  

  ${\dvec}$ will be a sequence of length ${\varepsilon}$, and
   ${\cvec}$ will be a sequence of length ${\varepsilon}^S$,
   ${\cvec}\in M$. 
\ENDPROCLAIM







\PROCLAIM\PdvecDef/Definition: 
  Given a sequence ${\dvec} = \sq d \alpha \varepsilon$ we 
   define 
  a countable support iteration \iter, 
   by letting  $Q_\alpha $  be a
   $P_\alpha$-name of $Q_{\dval\alpha}$ (if this is Souslin proper),
   i.e.\ 
   $P_\alpha$ forces the following: 

   \cleartabs
   \tabalign\qquad\qquad If $\dval\alpha $ &is a code for a Souslin proper
          forcing, then $Q_\alpha = Q_{d_\alpha}$ \cr
   \tabalign & otherwise  $Q_\alpha= \{\emptyset\}$ is the trivial forcing.\cr

\ENDPROCLAIM




\bigskip
\PROCLAIM\PvecNot/Notation and Remark: 
  We write $\bar{Q}_{\vec {d}}$ for the iteration defined above, and we
   write $P_{\dveca}$ for $P_\alpha$, i.e., 
   $P_{\dveca} $ is the $\alpha$-th iteration stage obtained from the
   definition ${\dvec}$, and $Q_\alpha = Q_{d_\alpha}$ describes the
   successor extension.   If ${\dvec}\in M \thinks ZFC^*$, then 
   $P_{\dveca}^M$ is the $\alpha$-th iteration
   stage, computed from the definition ${\dvec}$ in the model~$M$. 



We say ``$\dvec$ codes a Souslin proper iteration'', if for all
$\alpha$, ${} \forces_{P_{\dveca}} d_\alpha$ codes a Souslin Proper
forcing. 

\ENDPROCLAIM




  We will consider sequences ${\dvec} $ and ${\cvec}$, where $|{\dvec}|
   = {\varepsilon} $ and $|{\cvec} | = {\varepsilon} ^S$, ${\cvec} \in M$.





  \bigskip



\PROCLAIM{\restDef}/Definition: Assume $M$, ${\cvec}$, ${\dvec}$, $S$,
   ${\varepsilon}$ are as in \setUp/.

  By induction on $\alpha \in S \cut {\varepsilon} $, we will define a
   $P_\alpha$-name $\flta G_\alpha on S M$ (which we usually
   abbreviate to $G'_\alpha $ or $ G_\alpha \on (S,M)$), by requiring
   that $\emptycondition_{P_\alpha}$ forces the following:

  \begindent
   \item{} $G'_\alpha \subseteq P_{\cveca}^M$ and  
   \item{$\bullet$}  If $\alpha = \beta + 1$, and 
     \begindent
     \ite a $G'_\beta $ is $(P_{\beta^S}^M,M)$-generic
     \ite b $\dval\beta=\cval\beta $
     \ite c $\dval\beta$ codes a Souslin Proper forcing (in
		      $V[G_\beta]$)
     \endent

    then $G'_\alpha = G'_\beta*\left(G(\beta)\cut M[G'_\beta]\right)$
\item{} If $\alpha = \beta+1$ and (a)--(c) does not hold, then
   $G'_\alpha= \emptyset$. 

   \item{$\bullet$} If  ${\alpha} $ is a limit, then for $p \in
        P_{\cveca}^M$ we let  
   $$ p \in G'_{{\alpha} } \,\,\liff \,\,
   \forall \beta \in S \cut  \alpha \,\,p\on \beta^S \in
    G'_{\beta} $$
   \endent
\ENDPROCLAIM




\PROCLAIM\corrDef/Definition: We call $\dvec$ and $\cvec$ 
   ``corresponding'' sequences if for all $\alpha < \varepsilon $, 
   $$ \forces_\alpha 
   \hbox{If $G'_\alpha$ is generic over $M$, then
   $c_{\alpha^S}[G'_\alpha] = d_\alpha[G_\alpha]$}$$ 
\ENDPROCLAIM




\PROCLAIM\corrconv/Remark:   We will only consider sequences $\dvec$ that
   code a Souslin proper iteration (see \PvecNot/), and we will only
   consider corresponding~$\cvec$. 
\ENDPROCLAIM






\PROCLAIM\restRem/Remarks and Notation: 
   \begindent
   \ite 1  whenever the parameters $M$, $S$,  ${\cvec}$, ${\dvec}$  are
   clear from the context we will write $G'_\alpha$ for 
   $\flta G_\alpha on S M$. %%%, similarly for~$\mu_\alpha$.   
   \ite 2 
   If $G_\alpha$ is a $P_{\dveca}$-generic
   filter, then we also write $G'_\alpha$ for the evaluation of
   the name $G'_\alpha$ by $G_\alpha$, similarly for~$\mu_\alpha$. 
   \ite 3 Let~$M_\alpha=M[G'_\alpha]$.  
   \ite 4 It might seem  more natural to write $\flt G_\alpha on S M$ as
   $G'_{\alpha^S}$ ($=(G')_{\alpha^S}$) 
   instead of $G'_\alpha= (G_\alpha)'$, but this would only complicate
   the notation. 
   \ite 5 ``$G'_\alpha$ is generic'' means of course ``generic for the
       forcing $P_{\cveca}^M$ over the model $M$''. 
   \endent
\ENDPROCLAIM










\PROCLAIM\simplyGeneric/Remark:  Assume  $\cvec$ and $\dvec$ are as in
   \corrconv/, and   $M \thinks $``$\name{p} $ is a
   $P_{\cvec\on\gamma^S}^M$-name of a   
   condition in $ P_{\cvec}^M$''.  

We say  that $q$ is $\name p$-generic (or more precisely, $(\name p,
   {\gamma}, M, S, \name c, \name d)$-generic) iff $q$ forces: 

\begindent
\itemitem{{\bf (A)}} $G'_\varepsilon$ is generic over~$M$. 
\itemitem{{\bf (B)}} $\name p [G'_\gamma] \in G'_\varepsilon$. 
\endent
\ENDPROCLAIM



      






\PROCLAIM\itpropTheo/Theorem: 
   Let ${\dvec}$, ${\cvec}$, $S$, $M$, $\gamma$, $\varepsilon$ be as
   in \setUp/.   Assume that $M
   \thinks ``\name{p} $ is a $P_{\cvec\on\gamma^S} $-name for a
   condition in $P_{\cvec}$'' (so $\name{p} \on \gamma $ is the name for
   its restriction to $\gamma$, and there is a canonical $P_{\cvec}
   $-name which we also call $\name{p}$).

  Assume that $q\in P_{{\dvecg} } $ is $(\name{p}\on \gamma,\gamma,
   M,S, {\cvec\on\gamma^S} , {\dvecg} )$-generic.  
Then there exists a   condition $q^+\in P_{\dvec} $ such that $q^+\on
\gamma = q $ and $q^+   $ is $(\name{p}, \gamma , M,S, {\cvec} ,
{\dvec})$-generic.  
\ENDPROCLAIM







\PROCLAIM\itpropCor/Corollary: Assume $M \thinks p \in P_\cvec$.  Then
   there exists a $(p,M)$-generic condition $q\in P_\dvec$. 
\ENDPROCLAIM










\medskip
{\bf Proof of \itpropTheo/:}





  The proof is by induction on~$\varepsilon$.

Successor step: Here is the only
  place where we explicitly use Souslin properness: 
  let  $\varepsilon = \alpha+1$.



  Using the induction hypothesis on $\alpha$, we get 
   a $(\name{p}\on \alpha, \gamma )$-generic condition
   $q^+\on \alpha \in P_\alpha $. To find $q^+(\alpha)$, we will work in
   $V[G_\alpha]$, where $G_\alpha$ is an arbitrary generic filter
   containing $q^+\on \alpha$.  Let $d:= \dval\alpha$ (=
   $\cval\alpha$, because $\cvec$ and $\dvec$ are corresponding
   sequences).  

Since 
  \begindent
  \ite a $G'_\alpha \subseteq P_{\cveca} $ is generic over $M$
  \ite b $V[G_\alpha] \thinks d$  codes a Souslin   proper forcing,
  \endent
\noindent 
and  $p(\alpha)[G'_\alpha]$ is in the Souslin proper forcing $Q_d$,
    by definition we can find  an  
   $(p(\alpha)[G'_\alpha],M_\alpha)$-generic condition~$q^+(\alpha)$. 
 

  Coming back to $V$, we use the existential completeness lemma to get a
   name (which we also call $q^+(\alpha)$) about which the above  is forced
   by $q^+\on \alpha$. 

Clearly this  construction ensures that  $q^+$ is  generic, by
   \filterFact/. 




\bigskip\medskip

Limit step: let $\<\alpha_n:n<\omega>$ be a cofinal sequence in
   ${\varepsilon}\cut S$,~$\alpha_0=\gamma$. 
   Let $\<D_n:n\in \omega> $ enumerate
   all dense open subsets of $P_{\cvec}^M$ that are in~$M$. 



  First we will define a sequence $\<\name{p}_n: n \in \omega>$, 
   $\name{p}_n\in M$, $\name{p}_0 = \name{p}$, 
   such that $\underline{\hbox{in $M$}}$ the following will hold: 
   \begindent
   \item{(0)}
   $\name{p}_n$ is a $P_{\cvec\on \alpha_n^S}  $-name   %%   cveca !!
   for a condition in
   $P_{\cvec}$ 
   \item{(1)} $\forcess_{{\alpha_{n+1}^S}} \name{p}_{n+1} \stronger
   \name{p}_n$ 
   \item{(2)} $\forcess_{{\alpha_{n+1}^S}} \name{p}_{n+1}\in D_n$. 
   \item{(3)} $\forcess_{{\alpha_{n+1}^S}}$
   If  $\name{p}_n\on{\alpha_{n+1}^S} \in G_{\alpha_{n+1}^S}$ then 
   $\name{p}_{n+1}\on {\alpha_{n+1}^S} \in G_{\alpha_{n+1}^S}$. 
   \endent
  (Here, of course, $G_{\beta}$ stands for the canonical name (in $M$)
   for the generic object of $P^M_{{\cvec}\on \beta}$, and
   $\forces_\beta$ is the forcing relation of $P^M_{\cvec\on \beta } $ in~$M$.)

  For each $n$ we thus get a name $\name{p}_{n} $ that is in~$M$.   We use
  \newPrelim/ and 
\exComplete/ 
  (in $M$) to obtain~$\name{p}_{n+1}$. 


  Now we define a sequence $\<q_n: n \in \omega>$, $q_n \in
   P_{\alpha_n}$, $q_0=q$, such that for all $n$: 

  \begindent
  \ite a $q_n\in P_{\alpha_n}$, 
	  $n\ge1 \limpl q_n\on {\alpha_{n-1}} = q_{n-1}$. 
  \ite b $q_n$ is generic for $\dveca$, $\cveca$, $S$,~$M$.
	%%%	  $(\name{p}_n\on{\alpha_n^S},{\alpha_n^S})$-generic 
  \ite c $q_n \forces \np_n\on \alpha_n^S \in G'_{\alpha_n}$. 
	%%%	  $(\name{p}_k\on {\alpha_n^S}, \alpha_k^S)$-generic. 
  \endent




  $q_{n+1} = q_n^+ $ can be obtained  by the
   induction hypothesis, applied to ${{\alpha_n^S}}$, ${\alpha_{n+1}^S}$, and
   $\name{p}_n\on {\alpha_{n+1}^S} $.  

  $q_{n+1} = q_n^+$  can be obtained  by the
induction hypothesis, applied to ${{\alpha_n}}$, ${\alpha_{n+1}}$, and
$\np_n\on {\alpha_{n+1}} $.  By (c)$^\splus$ we know 
$$q_n^+ \forces (\np_n)\on
{\alpha^S_{n+1}}  \in
 G'_{\alpha_{n+1}}  \cut M $$
Hence by (3) we have 
$$q_{n+1} \forces (\np_{n+1})\on
{\alpha^S_{n+1}}  \in
 G'_{\alpha_{n+1}}  \cut M $$

 Since $q_{n+1}\on {\alpha_n} = q_n$,
         $q = \lim q_n$ exists and is ${} \stronger q_n$  for all~$n$.
  

We have to show that $q \forces p \in G'_{\varepsilon } \cut M $ and that $q$
is generic. Let $G_{\varepsilon}$ be a generic filter containing~$q$.  We
will write $p_n$ for~$\np_n[G'_{\alpha_n}]$.  (Note that $p_n\in M$,
   because $q_n$ was $M$-generic and $q_n\in G_{\alpha_n} $.)


Since $q_n \weaker q \in G_{\varepsilon}$, we have $ p_n \on
   {\alpha^S_n}\in G_{\alpha_n} \cut M$ and $M \models p_n \stronger
   p_{n-1} \stronger \cdots\stronger p_0 $.

Hence  $ p\on {{\alpha^S_n}} \in
 G'_{\alpha_n} \cut M$ for all $n$, and so by \Factfour/, 
$ p\on {\delta}  \in  G_{\delta}  \cut M $.  As $dom(p) \subseteq
 {\delta}$, $p\on {\delta} = p$, so  $p\in G_{{\varepsilon}}$. 
 Similarly, $p_n\in G_\varepsilon$ for all~$n$. 

Consider a dense set $D_n \subseteq P_{\varepsilon}$.  Since  $q_{n+1}
\forces$``$ \np_{n+1} \in  D_n$,'' we  have $p_{n+1}\in G_\varepsilon \cut
D_n \cut M$. 

Hence $q$ is generic. 



\bigskip


Shelah has suggested the following modification of the definition of
Souslin forcing:   

\PROCLAIM\SouslinPlus/Definition:    Assume $(Q,\le)$ is a
forcing notion, $ Q \subseteq \fct$ and $\epd_Q$ (``effectively
predense'') is a relation on
$Q\times [Q]^\omega $.  
$(Q,\le, \epd)$ is called a $\underline{\hbox{Souslin}^+}$ forcing if
\begindent
\ite 1 $\le$ is analytic,   and $\epd$ is a 
	${\bf \Sigma}_2^1$ set.
\ite 2 If $\epd(q, \{p_i:i<\omega\})$, then $\{p_i:i<\omega\}$ is
       predense below~$q$.
\endent

      
$(Q,\le, \epd)$ is called $\underline{\hbox{Souslin}^+\hbox{ proper}}$
       iff in addition 
\begindent
\ite 3 Whenever $(M,{\in})\thinks ZFC$ is a countable model, $Q\in M$
       (i.e., the formulas defining $\le_Q$ and $\epd_Q$ have
       parameters in $M$), and $p\in Q\cut M$, then there is a
       condition $q \stronger p$ such that 
$$ \vcenter{\hbox{For all $A\in M$, if $M \thinks A$ is predense below
       $p$}\hbox{\quad then
       $\epd(q,A\cut M)$}}\leqno\qquad(*)$$
\endent
\ENDPROCLAIM



      

\PROCLAIM\effgendef/Definition:  We call a condition $q$ satisfying $(*)$
	``$(p,Q,M)$-effectively generic''. 
\ENDPROCLAIM




\PROCLAIM\effgenFact/Fact:  If $q$ is $(p,Q,M)$-effectively generic, then
	$q$ is $(p,M)$-generic. 
\ENDPROCLAIM




Note that for Souslin forcing the relation ``$q$ is $(Q,M)$-generic''
is in general only $\Pi^1_2$, whereas the relation $(*)$ above is
$\Sigma^1_2$.  



\PROCLAIM\SacksEx/Example:  Sacks forcing is Souslin$^+$ proper. 
\ENDPROCLAIM




Proof:  

Recall  that Sacks forcing $\S$ is the set of all  perfect trees $\subseteq
\finzerooneseq $.  (The incompatibility relation for Sacks forcing is
not analytic, because  to find a condition $r$ extending
$p$ and $q$, one has to intersect the trees $p$ and $q$ (this is an
arithmetical computation) and then find a perfect subtree $r \subseteq
p\cut q$.  The Cantor-Bendixson argument needed to obtain this tree
$r$ may take any countable number of steps, so an argument using the
boundedness principle should show that ``$p\perp q$'' is not analytic.)






We let $$\epd(q, \{p_i:i<\omega\}) \ \liff \ \exists F
       \subseteq q, \hbox{$F$ is a front}, \forall \eta\in F\,\exists
       i\,\, p_i \weaker \trim q^\eta{}  .$$

(Recall that $F \subseteq q$ is  called a front, if $F$ is an
       $\subseteq$-antichain that meets every branch of $q$, and
       $\trim q^\eta = \{\nu\in q: \nu \subseteq \eta \lor \eta
       \subseteq \nu\}$.)

Clearly $\epd(q, A)$ implies that $A$ is predense below~$q$. 


To show that condition (3) is satisfied, we need a few definitions and
a lemma 
about Sacks forcing~$\S$.     


\PROCLAIM\splitDef/Definition:  For $p\in \S$ we let 
$$\eqalign{\split(p)&:=\{\eta\in p: \eta\extend0\in p\logand
\eta\extend 1\in p\}\cr 
\split_n(p)&:= \{\eta\in \split(p): |\{\vu\in \split(p):\vu \subset
			\eta\}|=n\}} $$
$\stem(p)$ is the unique element of $\split_0(p)$, i.e., the first
node in $p$ at which splitting occurs. 

If $p\in \S$, $D \subseteq \S$, we write 
$p\in^*D$ iff there is a pure extension $r$  of $p$ such that $r\in
D$.  ($r$ is a pure extension of $p$ if $\stem(p)=r$). 
\ENDPROCLAIM





\PROCLAIM\Dlemma/Lemma: Assume $D \subseteq \S$ is an open dense set, and let
$p\in\S$, $n\in \omega$.  Then there  is a condition $q \stronger_n p$ 
and a front $F \subseteq q$ such that $\forall \eta\in F$, 
$\trim q^\eta\in^*D$.  
\ENDPROCLAIM




Proof:  Consider the following game $G(D,p,n)$:  There are two
players, who play $\omega $ many moves.   We let $A_{-1}:=\split_{n+1}
(p)$. 

In the $n$th move, player I plays $\eta_n\in A_{n-1}$, and player II
responds by playing a set $A_n \subseteq p$ of pairwise incompatible
elements of $\zerooneseq$, $|A_n|\ge 2$, and
$\forall \nu\in A_n$, $\nu \supseteq \eta$. 

Player I wins, if for some $k$, $\trim p^{\eta_k} \in^* D$. 

We claim that player II has no winning strategy.   For assume that
${\sigma}$ is a winning strategy for player II, then we can define 
$$ q:=\set(\eta\on l: $l\le |\eta|$, $\eta$ appears as some $\eta_n$ in
						a play in which& 
		player II obeyed ${\sigma}$)$$

Clearly $q$ is a tree.   $q$ is perfect:  Assume $\eta\in q$. So there
is an initial segment $\<\eta_0, A_0, \ldots, \eta_k, A_k>$ of a play
in which player II obeyed ${\sigma}$, and $\eta \subseteq \eta_k$.
Let $\nu_0$, $\nu_1$ be two incompatible elements of $A_k$, then both
$\nu_0$ and $\nu_1$ are in~$q$.   Hence $q \in \S$.    It is also
clear that $q \stronger_n p$.    

But if ${\sigma}$ was a winning strategy for player II, then for all
$\eta\in q$, $\trim q^\eta \notin^* D$, a contradiction. 



The game is closed, so player I must have a winning strategy~$\tau$.
Let $q$ be defined as above, with ``player II obeys ${\sigma}$''
replaced by ``player I obeys $\tau$''.  

Again $q$ is perfect:  Let $\eta\in q$, so $\eta \subseteq \eta_k$,
where $\<\eta_0, A_0, \ldots, \eta_k>$ is an initial segment of a play
in which player I obeyed~$\tau$.  There are 4 incompatible extensions
$\nu_0$, $\nu_1$, $\nu_2$, $\nu_3$ of~$\eta_k$.   Let 
$$ \<\eta_0, A_0, \ldots, \eta_k, \{\nu_0, \nu_1\}, \eta'>\quad
\hbox{and} \quad  \<\eta_0, A_0, \ldots, \eta_k, \{\nu_2, \nu_3\},
\eta''>$$
be initial segments of plays according to~$\tau$.  Then $\eta'\in
\{\nu_0, \nu_1\}$, $\eta''\in \{\nu_2, \nu_3\}$, so $\eta'$ and
$\eta''$ are incompatible extensions of $\eta$ in~$q$.  Since $\tau$
is a winning strategy, we can find a front as required.

\PROCLAIM\coroffronts/Corollary: If $D \subseteq \S $ is dense open, $p\in
\S$, $n\in \omega$, then there is $p' \stronger_n p$ and a front $F
\subseteq p'$ such that for all $\eta \in F$, $\trim {p'}^\eta \in D$. 
\ENDPROCLAIM




Proof: FIrst we can get a condition $q$ and a front $F \subseteq q$ as
in the previous lemma.  We may assume that the front $F$ is above the
$n$-th splitting level,  i.e., $\forall \eta\in \split_n(q) \, \exists
\vu \in F\, \eta \subseteq \nu$.  Now thin out $q$ at each $\eta\in F$
to get into $D$, i.e., for all $\eta\in F$ let $q_\eta \stronger
\trim q^\eta$ be a condition with stem $\eta$, $q_\eta\in D$, and let
$p':= \bigcup_{\eta\in F} q_\eta$. 

{\bf Proof of \SacksEx/:}  Let $M \models ZFC$, $p\in P
\cut M$, and let  $\<D_n:n\in m>$ enumerate all sets $D$ such that $M
\thinks D$ is dense open below $p$. Using \coroffronts/ we can find a
sequence $\<(p_n, F_n):n\in \omega>$, $p=p_0 \weaker_0 p_1 \weaker_1
\cdots$, $p_n, F_n \in M$, $F_n \subseteq p_n$ a front, and $\forall
\eta \in F_n\, \trim q_n ^\eta \in D_n$.  Let $q \stronger p_n$ for
all $n$, then $F_n \cut q$ is a front in $q$, and for all $\eta\in F_n
\cut q$ we have $\trim q^\eta \in D$.  Now it is easy to see that for
all $A\in M$, if $M \models A $ predense below $p$, then $A \cut M$ is
effectively predense below $q$. 







\PROCLAIM\finalrem/Remark: Similar arguments apply to many other
forcing notions whose elements are perfect trees --- Laver forcing,
rational perfect sets, etc.  A theorem analogous to \itpropTheo/ can
be shown for Souslin$^+$ proper forcing notions. 
\ENDPROCLAIM






\bigskip

%------------------------------------------------------
%           ******  6: preservation fsi  ********
%------------------------------------------------------		

%% pres_finite.tex  (added May 26, 1991)
% preservation thm for finite support iteration.

\neusection
\beginsection{\printchapternumber 8\quad A simple preservation theorem
for finite support iteration} 



\def\finR{\sqsubset}
\def\notfinR{\not\sqsubset}


\PROCLAIM\newcontext/Context:  Similar to \context/. 
\ENDPROCLAIM

\PROCLAIM\finAssumption/Assumption:  We assume that for all $f\in \C$ the set 
	 $\{g: f \re _n g\} $ is closed.  (Often we even have that
	$\re _n$ itself is closed, in some reasonable topology.)
\ENDPROCLAIM











\PROCLAIM\moClosed/Definition:  We say that $M$ is $(\rvec,
	\omega)$-closed if  
$$ \forall A \subseteq M \cut \C \hbox{ ($A$ countable) } \ \exists
	f^*\in M : $$
$$ \forall g: \ f^* \re  g \limpl \forall f \in A \cut \C \, f \re  g \eqno(*)$$
\ENDPROCLAIM




\bigskip
Remark: Note that $(*)$ is a $\Pi^1_1$-statement, hence absolute
	between any $\in$-models of ZFC. 
\bigskip



\PROCLAIM\finiteTheo/Theorem:  Assume $M \subseteq V$ is $(\rvec,
	\omega)$-closed. Let $\iter$ ($\varepsilon $ limit) be a
	finite support iteration of ccc forcing notions such that 
$$ \forall \alpha<{\delta} \ \  \forces_{\alpha} \forall g\, \exists
	f\in M\cut \C\, \, f\not \re g$$
Then $ \forces_{\delta} \forall g\, \exists f\in M \, f\not \re g$. 
\ENDPROCLAIM




Proof:  By \nonew/, we may assume that~$cf({\delta})=\omega$.   Assume the
	conclusion is false, so there is a condition $p_0\in
	P_{\delta}$ and a $P_{\delta}$-name $\ng$ such that $p_0
	\forces \forall f \in M \,\, f \re \ng$. 

Let ${\delta}_0 < {\delta}_1 < \cdots\,$ be a sequence of ordinals
	conerging to~${\delta}$.  For each $n$, let $\ng_n$ be a
	$P_{{\delta}_n}$-name such that 
$$ \forces_{{\delta}_n}  \hbox{$\ng_n$ interprets $\ng$ } 
\qquad \hbox{(considering $\ng$ as a $P_{\delta_n} $-name for a
	$P_{\delta}/G_{\delta_n}$-name)}$$
and let $\nf_n$ be a $P_{\delta_n}$-name such that 
$$ \forces_{\delta_n} \nf_n\in M \logand \nf_n \not \re h$$
Since $P_{\delta}$ is ccc (even properness is sufficient here), there
 is  a countable set $F\in V$, $F \subseteq \C$  such that $\forall n\,
	\forces _{\delta_n} 	\nf_n\in F$. 

By our assumption, $M$ is $(\rvec, \omega)$-closed.  So  we can find a
	function $f^*\in M$ such that 
$$ \forall h \in \fct :  f^* \re h \limpl \forall f\in F \cut \C\, f \re 
	g$$
Since $f^*\in M$, $p_0 \forces_{\delta} f^* \re \ng$.  We can find a
	condition $p_1  \stronger p_0$ and an integer $n$ such that
	$p_1 \forces f^* \re_n \ng$.   Since $p_1$ has finite support,
	there is an $m\in \omega$ such that $p_1\in P_{{\delta}_m}$.  

Now work in $V[G_{\delta_m}]$, where $p_1\in G_{\delta_m}$.  Clearly
	$\forces _{{\delta_m}, {\delta}} f^* \re_n \ng$. 
Since $f_m \not \re_n g_m $ (where $f_m = \nf_m[G_{\delta_m}]$,
	$g_m=\ng_m[G_{\delta_m}]$), we also 	have $f^* \not \re _m
	g_m$.

We consider the set $\{h : f^* \not \re _m h\}$.  By assumption on $\re $,
	this is an open set, containing~$g_m$. So there is $k\in
	\omega$ such that 
$$ \forall h : h \on k = g_m \on k  \limpl f^* \not \re_n h$$
Let $q\in P_{\delta}/G_{\delta_m} $ be a condition forcing $\ng\on k =
	g_m\on k $.   Then $q $ also forces $f^* \not \re_n \ng$, a
	contradiction. 





\bigskip

\PROCLAIM\finExone/Example 1: Let  $$f \re_n g  \ \liff\  \forall k\ge n\,
   f(k)<g(k)$$
\ENDPROCLAIM




The ``bounding'' number $\frak b$ is defined by 
$$ {\frak b}:=\{ \min|B|: B \subseteq \fct, \hbox{$B$ is unbounded}\}$$
where ``$B$ is unbounded'' means that there is no function $g$ such
that for all $f\in B$ we have $f \re g$.  We are interested
in preserving an unbounded family.   It is easy to construct (by
induction) an unbounded family $B$ that is well-ordered by $\re$ and
has order type $\frak b$.  It is also easy to see that the cofinality
of $\frak b$ must be uncountable.  

Hence $B$ is $(\re,\omega)$-closed. So we get

\PROCLAIM\finbd/Fact: Assume $\iter$ is a finite support iteration of
ccc forcing notions such that for all $\alpha$ we have 
$$ \hbox{$\forces_\alpha $ $B$ is unbounded in $\fct \cut V[G_\alpha]$}$$
Then 
$$ \hbox{$\forces_\varepsilon $ $B$ is unbounded in $\fct \cut
			V[G_\varepsilon]$}$$ 
\ENDPROCLAIM




Proof: Apply \finiteTheo/. 


In particular, we get: If no $Q_\alpha$ adds a dominating function,
and $V \thinks {\frak b} = \kappa$, then $V[G_\varepsilon] \thinks
{\frak b } \le \kappa$. 

\PROCLAIM\finExtwo/Example 2:   Let $\routvec$ be defined as in \outRdef/.
It was proved above that $f \re g$ iff $g$ is not in the null set
coded by~$f$.   So, letting $M=V$ (which is clearly
$(\routvec,\omega)$-closed, we get 
\ENDPROCLAIM




\PROCLAIM\secondfact/Fact: If \iter\ is a finite support iteration of 
ccc forcing notions such that for all $\alpha$ we have 
$$ \hbox{$\forces_\alpha $ there is no random real over $V$} $$
then 
$$ \hbox{$\forces_\varepsilon  $ there is no random real over $V$} $$
\ENDPROCLAIM




\goodbreak
\vskip0.2\vsize\goodbreak
REFERENCES.



\newcount\refno
\def\key#1[#2]{\advance\refno by 1
			\write\mgfile{\string\def\string#1}
			\edef\next{\noexpand\write\mgfile{{\number\refno}}}
			\next
\medskip\noindent[#1] \ignorespaces}
\parindent=0cm\hangindent=1cm\hangafter1


\def\byBgJ{J.~Bagaria and  H.~Judah}
\def\byBarto{T.~Bartoszynski}
\def\byBGJS{T.~Bartoszynski, M.~Goldstern, H.~Judah, S.~Shelah}
\def\byG{M.~Goldstern}
\def\byGJ{M.~Goldstern, H.~Judah}
\def\byGJS{M.~Goldstern, H.~Judah,  S.~Shelah}
\def\byGS{M.~Goldstern, S.~Shelah}
\def\byGTT{M.~Goldstern, R.F.~Tichy,  G.~Turnwald}
\def\byJ{H.~Judah}
\def\byJS{H.~Judah and S.~Shelah}
\def\byJSW{H.~Judah, S~Shelah, H.~Woodin}


\def\paper#1,{{\it #1}, } \def\by{}\def\publ#1\publaddr#2\yr#3 {#1, #2 #3}
\def\inbook#1,{in:  #1, }  \def\nextreference#1\par{\bigskip \noindent#1}
\def\journall#1:#2(#3)#4--#5.{#1, {\bf #2} (#3), pp.#4--#5.}
\def\journalp#1:#2(#3)#4.{#1, vol~#2 (#3), p.~#4.}
\def\book#1,{{\it #1},} \def\vol#1 {Vol.~#1}
\def\pages#1--#2{pp.#1--#2}


\def\AnML{Annals of Mathematical Logic}
\def\AcM{Acta Mathematica}
\def\ArML{Arch.\ math.\ Logik}
\def\ArM{Archiv der Mathematik}
\def\AnM{Annals of Mathematics}
\def\AnPAL{Annals of pure and applied logic}
\def\FM{Fundamenta Mathematicae}
\def\IJM{Israel Journal of Mathematics}
\def\JSL{Journal of Symbolic logic}
\def\MoMa{Monatshefte f\"ur Mathematik}
\def\NDJFL{Notre Dame Journal of Formal Logic}
\def\TAMS{Transactions of the American Mathematical Society}
\def\PAMS{Proceedings  of the American Mathematical Society}
\def\PAcad{Proc.\  Nat.\ Acad.\ Sci. U.S.A.}
\def\handbookST{\inbook Handbook of Set-Theoretic Topology,  ed.\ by
        K.~Kunen and J.E.~Vaughan,  North-Holland,
        Amster\-dam--New York--Oxford 1984}
\def\contemporary{\inbook Axiomatic Set Theory, Boulder, Co 1983, 143--159,
Contemporary Math 31, AMS, Providence RI 1984}







%Baumgartner:Iterated forcing
 \key\IteratedForcing[Ba:IF] J.~Baumgartner, \paper{Iterated forcing},
        \inbook{Surveys in set theory {\rm
        (A.~R.~D.~Mathias, editor)}}, London Mathematical
        Society Lecture Note Series, No.~8, Cambridge
        University Press, Cambridge, 1983.       


 \key\GraysThesis[Gr:Th] \by C.~Gray: Ph.D. thesis, University of
California, Berkeley. 


\key\pmbc[GJ:pm]  M.~Goldstern, H.~Judah, \paper{Iteration of
        Souslin Forcing, Projective Measurability and the
        Borel Conjecture}, accepted by  \IJM. 


%Jech:Set theory, Academic Press, New
 \key\JechSt[JE:ST] T.~Jech, \book Set theory, Academic Press, New
        York, 1978.    

 \key\SouslinForcing[JS:SF] \by \byJS: \paper Souslin
        forcing, 
        \journall \JSL:53(1988)1188--1207.    


\key\DeltaOneThree[JS:d13]  H.~Judah and S.~Shelah, \paper
        $\Delta^1_3$-sets of reals, MSRI publication series. 

\key\KunenMiller[JS:KM] H. Judah and S. Shelah, \paper The Kunen
          Miller chart, \JSL, 1990. 



%Kunen: Set Theory
 \key\Kunen[Ku:ST] K.~Kunen, \book Set Theory: An Introduction to
         Independence Proofs,  North Holland,
        Amster\-dam-New~York-Oxford, 1980.


\key\Chaz[Sch:it] C.~Schlindwein, \paper Revised countable
        support iteration, to appear in \AnPAL


%Shelah:Proper Forcing, Lecture Notes
 \key\ProperForcing[Sh:PF] S.~Shelah, \book Proper Forcing, Lecture Notes
        in Mathematics \vol942 , Springer Verlag.    

 \key\ProperImproper[Sh:PI] S.~Shelah, \book Proper and Improper
         Forcing, to appear in Lecture Notes      in Mathematics,
         Springer Verlag.    


\key\CLXXVII[Sh:177] S.~Shelah, \paper More on proper forcing,
		\journall\JSL:49(1984)1035--1038.  


%Solovay Tennenbaum:Iterated
 \key\IteratedCohen[ST:IC]  R.~Solovay and S.~Tennenbaum, \paper
         Iterated Cohen extensions and Souslin's  problem,
         \journall\AnM:94(1971)201--245.   


\finish
\bye

%  That's all folks! You have just received: 
%  Paper number: 7
%  By:   Martin Goldstern
%  Title: Tools for your forcing construction
