Predicate logic

$\forall x\, P(x)$ means "no matter what we plug in for $x$, $P$ holds" — so plugging in any specific term $t$ must still make $P(t)$ hold. This is the rule that turns general laws into concrete instances: from "$\forall x\, (\text{Human}(x) \to \text{Mortal}(x))$" we instantiate at $t = \text{Socrates}$ to get "$\text{Human}(\text{Socrates}) \to \text{Mortal}(\text{Socrates})$", the first premise of the classic syllogism.

We argue directly from Tarski's satisfaction semantics, which defines truth in a structure recursively on formula structure.

By the semantic clause for $\forall$: $\mathcal{M} \models_s \forall x\, P(x) \iff \text{for every } d \in M,\ \mathcal{M} \models_{s[x \mapsto d]} P(x)$. Assume the hypothesis $\mathcal{M} \models_s \forall x\, P(x)$; by this clause, $\mathcal{M} \models_{s[x \mapsto d]} P(x)$ holds for every $d \in M$, with no exception.

Since the claim holds for every $d \in M$, it holds in particular for $d = t^{\mathcal{M},s}$, the element that the term $t$ denotes in $\mathcal{M}$ under $s$. Substituting this specific $d$ gives $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$.

By the Substitution Lemma (a standard result relating variable assignment to term substitution, provable by induction on the structure of $P$): $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x) \iff \mathcal{M} \models_s P(t)$, valid precisely because $t$ is substitutable for $x$ in $P(x)$ (no free variable of $t$ becomes accidentally bound). Applying the lemma converts $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$ into $\mathcal{M} \models_s P(t)$.

Since $\mathcal{M}$, $s$, and $t$ were arbitrary, the inference from $\forall x\, P(x)$ to $P(t)$ preserves truth in every structure under every assignment: the rule is sound.

$\exists y\, \forall x\, R(x,y)$ demands a single witness $y$ that works for every $x$ (a "fixed" witness), while $\forall x\, \exists y\, R(x,y)$ only demands that each $x$ has some witness, possibly a different one for each $x$ (a "moving" witness). A fixed witness is automatically a moving witness (just reuse it), but not conversely — this is exactly the difference between "someone loves everybody" (one universal lover) and "everybody is loved by someone" (possibly different admirers), a classic source of ambiguity in natural language that predicate logic disambiguates.

Forward direction. Assume $\mathcal{M} \models_s \exists y\, \forall x\, R(x,y)$. By the semantic clause for $\exists$, $\mathcal{M} \models_s \exists y\, \varphi \iff \text{there is } d \in M \text{ with } \mathcal{M} \models_{s[y \mapsto d]} \varphi$; applying it here gives some $d_0 \in M$ with $\mathcal{M} \models_{s[y \mapsto d_0]} \forall x\, R(x,y)$.

By the clause for $\forall$ applied to this, $\mathcal{M} \models_{s[y \mapsto d_0][x \mapsto a]} R(x,y)$ holds for every $a \in M$, since the $\forall x$ ranges over all of $M$ regardless of which $a$ we later pick.

Now fix an arbitrary $a \in M$ to verify $\forall x\, \exists y\, R(x,y)$. From the previous paragraph, taking $x \mapsto a$ gives $\mathcal{M} \models_{s[y \mapsto d_0][x \mapsto a]} R(x,y)$, which exhibits $d_0$ itself as a witness for $\exists y\, R(x,y)$ under $x \mapsto a$; hence $\mathcal{M} \models_{s[x \mapsto a]} \exists y\, R(x,y)$.

Since $a \in M$ was arbitrary, $\mathcal{M} \models_{s[x \mapsto a]} \exists y\, R(x,y)$ holds for every $a$, which is exactly the semantic clause for $\mathcal{M} \models_s \forall x\, \exists y\, R(x,y)$. This proves $\exists y\, \forall x\, R(x,y) \Rightarrow \forall x\, \exists y\, R(x,y)$.

Converse fails: a counterexample. Let $\mathcal{M}$ have domain $M = \mathbb{Z}$ (the integers) and interpret $R(x,y)$ as "$x < y$". Then $\forall x\, \exists y\, R(x,y)$ is TRUE: for every integer $x$, taking $y = x+1$ gives $x < y$. But $\exists y\, \forall x\, R(x,y)$ is FALSE: it would require a single integer $y$ larger than every integer $x$, and no such maximum integer exists (for any candidate $y$, the integer $y+1$ violates $y+1 < y$). So $\forall x\, \exists y\, R(x,y)$ holds while $\exists y\, \forall x\, R(x,y)$ fails, showing the converse implication is false in general.