Proving combinator identity KMN=M

Question

Have a problem proving K MN=M

1. By the K combinator definition

   $ (\lambda x y.x) M N $

2. Parenthesized

   $ ((\lambda x. (\lambda y.x)) M) N $

3. By the principal axiom of lambda calculus

   $ (\lambda y.M) N $

4. Second application of the principal axiom

   $ M[y:= N] $ ?

This would give correct result if M is y-free. Apparently there is an error at one of the steps.

Answer 1

When you reduce $(\lambda x.\lambda y.x)M$, the result is $(\lambda y.x)[x:= M]$. This substitution is only defined if$y$ is not free in $M$. Otherwise the $\lambda y$ will need to be $\alpha$-renamed before you can proceed.

Some texts define the substitution function to do this $\alpha$-renaming implicitly, others consider the result of the substitution to be undefined if the variable capture condition is not met.