\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{$\$}} %% -- 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){\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){\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 {\} \def\ffk{\ff {*} {k-1} } \def\nffk{\nff {} {k-1} } \def\pffk{\} \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{$\$}} \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 $\$, 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 $\$, 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 $\$, 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 = \$ 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 $\$ 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 $\$ such that $p\in P$ and $p\Forces_{ Q}``$\nq\in \nQ$''$. We let $\ \weaker_{P*\name 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 $\$, 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:= \{ \ \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\, \\in J\}$ is generic for $P$ over $V$, $H:= \{\nq[G]: \exists p\in G, \\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 := \$ is an $I$-supported iteration iff for all $\alpha<\varepsilon$, \itemitem{} $P_\alpha = \limi \$, 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\$ 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 $\$, we automatically define $P_\varepsilon$ to be the $I$-supported limit of this iteration. This allows us to avoid the more awkward notation $\$. \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 $\\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\$ is isomorphic to $P_\alpha * \nQ_\alpha$, via the map that sends $p\in P_{\alpha+1}$ to $\$. \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 = \$ 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 $\ $ 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 $\$ 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 $\$ is a family of finite sets. Then there is a set $S \subseteq \omega_1$ of size $\aleph_1$ such that the family $\$ 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 $\$. \ENDPROCLAIM See [\Kunen, II.1.5] for a proof. {\bf Proof of \cccPres/, limit step: } Assume (toward a contradiction) that $\$ 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 $\$ 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 $\$ 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 $\$ of sets in $H(\chi)$ such that for all $i\le {\lambda}$ $x_i \subseteq \{x_j:j$. 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 $\$ from $P_\varepsilon$ (in $N$), but the above definition makes it unnecessary, as we can include ``$\\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 $\$ 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 $\$ 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:=\$ 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 $\ $ 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 \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 $\$ 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 $\$ 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) = \$$ 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 $\\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 $\ \weaker \ \weaker \ \weaker \ \weaker \$. %\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 $\$ 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 $\$ 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) $ 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)$. (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)$. \ENDPROCLAIM We say that $\sqn p$ interprets $\bnffk $ as $\bffk$, if for all $i$ 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 $\$ 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$ 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 $\$, 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\in \erp{Q_1}^\omega $ and functions $f'_i$ for $i$ 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$. 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) = \$ 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 $\$ 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 = \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 $\$ 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$ 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^*$, $\$ 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$} $\$ 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\in \erp Q_\alpha^\omega$ is inconsistent''} \leqno(2)_0$$ {\bf [%] }Proof of first claim: It is enough to find a sequence $\$ 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 $\$ 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 $\ $ 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}: 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 = \<\nf_i:i$. \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}} \$ 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$ from the given sequences $\sqn {\np^{j}}$, $\<\nf^{j}_i:i$ 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 $\$ (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$, $\<\nf^j_i:i$ 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 $ 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$. \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:=\$ 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$ be defined by $f \re_n g \liff \forall k\ge n: f(k)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:=\$ 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 $\$ 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)$ and $\$ 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 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$, $\\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 $\$, $\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$ interpret $\bnffk$ as $\bsffk$, and assume $f_i^* \Rout _{n_i} g$. Let $n^*:= \max\{n_i:i$, 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\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$ 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 $\$ of finite subsets of $\omega$ with $|A_n| \le 2^n$ (i.e., a $1$-cone). We say that $\bar A = \$ ``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 r0$ $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 i0$ we can find a condition $p'_n \ge p_n$ such that for all $i0 \,\,\nf_i(m) \subseteq F_{n,i}(m)$$ We can find these sequences $\ $ and $\$ in~$N$. Now define for $i0$ 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 $in$. \ite ii For all $im _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 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)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 $ 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 $\ $ 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 \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 $\$ 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)