# quantifiers that bind nothing

Consider $\forall x \forall y P(y,y)$, where $x$ is quantified, but does not appear.

Is quantifying a variable that otherwise does not appear well-formed or meaningful? I've seen this sort of thing only once before, in a constructive proof that $\forall x A(x) \supset \exists x A(x)$, where what's proved instead is $\forall y (\forall x A(x) \supset \exists(x)A(x))$. I believe this is meant to guard against the possibility of an empty type, where "$\forall x A(x) \supset \exists(x)A(x)$" on its own would be false. But is this meaningful in a classical sense, where we assume the domain is non-empty?

And if $\forall x \forall y P(y,y)$ $is$ meaningful, how does it differ from $\forall y \forall x P(y,y)$?

What about $\exists x \exists y P(x,x)$ and $\exists y \exists x P(x,x)$?

• Yes it is well-formed, which follows from the definition of "formula". It's harmless and doesn't affect the interpretation of a sentence or formula. I don't know what "$\exists(x)$" means as a formula: that is not well-formed. Mar 9, 2016 at 5:00
• Yeah, I fixed that.... I was up late...
– mips
Mar 9, 2016 at 12:25
• But I still see it (3x). Mar 9, 2016 at 16:09
• I was up late and I didn't sleep well...
– mips
Mar 9, 2016 at 17:31
• Haha, no problem — now I don't see it. Thanks. Mar 9, 2016 at 18:03

You can add $\forall x_i$ in front of sentences as much as you want and nothing changes.
If you add $\exists x_i$ in front of sentences where $x_i$ is not being used, it prevents the empty type from satisfying the sentence. Adding multiple $\exists$ is equivalent to adding one, since all the objects that are said to exist can be the same object.