[Math] Substituting two variables in a first order logic formula (free and bounded variables)

Question

When we are trying to substitute $x$ by $y$ in a first order logic formula, No free occurrence of $x$ must be in the scope of $y$ quantifier, because if $x$ was free then by substituting by $y$ and being in the scope of $y$ quantifier it will bounded, not free any more!

My problem is the exact meaning of scope of $y$ quantifier. Suppose $Q_1,Q_2$ are any quantifiers and we are going to substitute $x$ by $y$, clearly we are allowed to do this in the following formula $$Q_1y \overbrace{Q_2x P(x,y)}^{Scope-of-y}$$ because $x$ is not free.

But my problem is with this formula:

$$Q_1x Q_2y\overbrace{ P(x,y)}^{Scope-of-y}$$

If we only think of the scope of the $y$ quantifier, $x$ is free because no quantifier of $x$ is in there so we are not allowed to replace $x$ by $y$ while on the other hand $x$ is already bounded by $Q_1x$, So I don't know if we are allowed to substitute $x$ by $y$ or not?. In the aggregate I don't know in replacing $x$ by $y$ in formulas like $$Q_1x Q_2y P(x,y)$$ how the substitution must be done. Thanks

Answer 1

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.