 Incidentally, the notion of free variables is straightforwardly definable now: \(x\) is a free variable of \(M\) iff \(x\) is a subterm of \(M\). The set of free variables of \(M\) is sometimes denoted by \(\textrm{fv}(M)\).