I am reading "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt.
On page 6, $M \equiv N$ is defined to mean that the $\lambda$-terms $M$ and $N$ are identical. On page 10, $\alpha$-equivalence is defined to be:
- $\lambda x. N =_\alpha \lambda y. N^{x \to y}$ if $y$ is not a variable in $N$
- Any other terms are lambda equivalent iff their subterms are $\alpha$-equivalent
- $M =_\alpha M$
On page 12, substitution is defined to be:
- $y[x := N] \equiv N$ if $x = y$ or $\equiv y$ otherwise
- $(PQ)[x := N] \equiv (P[x := N])(Q[x := N])$
- $(\lambda y. P)[x := N] \equiv \lambda z. (P^{y \to z}[x := N])$ if $P^{y \to z}$ is an $\alpha$-variant of $P$ such that $z$ is not a free variable in $N$
But since $(\lambda a. M)[x := y] \equiv \lambda a. M[x := y]$ if $a \neq x$ but also $(\lambda a. M)[x := y] \equiv \lambda b. M[x := y]^{a \to b}$ and $M[x := y] \equiv M[x := y]$, this would mean that (because of transitivity of $\equiv$) for any term $N$, $\lambda a. N \equiv \lambda b. N^{a \to b}$. Since $\equiv$ also follows rules 2 and 3 of alpha equivalence, this would mean that any $\alpha$-equivalent terms would be identical.
Is this a mistake in the book (does substitution not work for $\lambda y. P$ when $N$ contains a free $y$, as Wikipedia seems to say) ? Or can we really say that two $\alpha$-equivalent terms are identical?
Also, even if this is right, shouldn't there also be a condition that $z \neq x$ in rule 3 of substitution?