Determining $\forall x \exists y \varphi (x,y) \to \forall y \exists x \varphi (x,y)$ is valid I have the following formula, in an unspecified language:
$\forall x \exists y \varphi (x,y) \to \forall y \exists x \varphi (x,y)$
where $\varphi(x,y)$ is a formula containing free variables $x$ and $y$, presumably in that order.
So I want to show whether or not this is a valid formula, ie I want to show whether or not
$\vDash \forall x \exists y \varphi (x,y) \to \forall y \exists x \varphi (x,y)$
which is the case iff $\mathcal{S}, v \vDash \forall x \exists y \varphi (x,y) \to \forall y \exists x \varphi (x,y)$, for every structure $\mathcal{S}$ and for every variable assignment $v$
iff $\mathcal{S}, v \nvDash \forall x \exists y \varphi (x,y)$ or $\mathcal{S}, v \vDash \forall y \exists x \varphi (x,y)$, or both, for every structure $\mathcal{S}$ and for every variable assignment $v$ etc
But trying to follow through with this process systematically by describing all the variants of variable assignments and such leaves me with a lot of moving parts but not really much clarity.
My instinct is that the formula is not valid, and to show it as follows:
Consider $\mathcal{N}$, the structure of natural numbers, and let $\varphi(x,y) \equiv x<y$
Then indeed for every $x$ there is $y$ such that $x<y$, but it is not the case that for every $y$ there is $x$ such that $x<y$, as the natural numbers have a minimum value for which this does not hold. So the formula isn't true in at least one structure.
Does this suffice? Or is there a neater, more formal method I should be using? And what about a formula that is valid, where I wouldn't be able to hunt for a counter-example?
Any help appreciated, thank you
 A: Your counterexample is good. The only thing I would add to it is that you should first specify the language over which you are considering your structure $\mathscr N$; "the structure of natural numbers" is not the same when regarded as a structure in the laguage of posets (i.e. $\mathscr L = \{<\}$) and when regarded as a structure in the (first-order) language of Peano arithmetic (i.e. $\mathscr L = \{+, \cdot, s; 0 \})$.
With regards to looking for a method to prove validity of a formula (sentence in fact, i.e. no free variables), you should again specify over which language you are considering your formulas and structures, since otherwise the question doesn't make much sense. To illustrate this, consider the languages $\mathscr L = \varnothing$ (the pure language of equality) and $\mathscr L' = \{c\}$, where $c$ is a constant symbol. By definition of $\mathscr L'$-structure, every $\mathscr L'$ structure $\mathscr M'$ must interpret the constant symbol as an element in the universe of $\mathscr M'$, so in particular we have that for all $\mathscr L'$-structures $\mathscr M'$,  $\mathscr M' \models \exists x (x=c)$, so the $\mathscr L'$-sentence $\exists x (x=c)$ is valid (in all $\mathscr L'$-structures). However, since $c \notin \mathscr L$, an $\mathscr L$-structure $\mathscr M$ doesn't know how to interpret $c$, so asking if $\mathscr M \models \exists x (x=c)$ is not a well defined statement. If this last argument doesn't convince you, just note that the empty $\mathscr L$-structure doesn't have any elements in its universe, so in particular an existential sentence cannot be true in it.
Having said this, if you fix a language $\mathscr L$ and you want to show that some $\mathscr L$-sentence $\phi$ is valid, you could argue by contradiction; you assume that there is some $\mathscr L$-structure $\mathscr N$ which doesn't satisfy $\phi$, and hence (assuming that you're not working in intuitionistic logic, so that you can make use of the law of excluded middle) $\mathscr N \models \neg \phi$. Then you can try to exploit the fact that you know what language you are working with to see if the latter statement implies a contradiction to some sentence which you already know  is true in all $\mathscr L$-structures.
A: Regarding the question "what method should I use to prove the validity of a formula I suspect is valid?", probably the most accurate answer is that there is no one method or algorithm that will always work. This question is similar to "what method should I use to prove a theorem I suspect is true?"
But in terms of general strategies, your best bet is to first forget all about structures and variable assignments, and meditate for a while on what the formula expressing in words. There will usually be little to gain by trying to systematically analyze all structures and variable assignments. As you said, there is not much clarity there.$^{1}$ This is also not really the point since, although the definition of first-order satisfaction involves structures and variable assignments, the purpose of the definition is to rigorously capture a notion of "truth" that should be fairly intuitive (especially in introductory examples). So that's why it's good to first think about what the formula is really saying, and whether it sounds valid.
In your example, we have a binary relation $\varphi(x,y)$, and the formula is saying "If every $x$ is related to some $y$ in $\varphi(x,y)$, then every $y$ is related to some $x$ in $\varphi(x,y)$." So this just sounds false. For example, it would imply that every function is surjective (thinking of $\varphi(x,y)$ as potentially the graph of a function). So now that we've done this "informal" analysis, we can come up with an example and write it down carefully as a structure and a truth assignment.
But let's look at an example that's actually valid. Here's a classic
$$
\exists x\forall y\varphi(x,y)\rightarrow \forall y\exists x \varphi(x,y)
$$
Before diving into structures and variable assignments, we should parse the meaning of this formula. It says "if there is an $x$ that is related to every $y$ by $\varphi(x,y)$, then for every $y$ there is an $x$ that is related to $y$ by $\varphi(x,y)$". So this sounds true. So how should we prove it? Again, before getting into the nitty-gritty, it's often a good idea to sketch a less formal proof. To show this formula is valid I want to first assume there is an $x$ such that for all $y$, $\varphi(x,y)$ holds. Then I want to show that for every $y$ there is an $x$ such that $\varphi(x,y)$ holds. Of course, given a $y$, the $x$ I should pick is the same $x$ that I get in my initial assumption. Now we can translate this into a formal proof with structures and truth assignments (notation may vary beyond this point).
Suppose I have $(S,v)$ such that $(S,v)\models \exists x \forall y \varphi(x,y)$. Then there is some $a$ in the universe of $S$ such that if $v_{x\to a}$ is the assignment obtained by changing $v(x)$ to $a$, then $(S,v_{x\to a})\models \forall y\varphi(x,y$. (This is the definition of what it means for $(S,v)$ to satisfy an existential, and is the formal way to capture that "fixed $x$" from the assumption in the informal argument above.) So now I want to prove $(S,v)\models\forall y\exists x\varphi(x,y)$.
To do this, I need to fix an arbitrary element $b$ in the universe of $S$, and let $v_{y\to b}$ be the variable assignment obtained by changing $v(y)$ to $b$, and then show $(S,v_{y\to b})\models \exists x(\varphi(x,y))$ (this is the definition of what it means for $(S,v)$ to satisfy a formula starting with a universal quantifier). Again, to show $(S,v_{y\to b})$ satisfies what is now an existential statement, I need to find a particular element in $S$ so that if I change $v_{b\to y}(x)$ to this particular element then the resulting variable assignment satisfies $\varphi(x,y)$. Guided by my informal argument, I know that this particular element should be the fixed element $a$ from above. In other words, I should be able to show that if $v_{b\to y,x\to a}$ is the variable assignment obtained by changing $v_{b\to y}(x)$ to $a$, then $(S,v_{b\to y,x\to a})\models\varphi(x,y)$. My only recourse to verify this is with the assumption $(S,v_{x\to a})\models \forall y\varphi(x,y)$. I want to apply this universal quantifier to $b$. In other words, by the definition of satisfaction for a formula starting with the universal, I know that if I let $v_{x\to a,y\to b}$ be the variable assignment obtained by changing $v_{x\to a}(y)$ to $b$, then $(S,v_{x\to a,y\to b})\models\varphi(x,y)$.
To recap, I know $(S,v_{x\to a,y\to b})\models\varphi(x,y)$; and I want to know that $(S,v_{b\to y,x\to a})\models\varphi(x,y)$. The point now of course that $v_{x\to a,b\to y}$ and $v_{b\to y,x\to a}$ are the same variable assignment. They were both obtained from $v$ by changing $v(x)$ to $a$ and $v(y)$ to $b$ (just in a different order, which matches the change in order of quantifiers in the original formula).
All the notation might be hard to keep track of. But I always fall back to the informal idea that my fixed $a$ should work as an $x$  for any $b$ as a $y$.

$^{1}$This is one of the big differences between first-order logic and propositional logic. The analogy of structure/variable assignment pairs in propositional logic is truth assignments. For a given propositional formula, there are only finitely many truth assignments which can be organized neatly into a truth table. So this is an algorithm one can always fall back on to test validity in propositional logic. But in first-order logic, things aren't so easy.
