# I did not understand one thing in the proof of substitution lemma?

The substitution lemma in lambda-calculus is proved by the following way, but I just did not understand the application of induction hypothesis in it.

The lemma as shown below, where $x$ and $y$ are distinct and $x$ is not among the free variables of $L$:

   M[x:=N][y:=L]  equals M[y:=L][x:=N[y:=L]]


to prove that in the case where $M= \lambda z.M_1$, by the variable convention, $z$ is distinct from $x$ and $y$, and $z$ is not among the free variables of $N$ and $L$. and The proof goes like this

    (1)    =  (λz.M1)[ x:=N ] [ y:=L ]
(2)    =  λz.M1[ x:=N ] [ y:=L ]             by susbtitution definition
(3)    =  λz.M1[ y:=L ] [ x:=N [ y:=L ] ]    by induction hypothesis
(4)    = (λz.M1)[ y:=L ] [ x:=N [ y:=L ] ]   by susbtitution definition


so, it is proved.

I think 3th line is obtained by substitution definitions $(M_1 M_2)[x:=N] = (M_1[x:=N])(M_2[x:=N])$, right? Just did not see last line, how it is obtained? how induction hypothesis is applied? substitution lemma given here Can someone explain this point to me? Thanks in advance!

• The proof is by induction on the structure of $M$. $M_1$ is a simpler term than $M$, so we are using the induction hypothesis applied to the term $M_1$, that is, that the substitution lemma works for $M$.
– tci
Apr 25, 2016 at 21:10
• @tci. at the third step,I mean how it is applied?
– alim
Apr 26, 2016 at 6:30
• Which step are you referring to, exactly? The third step by my counting (and also by what you have written) is obtained by just using the definition of substitution, and the fact that z is a variable which does not occur in L or N.
– tci
Apr 26, 2016 at 19:49
• @tci, Hi, I edited my question to make it clear. please take a look :)
– alim
Apr 27, 2016 at 6:57

The proof of the substitution lemma for the case $\lambda z.M_1$ has nothing to do with the definition of substitution for the application.
By definition of substitution, $(\lambda z.M_1)[x:=N][y:=L] = \lambda z.(M_1[x:=N][y:=L])$ since the hypotheses about $x$ ensure that the substitutions can be moved inside the $\lambda$.
Since $M_1$ is a smaller term than $\lambda z.M_1$, the induction hypothesis can be applied to $M_1$. This means that you can use the statement that you want to prove for the term $M_1$ (see Wikipedia for more details about structural induction). Therefore, $M_1[x:=N][y:=L] = M_1[y:=L][x:=N[y:=L]]$ and hence $\lambda z.(M_1[x:=N][y:=L]) = \lambda z.(M_1[y:=L][x:=N[y:=L]])$.
By definition of substitution again, $\lambda z.(M_1[y:=L][x:=N [y:=L]]) = (\lambda z.M_1)[ y:=L ] [ x:=N [ y:=L ]]$ since the hypotheses about $x$ ensure that the substitutions can be moved outside the $\lambda$.