Maximality principle in symmetric extensions

Question

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}$.

Answer 1

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.