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
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.