# Lambda calculus : what about the bound variables in substituting expression?

I found the following set of lemma in my lambda calculus textbook :

Lemma 1.16 Let $x, y, v$ be distinct (the usual notation convention), and let no variable bound in $M$ be free in $vPQ$. Then

(a) $[P/v][v/x]M \equiv [P/x]M$ if $v \notin \mathrm{FV}(M)$;

(b) $[x/v][v/x]M \equiv M$ if $v \notin \mathrm{FV}(M)$;

(c) $[P/x][Q/y]M \equiv [([P/x]Q)/y][P/x]M$ if $y \notin \mathrm{FV}(P)$;

(d) $[P/x][Q/y]M \equiv [Q/y][P/x]M$ if $y \notin \mathrm{FV}(P), x \notin \mathrm{FV}(Q)$;

(e) $[P/x][Q/x]M \equiv [([P/x]Q)/x]M$.

In the first lemma , the first stage of substitution can be done because $x$ is a free variable in $M$ and and no variable bound in $M$ is free in $V$. But what about variables which are free in $M$ but bound in $V$? In that case, the substitution would carry the risk of changing the semantics, like if there were a free variable in $V$, let's say $K$, and there were a term in $M$ like $\lambda.k$ then it would definitely make $K$ a bound variable in $M$ if the $X$ being replaced is at a position right to the $\lambda .k$ and the substitution will be wrong.

How is this resolved? I am unable to see through this clearly.

$x$, $y$, and $v$ are variables not (arbitrary) terms. To the extent that it makes sense to say so, the only variable free in $v$ is $v$. There could still be an issue with, say, $M = \lambda v.x$, i.e. $[v/x]\lambda v.x$, but, by assumption, $v$ is not bound in $M$, so this is not a valid case; $v$ is clearly free in $vPQ$.
• It's seems apparent (and is likely explicitly specified as so in the book) that lowercase letters refer to variables and uppercase letters refer to terms, so you shouldn't arbitrarily change capitalization. For your question, I don't know what you mean. Sufficient for what? The lemma is only talking about the case where $v$ is a variable. You don't need to consider other cases because it's not saying anything about other cases. – Derek Elkins left SE Jun 25 '17 at 22:02
• @AgniveshSingh It's generally on this site to create new questions, if you have further questions. Roughly, if you can tell whether an answer answers your (original) question, then any further questions should probably be new questions. Nevertheless, there is no assumption that $x$ is not free in $P$ or $Q$, so $[Q/x]M$ can still have occurrences of $x$. – Derek Elkins left SE Jun 26 '17 at 20:26