I am trying to prove Los theorem (the one for ultraproducts, the statement with a proof is here. https://proofwiki.org/wiki/Łoś%27s_Theorem), but using $\forall$ as primitive quantifier. Any proof online uses $\exists$ as primitive quantifier to do the induction step. Could someone please give a proof using $\forall$ instead of $\exists$ to prove it?
I know, the $\forall$ is just $\lnot \exists \lnot$, but now I am searching for a direct proof. I did not expect it to be hard (basically "by definition"). However, after tried manipulating the statement, I still cannot get it. Any help or reference would be appreciated, thank you!
First, if $$\{i\in I:\mathcal A_i \models \forall x\varphi(x)\} \in U$$ then for any $f,$ $$ \{i\in I:\mathcal A_i\models\varphi(f(i))\}\in U$$ (since the latter is a superset of the former) and hence by the IH, $ \forall [f]\in A,\mathcal A\models \varphi([f]).$
For the converse, assume that $$ \{i\in I:\mathcal A_i\models\forall x\varphi(x)\}\notin U,$$ so that $$ \{i\in I:\exists x\in A_i,\mathcal A_i\not\models\varphi(x)\}\in U.$$ Use choice to let $f(i)$ be a witness to the statement $"\exists x\in A_i,\mathcal A_i\not\models\varphi(x)"$ when it's satisfied. Then $$ \{i\in I : \mathcal A_i\not\models \varphi(f(i))\}\in U,$$ so $$ \{i\in I : \mathcal A_i\models \varphi(f(i))\}\notin U$$ and $$ \exists [f]\in A,\mathcal A\not\models \varphi([f])$$