Definition of "substitutable" in Mathematical Logic

Solution 1:

I don't have the book, but this must go with a definition of substitution of $t$ for $x$ in $\phi$, which I'd write $\phi[t/x]$ and which you are writing as $\phi^x_t$. The definition goes like this (where $y$ denotes any variable other than $x$): $$ \begin{array}{tcl} x[t/x] & = & t \\ y[t/x] & = & y \\ (\lnot\alpha)[t/x] & = & \lnot(\alpha [t/x]) \\ (\alpha \lor \beta)[t/x] & = & \alpha[t/x] \lor \beta[t/x] \\ ((\forall x) \alpha)[t/x] & = & (\forall x) \alpha \\ ((\forall y) \alpha) [t/x] & = & (\forall y) (\alpha[t/x]) \end{array} $$

However, the last clause is not always semantically acceptable. To see what can go wrong, consider the formula $(\forall x)\lnot((\forall y)y + 1 \le x)$. This formula is true and we want to be able to deduce consequences of it by instantiating the bound variable $x$. I.e., given any term $t$, we should have that $\lnot((\forall y) y + 1 \le x)[t/x]$. But if $y$ appears free in $t$, this breaks down: if we just do the substitution according to the above definition with $t \equiv y + 1$, we get the false statement $\lnot((\forall y) y + 1 \le y + 1)$. This has gone wrong because $t$ is not substitutable for $x$ in $(\forall y) y + 1 \le x$ and doing the substitution has invalidly identified the outside world's $y$ with the bound $y$ inside $\forall y\, y + 1 \le x$. To do the substitution validly, we need to rename the bound variable $y$ in $\lnot((\forall y) y + 1 \le x)[t + 1/x]$ to give the equivalent formula $\lnot((\forall z) z + 1 \le x)[t + 1/x]$ and then we get the valid statement $\lnot((\forall z) z + 1 \le y + 1)$.

It would be more intuitive to say validly substitutable rather than substitutable, because substitutable read informally does suggest that it's OK just to replace all the $x$s by $t$s. You have to read it in the context of a definition of substitution for $x$ that always treats bound occurrences of $x$ correctly (by leaving them alone) but only sometimes treats bound occurrences of other variables correctly.