Is there a reason to consider formulas with multiple quantifiers on the same variable?

Question

I'm very green at mathematical logic, so I apologize for what may be a stupid question.

As I understand it, the definition of a first-order formula allows for monstrosities like

$$\exists x \neg \exists x \varphi(x),$$

$$\forall x \forall x \forall x \exists x \psi(x),$$

etc. Is there a good reason to define formulas in such a way that these kinds of "formulas" are included? For instance, I was trying to write up a proof of the Tarski-Vaught test, and it seems like this case requires special handling apart from the main argument.

My natural instinct would be to define formulas in such a way that $\exists x \phi$ is a formula only if $x$ is a free variable in $\phi$, but this doesn't seem to be how things are generally done.

Answer 1

Note that when a specific variable $x$ is quantified repeatedly, the quantifier nested closest to the quantified statement is the one and only quantifier of $x$ that applies: it negates any and all previous quantifiers on that variable.

So:

$$\exists x, \color{blue}{\lnot \exists x}\varphi(x)\;\equiv\;\lnot \exists x\, \varphi(x)$$

$$\forall x,\,\forall x, \,\forall x, \,\color{blue}{\exists x}\, \psi(x)\; \equiv \;\exists x\, \psi(x)$$

Answer 2

Here are a few places where the convention is used:

• If $x$ is not free in $\psi$ then $(\forall x)\phi \lor \psi$ is equivalent to $(\forall x)(\phi \lor \psi)$. This is used to help put formulas in prenex normal form. If $\psi$ contains $x$ as a bound variable, under the proposal in the question, we would have to modify the algorithm for prenex form, because otherwise $(\forall x)(\phi \lor \psi)$ might no longer be a formula. In particular, the algorithm would no longer be purely recursive in the same way.

• If we want to replace a symbol in a formula with its definition in terms of another formula, normally we can ignore any bound quantifiers in the definition. For example, the set-theoretic formula $\emptyset \subseteq x$ can be rewritten in the language $\{\in\}$ as $$(\forall z)[(\forall w)[w \not \in z] \to (\forall p)[p \in z \to p \in x]]$$ If we did this inside a larger formula, we can normally just ignore any outer quantifiers over $z$, $w$, or $p$, because these are not free in the displayed formula above. It would add a small amount of extra work to keep changing the variables to other ones.