Now includes edits to the question to correct for the mistake in Equation (3), as identified by vsotvep
Could I ask a question relating to the last step in the elegant answer to What does the Forcing relation mean semantically? - see summary of the previous posting below between the horizontal lines (with slightly changed notation only and my introduction of Equation (2)), with my question posed afterwards:
"In particular, the case $p \Vdash x_0 = x_1$ appears tricky to me. The definition states the following (I am assuming that $M$ is a countable transitive model of ZFC); suppose $x$ is a $\mathbb{P}$-name for some forcing notion $\mathbb{P}$ if it comprises ordered pairs where the first cooridnate is another $\mathbb{P}$-name, and the second coordinate is a condition. I follows the standard convention that $p \leq q$ means $p$ is stronger than $q$.
Suppose $\mathbb{P} \in M$ is a forcing notion in some countable transitive model of ZFC. Suppose $p \in \mathbb{P}$ is a condition, and $x_0$ and $x_1$ are $\mathbb{P}$-names. We say $p \Vdash x_0 = x_1$ if the following holds: for any $\langle y,s \rangle \in x_0$ the set $$ \{ q \leq p \mid q \leq s \rightarrow \exists\langle y',s'\rangle \in x_1 (q \leq s' \land q \Vdash y=y') \} \tag{1}$$ is dense below $p$, and vice versa with $x_0$ and $x_1$ swapped symmetrically)."
The relevant bits of the answer include :
Suppose $M$ is a c.t.m., $\mathbb{P}\in M$ is a forcing notion, and $G$ is $\mathbb{P}$-generic over $M$. We can as usual define the generic extension $M[G]$ - note that this does not involve any appeal to the forcing notion itself, it's simply a direct recursive construction.
The forcing notion $\Vdash_\mathbb{P}$ is then defined as follows:
For $p\in\mathbb{P}$ and $\varphi$ a sentence in the forcing language we write $p\Vdash\varphi$ iff for all $G$ which are $\mathbb{P}$-generic over $M$ we have $$p\in G\implies M[G]\models\varphi[G]$$
where $\varphi[G]$ is the result of replacing each name occurring in $\varphi$ with its evaluation at $G$)
For example, let's look at the case of equality. We have:
$p\Vdash x_0= x_1$ iff for all $G\ni p$ generic we have $x_0[G]=x_1[G]$.
... which holds iff for each $G\ni p$ generic and $\langle y,s\rangle\in x_0$ then
$$s\in G\implies \exists \langle y',s'\rangle\in x_1 (s'\in G\wedge y[G]=y'[G]),$$ or equivalently :
$$\forall G\ni p [s\in G\implies \exists \langle y',s'\rangle\in x_1 (s'\in G\wedge y[G]=y'[G])]\tag{2}$$
with the "$s\in G\implies$" bit here addressing the fact that if $s\not\in G$ then the pair $\langle y,s\rangle$ doesn't get "triggered" and so we don't care what it does (and identically with $x_0$ and $x_1$ flipped).....
OK, now let's start to peel away the reference to $G$ in the above, shooting instead for a characterization in terms of individual conditions and dense sets. $p\Vdash x_0=x_1$ is just saying that for every $\langle y,s\rangle\in x_0$ the situation above is unavoidable by generic filters containing $p$ (and identically with $x_0$ and $x_1$ flipped).
Specifically, suppose $q\le p$ and $q\le s$ (so $q$ is something that $p$ so far doesn't rule out and also "triggers $y$ in $x_0$"). Then we want there to be some q and some $\langle y',s'\rangle\in x_1$ such that $q\le s'$ (that is, $q$ "triggers $y'$ in $x_1$") and $q\Vdash y=y'$ (and identically with $x_0$ and $x_1$ flipped).
My questions is :
Why is Equation (2) logically equivalent to Equation (1) - for example it doesn't look like it is because the conversion from Equation (2) to Equation (1) appears to 'roughly' require $\forall G\ni q \exists\langle y',s'\rangle \in x_1 $ to be converted to $ \exists\langle y',s'\rangle \in x_1 \forall G\ni q $ which are not logically equivalent. To elaborate:
Suppose the G are labelled by each of the elements q in $\mathbb{P}$ then with $\boldsymbol{G(q)=\{G:q \in G\}}$ -
$$\{G\} \Leftrightarrow \boldsymbol{\bigcup \{G(q) : q \in \mathbb{P} \}}$$
The idea being to split all the G into collections having q $\in$ G (i.e. G(q)), for each $q \in \mathbb{P}$ so that a test "for all G" is the same as a "test for all $q \in \mathbb{P}$" and "test for all G in G(q)" . This means as $\forall G \in G(q) \Leftrightarrow \forall G \ni q $ that :
$$\forall G \ \ \Leftrightarrow \ \ (\forall q\in \mathbb{P} \; \forall G \in G(q)) \ \ \Leftrightarrow \ \ (\forall q\in \mathbb{P} \; \forall G \ni q) $$
and as by definition $\forall G \ni p(X) \Leftrightarrow \forall G (p \in G \implies X)$ so :
$$\forall G \ni p (X) \ \ \Leftrightarrow \ \ \forall G (p\in G \implies X) \ \ \Leftrightarrow \ \ \forall q\in \mathbb{P} \; \forall G \ni q (p\in G \implies X) \tag{3}$$
Then Equation (2) would be equivalent to, by inserting (3) into (2) :
$$\forall q\in \mathbb{P} \; \forall G \ni q (p \in G \implies [s\in G\implies \exists \langle y',s'\rangle\in x_1 (s'\in G\wedge y[G]=y'[G])])\tag{4}$$
To get Equation (4) to look anything like Equation (1) would require the $\forall G \ni q$ to be moved into the RHS of the expression (ie 'illegally' through the $\exists$ symbol) :
$$\forall q\in \mathbb{P} \; (p \in G \implies [s\in G\implies \exists \langle y',s'\rangle\in x_1 (s'\in G\wedge \boldsymbol{\forall G \ni q (y[G]=y'[G])})])\tag{5}$$
since this would be the same as :
$$\forall q\in \mathbb{P} \; (p \in G \implies [s\in G\implies \exists \langle y',s'\rangle\in x_1 (s'\in G\wedge \boldsymbol{q \Vdash y=y')}])\tag{6}$$
To get to this point required an illegal conversion of $\forall \exists$ to $\exists \forall$ (presumably to get $q \leq s'$ etc would require other information to be used, but I got stuck at this point). Indeed suppose Equation (4) does not have a single $\langle y',s'\rangle\in x_1$ for which $q \Vdash y=y'$. However despite this, for example, there may be half of the set {$G \; :\; q\in G$} having $\langle y',s'\rangle\in x_1$ with y[G]=y'[G], but the other half having a different $\langle y'',s''\rangle\in x_1$ with y[G]=y''[G], even though its false that $q \Vdash y=y'$. So some solutions may be missed, or an incorrect solution produced?
Any help in sorting out what I have missed will be much appreciated.
I usually like to mark all $\Bbb P$-names with a dot ($\dot x$) to keep it clear that these are names, and I like to write the interpretation of a name $\dot x$ by some generic $G$ as $\dot x_G$.
Now, your question mentions two definitions of the forcing relation $\Vdash$:
I believe your question asks why $\Vdash_O$ and $\Vdash_I$ are equivalent. The main theorem we need, is the following:
Note that this theorem only talks about a certain fixed $G$, and does not quantify over all generic filters $G$, so we have not yet reached the outside definition of the forcing relation. However, to prove the Forcing Theorem, you will not need to quantify over the generic filters. Unless I'm mistaken, this should solve your problem of "illegal conversion from $\forall\exists$ to $\exists\forall$".
The proof of the Forcing Theorem is mostly technical, but it is important to note that it is proved by induction in the same way that the inside definition is defined by recursion. In particular, one assumes that the theorem has been proved for all formulas $\psi$ of lower complexity than $\phi$ and all names $\dot y$ with rank strictly below $\max\{\mathrm{rk}(\dot x^k)\mid 1\leq k\leq n\}$. The base case of the induction with regard to the complexity of $\phi$ occur when we consider the atomic formulas $\dot x=\dot x'$ and $\dot x\in \dot x'$, and in turn the base case with regard to the rank of the names occurs when each name is the empty name.
For more details, I recommend to take a look in the literature. In particular Kunen's Set Theory is a standard reference, but there are many other books that go through the details (e.g. Schindler's Set Theory, Halbeisen's Combinatorial Set Theory)
We can use the Forcing Theorem to prove that $p\Vdash_O\phi(\dot x^1,\dots,\dot x^n)$ is equivalent to $p\Vdash_I\phi(\dot x^1,\dots,\dot x^n)$, assuming that we know that the model $\mathcal M\vDash\mathsf{ZFC}$ exists (in fact, for practical purposes we only need a large enough finite fragment of $\mathsf{ZFC}$, which solves problems regarding Gödel's incompleteness, see also Kunen's book), $\Bbb P\in \mathcal M$ and that for every $p\in \Bbb P$ there exists some filter $G\subset \Bbb P$ (outside of $\mathcal M$) that contains $p$ and that intersects all dense subsets of $\Bbb P$ contained in $\mathcal M$. These assumptions are necessary for the outside definition to be made at all, and hence we are working in universe $\bf V\ni\mathcal M$ that is large enough to contain sufficiently many $G$ that are $\Bbb P$-generic over $\mathcal M$.
Proof.
($\Vdash_I$ implies $\Vdash_O$)
If $p\Vdash_I\phi(\dot x^1,\dots,\dot x^n)$ and $p\in G$, then the Forcing Theorem tells us that $\mathcal M[G]\vDash \phi(\dot x^1_G,\dots,\dot x^n_G)$. This holds for any $G$ with $p\in G$, so it follows that $p\Vdash_O\phi(\dot x^1,\dots,\dot x^n)$.
($\Vdash_O$ implies $\Vdash_I$)
If $p\Vdash_O\phi(\dot x^1,\dots,\dot x^n)$, let's assume that $p\not\Vdash_I\phi(\dot x^1,\dots,\dot x^n)$. Then the set of conditions $\{q\leq p\mid q\Vdash_I\phi(\dot x^1,\dots,\dot x^n)\}$ is not dense below $p$, so we can fix some $q\leq p$ for which $r\not\Vdash_I\phi(\dot x^1,\dots,\dot x^n)$ for all $r\leq q$. But then $q\Vdash_I\lnot \phi(\dot x^1,\dots,\dot x^n)$. As we've already seen above, this implies $q\Vdash_O\lnot \phi(\dot x^1,\dots,\dot x^n)$. Now let $G$ be a generic filter with $q\in G$, then also $p\in G$ since $q\leq p$. But, using the definition of $\Vdash_O$, we now see that:
Hence we have reached a contradiction.