Partial answer. There is a $V\models ZFA$ containing a generically presentable cardinal $(\nu,\mathbb{P})$ such that for all $a\in V$ we have $\Vdash_{\mathbb{P}^2}\nu[G_0]\not\equiv\check{a}.$ This should be equivalent to your first condition, assuming the first condition can even be stated i.e. the ground model is definable in the ZFA setting.

I am not sure about ZF models. (But I *don’t* see a reason why Pincus’ transfer theorems *don’t* apply, using the “surjectively boundable” condition for example. I think we only need to consider $a$ that don’t admit a surjection to $\omega_1,$ because the below model should give $\Vdash_{\mathbb{P}^2}\text{there is no surjection }\nu[G_0]\to\omega_1.$ And the forcing relation should be equivalent to some fairly tame sentence, surely?)
$
\DeclareMathOperator{dom}{dom}
\DeclareMathOperator{rng}{rng}
\DeclareMathOperator{supp}{supp}
$

Take $V$ to be the basic Fraenkel model, with set of atoms $A.$ Every set $x\in V$ has a minimal finite support $\supp(x)\subset A.$ So $x$ is fixed by permutations that fix each element of $\supp(x).$

Conditions $p\in \mathbb P$ are bijections such that $\dom p$ and $\rng p$ are disjoint finite subsets of $A.$ Graphically, imagine a finite set of vertex-disjoint directed edges using the vertex set $A.$ As usual $p\leq q$ if $p\supseteq q.$

Take $\nu$ to be the name for $\dom \bigcup G.$

I’ll make use of the dense subset $\mathbb Q\subset \mathbb P^2$ consisting of pairs $p=(p_0,p_1)$ such that $\dom p_0 \cup \rng p_0 = \dom p_1 \cup \rng p_1.$ Graphically, these conditions are a finite union of cycles (possibly 2-cycles) using the vertex set $A.$ In each cycle edges are alternately colored $0$ and $1,$ and every edge has a direction. (Note these aren’t “directed cycles”, just cycles with directed edges - the direction on different edges are unrelated.)

The interesting part is that these cycles have no orientation-reversing symmetry. Graphically, a reflection of a regular polygon would have to pass through the midpoint of an edge, which is ruled out by the directions, or pass through a vertex, which is ruled out by the coloring. Pick an isomorphism-invariant choice function for orientations of alternating-colored cycles with directed edges. This is kosher because we can define these using only pure sets, and in fact this is completely finitary. This gives a bijection $\nu[G_0]\to \nu[G_1]$ by identifying each set with edges of the appropriate color, and sending each edge in a cycle one step along the chosen orientation.

The rest of the argument is just the usual trick of making use of compatible conditions related by symmetries. Suppose for contradiction that there exists $z\in V$ and $p\in\mathbb Q$ and a $\mathbb Q$-name $\dot{f}$ such that $$p\Vdash\text{$\dot{f}$ is a bijection $\check{z} \to \nu[G_0]$}$$
where $\Vdash=\Vdash_{\mathbb Q}.$
By refining $p$ if necessary we can assume that the supports of $z$ and $\dot{f}$ are contained in $A_0:=\dom p\cup \rng p.$ There exists $q\leq p$ and elements $x_a\in z$ for $a\in A_0$ such that $q\Vdash \bigwedge_{a\in A_0}\dot{f}(\check{x_a})=\check{a}.$ Consider a permutation $\pi$ fixing $A_0$ but moving every other atom used by $q,$ and every $x_a,$ to unused atoms. Then $q$ and $\pi q$ are compatible, which shows that $\supp(\check{x_a})\subseteq A_0,$ so the choice of $q$ was irrelevant:

$$p\Vdash \bigwedge_{a\in A_0}\dot{f}(\check{x_a})=\check{a}.$$

Pick an element $x\in z\setminus \{x_a:a\in A_0\}.$ Pick $r\leq p$ such that each element of $\supp(x)\setminus A_0$ is in a distinct 2-cycle of $r.$ Let $A_1$ be the set of elements of cycles in $r$ that use an element of $\supp(x)\setminus A_0.$ Refine $r$ if necessary such that: for all $y=\pi x$ where $\pi$ fixes $A_0$ and $\supp y\subseteq A_1,$ there exists $a_y\in A$ with $$r\Vdash \dot{f}(\check y)=\check{a_y}$$

For each such $a=a_y$ we have $a\not\in A_0.$ Suppose for contradiction that $a\not\in A_1.$ Pick $\pi$ fixing $A_0\cup A_1$ but sending all other atoms used by cycles in $r$ to unused atoms, and such that $a\neq \pi a.$ Then $\pi r$ and $r$ are compatible, which gives the contradiction $r\cup \pi r\Vdash \check a=\pi \check a.$ So $a\in A_1.$

Each $a_y$ lies in the set $\dom r_0\cap A_1$ of order $|A_1|/2,$ but there are at least $\binom{|A_1|}{|A_1|/2}> |A_1|/2$ choices of $y$ (with $\binom{0}{0}=1>0$) because sets with distinct supports are distinct.

I think this all generalizes to $\kappa$-closed conditions, using a generalization of the basic Fraenkel model to supports of order $<\kappa.$ However, the cycles can then be infinite, so the choice function for orientations now seems to genuinely need choice, for pairs of countable sets of reals.

haveto force back the axiom of choice? No, you don'thaveto force it back. $\endgroup$3more comments