Deje $\mathcal{A}_i (i \in I)$ ser una familia de $L$-estructuras, $F \subseteq \mathcal{P}(I)$ un filtro y se denotan por $\mathcal{A}$ la reducción del producto de esta familia por $F$. Voy a indicar el dominio de $\mathcal{A}_i$ por $A_i$ y de manera similar para $\mathcal{A}$. Por otra parte, si $\alpha \in A$, entonces voy a indicar el $i$ coordenadas de un representante de $\alpha$ por $a_i$.
Ahora, no es un argumento habitual por inducción sobre la complejidad de las fórmulas que muestra que, si $\phi$ es positivo primitiva, entonces tenemos
$\mathcal{A} \models \phi$ fib $\{i \in I \; | \; \mathcal{A}_i \models \phi\} \in F$.
Lo que me preocupa aquí es acerca de la $\exists y \psi$ caso. En la prueba por inducción, por lo general, tener algo como:
$\mathcal{A} \models \exists y \psi$ fib no es $\alpha \in A$ tal que $\mathcal{A} \models \psi[\alpha]$ fib $\{ i \in I \; | \; \mathcal{A}_i \models \psi[a_i]\} \in F$, lo que implica que $\{i \in I \; | \; \mathcal{A}_i \models \exists y \psi\} \in F$.
De lo contrario, se suele proceder de la siguiente manera:
Supongamos $X = \{i \in I \; | \; \mathcal{A}_i \models \exists y \psi\}$ e $X \in F$. Necesitamos construir una secuencia $a$ tal que su correspondiente equivalencia de la clase $\alpha$ es tal que $\mathcal{A} \models \psi[\alpha]$. Así, para cada una de las $i \in X$, recogemos $a_i \in A_i$ tal que $\mathcal{A}_i \models \psi[a_i]$, lo cual se puede hacer la hipótesis. Pero si $j \not \in X$, entonces podemos elegir cualquier elemento de $A_j$. La prueba, a continuación, continúa como de costumbre.
Esta prueba de lo contrario paso claramente hace uso del axioma de elección. Mi pregunta es: ¿hay modelos de $\mathsf{ZF}$ en que esta conversar falla?