First-order logic: nested quantifiers for same variables

Doing some homework, I'm asked to determine if the following formula is satisfiable, valid or neither.

I am confused by the nesting quantifiers for the same variables.

Using sequent calculus, I derive this is not valid, but I think it's valid because the variables are all bounded to the same first quantifier.

$$\exists x\exists y (P (x, y) \rightarrow \forall x\forall y P (x, y))$$

Help would be much appreciated.

Edited to avoid confusion. This is about classical FOL using sequent calculus.

Solution 1:

This is really about how you evaluate the truth value.

$\exists x\varphi(t)$ is true if and only if there exists some $x$ for which $\varphi(x)$ is true. Conversely it is false if and only if for all $x$ (in a given model, of course) $\varphi(x)$ is false.

The inner quantification is mostly to "confuse" your intuition and since the truth value of $\forall x\forall y(P(x,y))$ is not dependent of the truth value of the outer quantification it is easier to change the variables, even informally before writing the actual proof.

The claim itself just says that there is a pair $(x,y)$ such that if $P(x,y)$ then $P$ is all the ordered pairs of the universe.

We can prove the validity of this formula from an external point of view, and we do that semantically (that is we do not try to write a proof, but rather show that is holds in every model), for brevity denote our formula $\varphi$.

Let $M$ be an arbitrary model of our language (where $P$ is a binary relation).

If $M\models\forall x\forall y(P(x,y))$ then $M\models\varphi$ (can you see why?)

If $M\models\lnot(\forall x\forall y(P(x,y))$ then for some $a,b\in|M|$ we have $\lnot P(a,b)$. In particular for this pair that $M\models P(a,b)\rightarrow\forall x\forall y(P(x,y))$, so we have $M\models\varphi$.

If needed, this should be made rigorously using the $\operatorname{val}$ function. I strongly recommend on working the details yourself and following closely after the definitions of $\operatorname{val}_M(\exists x\varphi,g)$ (and similarly $\forall x\varphi$).

Solution 2:

$$\exists x\;\exists y\; \left(P (x, y) \rightarrow \forall x\;\forall y \;P (x, y)\right).$$

I wonder if the notion of an "alphabetic variant" can make this clearer: $$\exists x\;\exists y\; \left(P (x, y) \rightarrow \forall u\;\forall v \;P (u, v)\right).$$ Then you can say that $P(x,y) \rightarrow \forall u\;\forall v \;P (u, v)$ is equivalent to $\forall u\;\forall v \;\left( P(x,y) \rightarrow P (u, v) \right)$, so the expression above is equivalent to $$\exists x\;\exists y\; \forall u\;\forall v \;\left( P(x,y) \rightarrow P (u, v) \right).$$