[Math] Why not ban nested quantifiers over the same variable

first-order-logiclogicnatural-deductionpredicate-logic

People seem to think (1, 2, 3) that a wff can have nested quantifiers over the same variable, e.g., $\forall x(Px \wedge \exists x Qx)$.

However, consider the following argument:

  1. $\forall x \exists y Pxy$ (Premise)
  2. $\exists y P\hat{x}y$ (1, $\forall$E)
  3. $\forall y \exists y Pyy$ (2, $\forall$I)

This is clearly not valid, but what is wrong with it? According to wikipedia, the application of $\forall$I is wrong because $y$ occurs in 2.

Here is another invalid argument:

  1. $\forall x Pxc$ (Premise)
  2. $\exists x \forall x Pxx$ (1, $\exists$I)

This is considered invalid for a similar reason: the application of $\exists$I is wrong because $x$ occurs in 1.

But we wouldn't need these restrictions if we just banned nested quantifiers over the same variable. This seems like a simpler rule and we're not losing any expressive power. Does anyone set up predicate logic this way?

Best Answer

It could be done, as described in the other answers.

But it would not make capture-avoiding substitution easier to define, so there's no real benefit.

On the other hand, we would lose the sometimes useful property that a sentence can be substituted into any context without needing to look inside it.

It would also be more difficult to define local rewrites of a formula that introduce a new variable and its quantifier somewhere in the parse tree. Instead of just looking down from the new quantifier's location to make sure it won't capture anything we'd also need to look up to make sure it won't shadow anything. Needing to "look in both directions" might heavily complicate the structure of an inductive definition.

Related Question