5
$\begingroup$

Let $M$ be a ctm and $P\in M$ a forcing order.

In regular forcing extensions, we have the following well-known Principle: $$p\Vdash_{M,P}\exists x\phi[x]\;\Longrightarrow\;\exists\sigma\in M^P\;p\Vdash_{M,P}\phi[\sigma]$$ (where $M^P$ is the class of $P$-names in $M$).

Given an automorphism $f$ of $P$, we can turn $f$ into a function mapping $P$-names to $P$-names, given by $$\overline{f}(\tau)=\{(\overline{f}(\sigma),f(p))\;|\;(\sigma,p)\in\tau\}$$ Given a subgroup $H$ of $Aut(P)$, we say that $\tau$ is $H$-invariant iff $\overline{f}(\tau)=\tau$ for all $f\in H$.

We can also fix a filter $\mathcal{F}$ on the set of subgroups of $Aut(P)$ and consider the so-called $\mathcal{F}$-symmetric extension of $M$ given by the evaluation only of those names $\tau$ that are hereditarily $\mathcal{F}$-symmetric, i.e. for some $H\in \mathcal{F}$, $\tau$ is $H$-invariant and for all $(\sigma,p)\in\tau$, $\sigma$ is hereditarily $\mathcal{F}$-symmetric. It can be shown that the resulting model always satisfies ZF, but not always AC.

My question now is whether or not the following principle can be shown to hold (in $M$): Given $p\in P$ such that $p\Vdash_{M,P}^{\mathcal{F}}\exists x\phi[x]$ (i.e. for any $P$-generic filter $G$ containing $p$, there is a hereditarily $\mathcal{F}$-symmetric name $\tau$ such that $M[G]\models\phi[\tau]$), does there necessarily exist a hereditarily $\mathcal{F}$-symmetric name $\sigma$ such that $p\Vdash\phi[\sigma]$?

As far as i can tell, the proof for the usual case can not be modified to prove the symmetric case, since we "stitch together" witnesses along a maximal antichain, which might not be $H$-invariant for any $H\in\mathcal{F}$.

$\endgroup$

1 Answer 1

4
$\begingroup$

No. Not even remotely.

Consider the Cohen model, i.e. add $\omega$ Cohen reals, permute them amongst themselves, and take finite supports. Let $\dot a_n$ be the canonical name of a Cohen real, and let $\dot A$ be the name of the set of Cohen reals.

$$1\Vdash\exists x(x\in\dot A\land\check 0\in x)$$

But there is no symmetric name that we can instantiate. If $\dot x$ would be such name, then it is easy to see that its value has to be one of finitely many reals, but then just take a condition which decides that $\check 0\notin\dot a_n$ for any of those finitely many reals.

$\endgroup$
2
  • 1
    $\begingroup$ My work on symmetric iterations deals with this problem extensively. See "Iterations of symmetric extensions", J. Symb. Log. 84 (2019) no. 1, pp. 123–159. Or, arxiv.org/abs/1606.06718 $\endgroup$
    – Asaf Karagila
    Jun 21, 2020 at 11:21
  • $\begingroup$ (I also mention this issue in several other papers dealing with iterations.) $\endgroup$
    – Asaf Karagila
    Jun 21, 2020 at 11:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.