Prove that: $\vdash \forall x(\forall y\alpha)\to \forall y(\forall x \alpha)$

Question

How does one prove that

$$\vdash \forall x(\forall y\alpha)\to \forall y(\forall x \alpha)$$

in first order logic?

I have tried using the specialization and generalization rules on various wffs but they don't lead me to anything concrete.

Answer 1

If we have a formula like $\forall x \forall y\ \alpha$, where $\alpha$ is another arbitrary formula, then we can exchange the order of the quantifiers without changing its semantics. Note, however, that this would NOT be possible if the quantifiers were different, e.g. $\forall x \exists y$.

Now why can we do this? Well, if we have a look at how the semantics of classical first-order logic are defined, then this becomes pretty obvious. Let's suppose we wish to evaluate the truth value of the formula for some signature $\Sigma$ over the domain $\mathcal{U}$ and a variable assignment $\gamma$. Furthermore, let's call the truth evaluation function $I$. With this we have $$I_{\Sigma, \gamma} ( \forall x \forall y\ \alpha ) = \mathbf{T}$$ $$\iff I_{\Sigma, \gamma \cup \{ x \gets c \}} ( \forall y\ \alpha ) = \mathbf{T} \text{ for each $c \in \mathcal{U}$}$$ $$\iff I_{\Sigma, \gamma \cup \{ x \gets c, y \gets d \}} ( \alpha ) = \mathbf{T} \text{ for each $c , d \in \mathcal{U}$.}$$ Obviously, it makes no difference in which order these two quantifiers occur.

Therefore we observe that $$ \forall x \forall y\ \alpha \to \forall y \forall x\ \alpha \equiv \forall x \forall y\ \alpha \to \forall x \forall y\ \alpha \equiv $$ $$ \equiv \neg \forall x \forall y\ \alpha \lor \forall x \forall y\ \alpha \equiv \top \text{,} $$ thus the formula is valid.

Answer 2

I have tried using the specialization and generalization rules on various wffs but they don't lead me to anything concrete.

They should.

Just assume $\forall x~(\forall y~\alpha)$, instantiate using fresh arbitrary variables, and generalise in reverse order to derive $\forall y~(\forall x~\alpha)~$, under that assumption.

Now you may deduce $(\forall x~(\forall y~\alpha))\to(\forall y~(\forall x~\alpha))$.

$\blacksquare$