Substitution is the "process" of replacing in a formula $\alpha$ the variable $x$, wherever it occurs free in $\alpha$, by the term $t$ [that, of course, can be another variable, like $y$].
In symbols :
$\alpha^x_t$
or :
$\alpha[t/x]$.
The substitution is allowed provided that “$t$ is substitutable for $x$ in $\alpha$”; informally, it means that, if the term $t$ contains some occurrence of e.g. the variable $y$, we have to avoid that with the substitution for $x$, $y$ is “captured” by a $∀y$ quantifier.
We do not replace the quantified variable; getting e.g. $\forall y \ P(y)$ from $\forall x P(x)$ is not a substitution. We can do it, with some care...
In your example with :
$Q_1 x \ Q_2 y \ P(x,y)$
the scope of $Q_1 x$ is the subformula $Q_2 y \ P(x,y)$ and the scope of $Q_2 y$ is the subformula $P(x,y)$.
Thus, we cannot substitute neitehr $x$ nor $y$; if we want "rename" one of them we can do it; the only prescription is : use a fresh variable.
In this way, we can also "swap" them; we have to rename first $y$ with $z$, in order to get :
$Q_1 x \ Q_2 z \ P(x,z)$
then rename $x$ with $y$ (now $y$ does not occur any more in the formula) :
$Q_1 y \ Q_2 z \ P(y,z)$
and finally rename $z$ with $x$ :
$Q_1 y \ Q_2 x \ P(y,x)$.
The result has the "same meaning" of the initial formula; all the above process can be "made formal" thorugh suitable derivations in the proof system.
Yes, it is. The $\forall x$ isn’t quantifying any free variables, since there are no free variables in $\exists x \ x<x$, and the $\forall x$ is therefore called a ‘null quantifier’. However, using the standard semantics for quantifiers we can still evaluate such a statement: we effectively ask: is it true for all objects in our domain that $\exists x \ x<x$ is true? And note, if $\exists x \ x<x$ is true, then it is true that 'for all objects' $\exists x \ x<x$ is true.
Indeed, it turns out that $\forall x \ P$ is equivalent to just $P$ if $P$ does not contain any free variables. Same goes for a null existential quantifier. As such, we have the following well recognized equivalence principles:
Null Quantification
where $P$ does not contain any free variables $x$, we have:
$\forall x \ P \Leftrightarrow P$
$\exists x \ P \Leftrightarrow P$
So no, there is no problem with allowing null quantifiers. And the fact that we have multiple quantifiers quantifying over the same variable isn't an issue either. Indeed, if it helps you to think about this, we can note that $\forall x \exists x \ x < x$ is equivalent to $\forall y \exists x \ x < x$ : both have null quantifiers that can simply be removed.
In fact, sometimes when we do formal logical manipulations it is handy to allow these null quantifiers. Consider the following demonstration of one of the Prenex laws that says that if $P$ contains no free variables $x$ then $P \land \forall x Q \Leftrightarrow \forall x (P \land Q)$
Going from right to left:
$\forall x (P \land Q) \Leftrightarrow$
$\forall x \ P \land \forall x \ Q$ (by distribution of $\forall$ over $\land$) $\Leftrightarrow$
$P \land \forall x \ Q$ (by Null quantification)
Best Answer
You are right.
The "usual" convention is that quantifiers, like negation, apply as little as possible.
Thus, $∃xα∧β$ is $(∃xα∧β)$, and not $∃x(α∧β)$.
The same for $∀xP(x) → Q(x)$: without parentheses, the scope of $∀x$ is only $P(x)$. Thus, the occurrence of $x$ into $Q(x)$ is free.