Is replacing $y$ by $x$ formally a valid substitution in the formula $\forall x\exists y ¬(x=y)$?

Question

In “Friendly introduction to mathematical logic” by Leary, an example is mentioned to demonstrate the importance of defining substitutions and then substitutability as follows:

let $\sigma$ be the $L$-formula, $\forall x\exists y ¬(x=y)$; then when we replace $x$ by $y$ in the formula, the truth value changes, and this is considered as an example for unwanted substitutions. So, we define substitutions and substitutability formally.

The problem is that, according to the formal definition of substitution, this example is not even a substitution!

Because one of the clauses of the definition says that: if $t$ is a term, $x,y$ are variables and $\sigma$ is a formula then,

if $\sigma$ is $(\forall x) (\alpha) $ then $\sigma ^y_t$ is $(\forall x)(\alpha ^y_t)$ if $x\not= y$ and is itself otherwise.

In our example, we have $x=y$ so $\sigma ^x_y$ is $\sigma$ and there is no change in the formula. hence, such replacement is not a substitution. Am I getting it wrong?

I've checked the errata, no thing is mentioned about this particular example.

Answer 1

I'll refer to (one of) my preferred textbooks :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112 :

he defines substitution by recursion :

1. For atomic $\alpha, \alpha_t^x$ is the expression obtained from $\alpha$ by replacing the variable $x$ by $t$.

[...]

4. $(∀y \alpha)_t^x$ is $∀y \alpha$, if $x = y$, $∀y(\alpha_t^x)$ if $x \ne y$.

Then he discuss the fallacy of substituting $y$ for $x$ into $∀x¬∀y(x=y)$, getting the wrong : $¬∀y(y=y)$, which again is exactly your example.

The problem is that when $y$ was substituted for $x$, it was immediately “captured” by the $∀y$ quantifier. We must impose a restriction [...] that will preclude this sort of quantifier capture. Informally, we can say that a term $t$ is not substitutable for $x$ in $\alpha$ if there is some variable $y$ in $t$ that is captured by a $∀y$ quantifier in $\alpha_t^x$.

Thus [page 113] he defines :

Let $x$ be a variable, $t$ a term. We define the phrase “$t$ is substitutable for $x$ in $\alpha$” as follows:

1. For atomic $\alpha, t$ is always substitutable for $x$ in $\alpha$. (There are no quantifiers in $\alpha$, so no capture could occur.)

[...]

3. $t$ is substitutable for $x$ in $∀y\alpha$ iff either

(a) $x$ does not occur free in $∀y\alpha$, or

(b) $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\alpha$. (The point here is to be sure that nothing in $t$ will be captured by the $∀y$ prefix and that nothing has gone wrong inside $\alpha$ earlier.)

For example, $x$ is always substitutable for itself in any formula. If $t$ contains no variables that occur in $\alpha$, then $t$ is substitutable for $x$ in $\alpha$.

The reader is cautioned not to be confused about the choice of words. Even if $t$ is not substitutable for $x$ in $\alpha$, still $\alpha_t^x$ is obtained from $\alpha$ by replacing $x$ wherever it occurs free by $t$.

The two definitions are exactly the same as in Christopher Leary, A Friendly Introduction to Mathematical Logic (2000), pages 39-41.

---

I think that you are "not seeing" the difference between the two concepts because you are thinking only to one part of the problem :

$(∀y \alpha)_t^x$ is $∀y \alpha$, if $x = y$, $∀y(\alpha_t^x)$ if $x \ne y$.

This clause prevent us from replacing the bound variable. I.e. with $∀y(x=y)$ we can perform $(∀y(x=y))_t^x$ to get $∀y(t=y)$ but we cannot perform $(∀y(x=y))_t^y$.

But we have another possible (bad) case : when $t$ has free variables inside, included the "degenerate" case when $t$ is $y$.

In this case the above clause tells us nothing, because we are trying to put $t$ (i.e. $y$) in place of $x$ inside $∀y(x=y)$. In this case $x$ is not the bound variable (which is $y$) but the result is still not what we expect.

The formula :

$∀y(x=y)$

is true in a model with only one object, while :

$∀y(y=y)$

is true in every model.

Answer 2

To be able to formally replace $y$ by $x$, it must be true that $x=y$ (or $y=x$) where $x$ and $y$ are free variables. In the statement $\forall x\exists y ¬(x=y)$, $x$ and $y$ are not free variables; they are bound variables. For this reason, we cannot make the substitution.