Free variables preserved in beta-reduction, lambda calculus

Question

In a previous post, it was stated that

"If $M$, $N$ are $\lambda$-terms, and $M \twoheadrightarrow_{\beta\eta} N$, then $fv(N) \subseteq fv(M)$."

Do you have a reference for this statement?

I cannot find it unfortunately.

Thanks for your help.

• Naïm Camille Favier: It's a simple proof by induction, please show some effort.
• Marco Zanin: I think there is some confusion. I do not need the proof. I need a reference, such as a paper (e.g., Feyman et al. 2053, conference, journal) or book (e.g., textbook) that includes this statement. Is there any that you know about?

Answer 1

You first need to show that $\mathrm{fv}(M[N/x]) \subseteq \mathrm{fv}(M) - \{x\} \cup \mathrm{fv}(N)$. This is a straightforward induction on the definition of the substitution. In particular, this means that $\mathrm{fv}(M[N/x]) \subseteq \mathrm{fv}((λx.M)N)$, which gives the result you’re looking for for the base β-reduction case.

For the base η-conversion case, the result is immediate: $\mathrm{fv}(λx.Mx) = \mathrm{fv}(M)$ for any fresh $x$.

The whole result follows by a straightforward induction on arbitrary βη-reductions (i.e., lifting to contexts).

• Marco Zanin: Thank you both for your help, I appreciate it. However, I did not need the proof of the statement, but a reference, such as a paper (e.g., Feynman et al., 2053, conference, journal) or book (e.g., textbook) that includes this statement that I can use.
• sparusaurata: Lemma 9.1.2 in the Barendregt is a variant of what you're looking for. But I don't get why you need a reference for such a standard and trivial result (in particular it would feel quite weird if a paper or a report cited a reference for this).