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

-
Do you mean $\exists x\exists y\ldots \forall x\forall y\ldots$? – Asaf Karagila Oct 24 '11 at 23:36
Yes, where ∀x∀y are inside the scope of ∃x∃y, ie ∃x∃y(...∀x∀y(...)). – user18180 Oct 24 '11 at 23:40
The variable bound by a quantifier is completely separate from other uses of the variable letter outside the scope of the quantifier, so your formula is nothing more nor less than $\exists x\exists y.(P(x,y)\to\forall z\forall w. P(z,w))$. This is classically valid, by the way. – Henning Makholm Oct 24 '11 at 23:41
@HenningMakholm OK, that change of letters make sense. However, I fail to proof its validity. It's hard for me to type my sequent calculus "proof" (it's: $\exists right; \rightarrow right; \forall right$ and then I end up with different variables on each side). Thanks for the comment :) – user18180 Oct 24 '11 at 23:57
Hint: since it's classically valid but not intuitionistically valid, you'll need to use sequents with more than one formula on the right-hand side. It may be easier to draft the proof as $\exists x.(\phi(x)\to\forall y.\phi(y))$ and then double the variables afterwards. – Henning Makholm Oct 25 '11 at 0:03

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

-
This answer makes complete sense. I also understand the last sentence. And my intuition says it's satisfiable (make $P(x,y)$ false for a pair of values and the formula would be true). However, I can't see how that statement would be valid (true in all interpretations). – user18180 Oct 25 '11 at 0:04
@user18180: I am not sure what is the framework in which you work here. – Asaf Karagila Oct 25 '11 at 0:11
Well, an implication is true if the LHS is false, thereby making the whole formula true. Am I incorrect? – user18180 Oct 25 '11 at 0:22
@user18180: Yes, you are correct. If there is a pair for which the LHS is false then the formula is true, if there is none then for every pair it is true and the RHS of the implication is true. – Asaf Karagila Oct 25 '11 at 0:24
@user18180: Of course this is true if you are working in classical FOL, which is why I asked about the framework. The comments on the main question seemed to possibly imply otherwise. – Asaf Karagila Oct 25 '11 at 0:26

$$\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).$$

-
Thanks for the formula clarification. I'm sure I'll use this in my attempts to prove it :) – user18180 Oct 25 '11 at 1:11