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.

  • 2
    $\begingroup$ You are right ! but the example is aimed exactly at showing you why we have to define substitution in that way. If we do not add the proviso : "$σ_t^y$ is ... if $x≠y$ and is itself otherwise", we are licensed to replace $x$ by $y$ into $∀x∃y(x \ne y)$ getting : $∃y(y \ne y)$. $\endgroup$ – Mauro ALLEGRANZA Sep 29 '14 at 14:35
  • $\begingroup$ @MauroALLEGRANZA , Maybe, but I understood that he defines substitutablity to prevent "bad substitutions" so the idea that any replacement of all occurences of a varaible by a term counts as a substitution seemed to be true and that we define substitutability to prevent such bad substitutions. $\endgroup$ – Fawzy Hegab Sep 29 '14 at 15:07

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

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$.


  1. $(∀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.)


  1. $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 :


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


is true in every model.

  • $\begingroup$ A very good answer, but I wonder, why shouldn't we allow the replacement of a bounded variable? $\endgroup$ – Fawzy Hegab Sep 30 '14 at 4:04
  • 1
    $\begingroup$ @MathsLover - we can "rename" a bound var; i.e. $\forall x \varphi$ is equivalent to $\forall y \varphi$, but again we have to do it "with care". If we have $\forall x \forall y (x=y)$ we cannot do it, because otherwise we will have $\forall y \forall y (y=y)$ which is $\forall y (y=y)$, and the two are not the same ! $\endgroup$ – Mauro ALLEGRANZA Sep 30 '14 at 7:39

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.