# $\lambda$-calculus: structural induction principle over $\Lambda$

The set $\Lambda$ is given inductively by:

• $x\in\Lambda$, if $x$ is a variable;
• $(\lambda x M)$, if $x$ is a variable and $M\in\Lambda$;
• $(MN)$, if both $M,N\in\Lambda$.

Now, consider the structural induction principle associated with $\Lambda$. Say a property $P(M)$ over $M\in\Lambda$. Consider just the second case; is it(?)

• $P(x)\wedge P(M)\implies P(\lambda x M)$, for all $x$ variable and $M\in\Lambda$.
-

No. $P(x)$ doesn't even make sense, because $P$ is a property of lambda expressions, and $x$ is not an expression, it is just a variable. The correct induction principle is
• $P(M) \implies P(\lambda x M)$ for all variables $x$ and $M\in\Lambda$.
I considered that, but since the first case says that $x\in\Lambda$ whenever $x$ is a variable, I thought that I should include it too as the hypothesis. – user59517 Jan 24 '13 at 17:01
The definition given abuses the terminology a little bit. A single variable is an example of an expression, but the bound variable $x$ in $\lambda x.M$ is not an expression, it is a variable. – MJD Jan 24 '13 at 18:52