Equivalence of two definitions of substitution

Preliminary definitions

Barendregt [2004] introduces the following two definitions of substitution and their equivalence:

-
Ottamnn variable convention (p. 26)


2.1.13. Ottamnn variable convention. If $M_1, ..., M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.

Remark 1: I'm using the name 'Ottmann variable convention' because in the 6th impression of "The Lambda Calculus. Its Syntax and Semantics", Barendregt replaced the name 'variable convention' by this name. See 'Addenda for the sixth imprinting', p. E1.

-
First definition (p. 27)

-
Second definition (p. 578)

-
Equivalence (p. 579)


If one observes the variable convention, then $M[ x:= N ]$ as in definition 2.1.15 is the same substitution as in Curry's definition C.1.

Question

Since (1) follows the Ottmann variable convention its normalisation using both definitions of substitution should be the same.

$$(λxx.x)yz \qquad \qquad (1)$$

Remark 2: I know it is silly to abstract over $x$ twice in (1), but this is not banned anywhere.

Using Definition C.1, the normalisation of (1) is $z$, but using Definition 2.1.15 I got stuck in

$$(λxx.x)yz = ((λx.x)[ x:=y ])z$$

because Definition 2.1.15 doesn't include a clause when the bound variable and the variable to substitute are the same, that is, the missing clause is

$$λx.M[ x:=N ] ≡ λx.M.$$

Are really both definitions the same using the Ottmann variable convention? Am I missing something when using Definition 2.1.15?

Reference

Barendregt, H. P. (2004). The Lambda Calculus. Its Syntax and Semantics. Revised edition, 6th impression. Vol. 103. Studies in Logic and the Foundations of Mathematics. Elsevier.

The following remark from definition 2.1.15 gives you a clue:


In the third clause it is not needed to say "provided that $y \not \equiv x$ and $y \not \in \mathsf{FV}(N)$". By the variable convention this is the case.

Since you can't make substitutions, it means that there is some violation of the variable convention (§2.1.13):


If $M_1, ..., M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.

In the meta-level expression

$$((λx.x)\ [ x := y ])\ z,$$

let us denote $M_1 = (λx.x)$ and $M_2 = x$. Notice that $x$ is bound in $M_1$, but free in $M_2$. That violates the variable convention, so you can't use definition 2.1.15, because it relies on that convention.

StackExchange Computer Science Q#65315, answer score: 3