I understand that questions about intuition are usually frowned upon, but I'd really appreciate it if someone could verify (or extend) my intuition about the definition of the forcing relationship.
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') \} $$ is dense below $p$, and vice versa with $x_0$ and $x_1$ swapped symmetrically).
I understand this to mean the following: a condition $p$ forces equality if we can always find an extension $q \leq p$ that, for any element of the first name in question, can find a name in the second name in question, so that $q$ forces equality between those elements. So, effectively, the relation ensures that the interpretations of both names w.r.t. some M-generic filter have the same elements, which would indeed force equality.
Now, this is where my intuition ends. I don't understand what the denseness of sets of conditions has to do with this (although it is clearly crucial). I think understand why this is done recursively (it almost looks like a game where each element of each name checks whether it's realised, and then the respective other name must come up with an element for which conditions force equality; if one name fails to come up with such a name, their interpretations can't be equal).
Apologies if this last paragraph didn't quite make sense, but I am struggling to isoloate what I don't understand. If my comments above are insufficient, please let me know and I'll try and rephrase my lack of understanding.
Best Answer
At first pass, it's best to approach the recursive approach to forcing as secondary: namely, it's an alternate (and extremely useful) characterization of the purely semantic definition of forcing.
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.
This is actually something we need to amend later on when we talk about forcing over ill-founded models, but ignore that for now.
The forcing notion $\Vdash_\mathbb{P}$ is then defined as follows:
(or more precisely $M[G]\models\varphi[G]$, where $\varphi[G]$ is the result of replacing each name occurring in $\varphi$ with its evaluation at $G$).
This definition is quite straightforward and well-motivated, and some of its basic properties are easy to check (e.g. $p\Vdash\varphi\vee\psi$ iff for each $q\le p$ there is an $r\le q$ such that either $r\Vdash\varphi$ or $r\Vdash\psi$). However, beyond that it's also horrible to work with, the key issue being that it is not obviously definable within $M$. For forcing to be useful we'll need at a bare minimum that for each sentence $\varphi$ of the forcing language in $M$ the set $\{p\in\mathbb{P}: p\Vdash\varphi\}$ is a set in $M$, and the definition above doesn't suggest that that's the case at all.
This is where the recursive approach to forcing comes in. We're going to sit down and think carefully about the definition of $\Vdash$ with the hope that we can whip up a concrete characterization of it (and indeed we'll be successful). Unsurprisingly there are two fundamental recursions going on here: we have to break high-complexity sentences into lower-complexity sentences, and we have to break high-complexity names into lower-complexity names. The former is much easier, with the somewhat unusual result that pinning down the atomic cases (= equality and elementhood) is much more complicated than going from simple sentences to complicated sentences (= handling Booleans and quantification).
For example, let's look at the case of equality. We have:
$p\Vdash\mu=\nu$ iff for all $G\ni p$ generic we have $\mu[G]=\nu[G]$.
... which holds iff for each $G\ni p$ generic and $\langle q,\delta\rangle\in \mu$ there is some $\langle r,\eta\rangle\in \nu$ such that $$q\in G\implies r\in G\wedge \delta[G]=\eta[G],$$ with the "$q\in G\implies$" bit here addressing the fact that if $q\not\in G$ then the pair $\langle q,\delta\rangle$ doesn't get "triggered" and so we don't care what it does (and identically with $\mu$ and $\nu$ 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\mu=\nu$ is just saying that for every $\langle q,\delta\rangle\in \mu$ the situation above is unavoidable by generic filters containing $p$ (and identically with $\mu$ and $\nu$ flipped).
Specifically, suppose $r\le p$ and $r\le q$ (so $r$ is something that $p$ so far doesn't rule out and also "triggers $\delta$ in $\mu$"). Then we want there to be some $s\le r$ and some $\langle t,\eta\rangle\in\nu$ such that $s\le t$ (that is, $s$ "triggers $\eta$ in $\nu$") and $s\Vdash\delta=\eta$ (and identically with $\mu$ and $\nu$ flipped).
Rephrasing this a bit more snappily, we get the characterization in the OP. This might appear circular at first glance since we've used forcing equality inside the definition of forcing equality, but it's a perfectly valid recursion since we keep going down in rank (the $\delta$s and $\eta$s we look at are coordinates of ordered pairs which are themselves elements of $\mu$ and $\nu$ respectively). The point is that this characterization is obviously expressible in $M$, and it's not hard to prove (externally to $M$) that it in fact coincides with the semantic definition.
Hopefully this indicates how the messy-looking recursive definition of forcing inside $M$ emerges from natural considerations. It's a good idea at this point to similarly whip up a definition of the forcing relation for elementhood; it will go very similarly. (Actually the presentation I learned from treated equality and elementhood by simultaneous recursion; that's also a fine option.)