Second order universal quantifier elimination restriction

Question

Dirk van Dalen in his Logic and Structure gives following universal elimination rule:

from $\forall_{X^n} \phi$ infer $\phi^*$

where $\phi^*$ is $\phi$ in which every occurence of $X^n(t_1, ..., t_n)$ was substituted by such $\rho(t_1, ..., t_n)$ ,where $\rho$ is formula, that no free variable of $t_i$ is captured by $\rho$.

He states this rule without any explanation. It do not understand why I can not capture any of free variables of $t_i$. I would intuitively expect that I can because if I proved that something is derivable for any formula $\rho$ why should I limit my self to some subset of all formulas?

Answer 1

Regarding the rules for SOL :

$$\frac{∀X^n \varphi }{\varphi^*}\quad ∀^2E$$

where [...] $\varphi^*$ is obtained from $\varphi$ by replacing each occurrence of $X^n(t_1,\ldots, t_n)$ by $\sigma(t_1,\ldots, t_n)$ for a certain formula $\sigma$, such that no free variables among the $t_i$ become bound after the substitution [and the same for $\exists^2I$, page 147]

the reason for the restriction is the same as for FOL: we have to avoid that a free occurrence of a variable in the formula $\sigma$ used in the substitution is captured by a quantifier already present into $\varphi$.

We must take into account than in SOL the variables are not only individual ones, but also predicate ones.

So, we can try with the following counter-example ...

From the quite harmless formula :

$\forall X \exists Y \forall x [Y(x) \leftrightarrow \lnot X(x)]$

substituting (illegally) $\sigma(x) := Y(x) \land (x = x)$ in place of $X(x)$, by ($\forall^2E$) we get :

$\exists Y \forall x [Y(x) \leftrightarrow \lnot (Y(x) \land (x = x))]$

i.e.

$\exists Y \forall x [Y(x) \leftrightarrow (Y(x) \rightarrow (x \ne x))]$.