# Proving combinator identity KMN=M

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.

-

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.
@TegiriNenashi: The most convenient way to proceed would be, because you're free to $\alpha$-convert at any time, to start by saying: "Choosen an $\alpha$-renaming of $\lambda xy.x$ such the each variable becomes something that is neither free in $M$ nor in $N$; in the following, assume that the letters $x$ and $y$ stand for whichever such "safe" variable names we choose." – Henning Makholm Jun 15 '12 at 20:07
...(continued) Often the lambda calculus is defined such the real name of variables in the calculus is always something ugly such as $X''''''''$, and the meaning of the "$x$"s that appear on the page in actual proofs is always a meta-variable that ranges over the ugly "real" variable names. (Another somewhat popular convention is that calculus-level variable names are in typewriter-style like x, and things in mathematics fonts like $x$ are always metavariables that range over variable names). – Henning Makholm Jun 15 '12 at 20:09