I'm working through Martin Goldstern's "Tools for Your Forcing Construction" and am confused about definition 5.11.
First some notation:
- $\mathbf C\subseteq{}^\omega\omega$ is some closed set,
- $\langle{\sqsubset_n}\mid n\in\omega\rangle$ is a sequence of binary relations on ${}^\omega\omega$
- ${\sqsubset}=\bigcup_{n\in\omega}{\sqsubset_n}$, which is therefore also a relation on ${}^\omega\omega$
We furthermore assume that each of the above sets can be defined by some nice enough formula. Given some model $\mathcal N$, we say that $g\in{}^\omega\omega$ covers $\mathcal N$ if for all $f\in\mathbf C\cap\mathcal N$ we have $f\sqsubset g$. Given some chain of conditions $\langle p_n\mid n\in\omega\rangle\in{}^\omega\Bbb Q$, a tuple of $\Bbb Q$-names for reals $(\dot f_0,\dots,\dot f_k)$ and a tuple of reals $(f_0^*,\dots,f_k^*)$, we say that $\langle p_n\mid n\in\omega\rangle$ interprets $(\dot f_0,\dots,\dot f_k)$ as $(f_0^*,\dots,f_k^*)$ if for each $i\leq k$ and all $n$ we have $p_n\Vdash \dot f_i\restriction n=f_i^*\restriction n$. We let $\chi$ be a large ordinal such that everything relevant to us happens in the hereditary universe $\mathbf H(\chi)$.
My confusion is about the role of $x$ in following definition:
Definition 5.11. We say that a forcing $\mathbb Q$ preserves $\sqsubset$ if for some $x$ (called the "witness") and all countable elementary submodels $\mathcal N\prec\mathbf H(\chi)$ with each of $\mathbb Q,x,\sqsubset$ in $\mathcal N$ for which there is $g$ that covers $\mathcal N$ and for any chain of conditions $\langle p_n\mid n\in\omega\rangle\in\mathbb {}^\omega \Bbb Q\cap\mathcal N$ interpreting $(\dot f_0,\dots,\dot f_k)$ as $(f^*_0,\dots,f^*_k)$ where each $f^*_i\sqsubset_{n_i} g$, there exists an $\mathcal N$-generic condition $q$ stronger than $p$ [sic] such that "$q\Vdash g\text{ covers }\mathcal N[G]$" and for each $i\leq k$ we have $q\Vdash \dot f_i\sqsubset_{n_i}g$.
(I believe that where it says "$q$ is stronger than $p$", it should say "$q$ is stronger than $p_0$")
The witness $x$ does not seem to be used in a meaningful way anywhere in the paper after this, and I'm not aware of its role in any other preservation results I have seen. It clearly puts a limit on which models $\mathcal N$ we want to consider, but I'm not seeing how this is used in practice. If we simply set $x$ to be something absolute, like $\varnothing$, then it does not really harm the definition either.
Furthermore, such a witness is absent in the definition of "almost preserving" (definition 5.5). Because of this, I'm not sure how to conclude that "preserving" implies "almost preserving".
First, you're right, $p$ should be $p_0$.
Regarding the witness $x$, if you look back at Goldstern's treatment of properness (definition 3.7), there's a similar thing going on:
As Goldstern himself observes (remark 3.8), the clause "for some $x$" isn't necessary, it's just there to simplify the exposition. This is essentially a crux to get away with not introducing clubs of elementary submodels. The definition of properness can be annoying to work with if you require "for every countable elementary submodel", whereas making sure the models you start with contain a few convenient parameters will make the proof smoother. Of course, one can prove that if $P$ is proper for a club of elementary submodels, then it is proper for every elementary submodel $N$ with $P\in N$.
I believe the role of $x$ in 5.11 is essentially the same, and it might be the case that this is never used afterwards (I don't remember the paper in that level of detail), but it's there so as to simplify the treatment, should that be necessary. I don't immediately see how to show that the definition doesn't really need the witness. I'll update if I do), but, if only for peace of mind, you might want to add the witness clause to the definition of "almost preserves", or remove the witness from the definition of "preserves". The latter is the approach taken by Bartoszynski and Judah in Set Theory: on the structure of the real line, page 274, which in turn follow Repicky.
Okay, here's how to bypass the witness in showing that "preserving" implies "almost preserving". We'll show that, with some flexibility on the parameter $\chi$ (I'll use $\theta$ instead for aesthetic reasons), the witness in the definition of "preserves" can be dropped.
Suppose $Q$ preserves $\sqsubset$. Let $\theta$ be the least regular cardinal witnessing the definition of "preserves". Take $\theta^*$ regular and much larger than $\theta$ (something like $(2^\theta)^+$ probably works, but we can follow Goldstern and take $\theta^*=(\beth_\omega(\theta))^+$ to be safe). Note that $\theta$ is definable in $(H(\theta^*),\in)$.
Fix $N^*\prec H(\theta^*)$ countable with $\{Q,\mathbf C\}\subseteq N^*$ and fix $p\in N$. By assumption,
$$ \exists x\in H(\theta)\forall M\prec H(\theta)[(|M|=\aleph_0\wedge x\in M)\to \forall p\in M\cap Q\exists q\le p \text{ (b),(c), and (d) hold}] $$ where (b),(c),(d) refer to definition 5.11 (or see below). Now, this is a statement which holds in $H(\theta^*)$, and moreover all the parameters belong to $N^*$. By elementarity, we can find a witness $x\in H(\theta)\cap N^*$. Put $N:=H(\theta)\cap N^*$. By general facts, $N\prec H(\theta)$, so the choice of $x$ says that there is some $q\le p$ such that
(b) $q$ is $(N,Q)$-generic.
(c) $q\Vdash \forall f\in N[\dot G]f\sqsubset g$
(d) $\forall i<k (q\Vdash \dot f_i\sqsubset_{n_i}g)$
(I'm using dots for names instead of Goldstern's under tildes because I don't know how to typeset those, plus I like dots better).
I claim (b), (c), and (d) all hold with $N$ replaced by $N^*$. For (b), note that $Q\cap N=Q\cap N^*$, so being $(N,Q)$-generic is the same as being $(N^*,Q)$-generic. For (c), note that any real in $N^*$ must be in $N$, because $\omega^\omega\subseteq H(\aleph_1)$.