 The function of \(\lambda\) in an abstraction term \((\lambda x[M]\)) is that it binds the variable appearing immediately after it in the term \(M\). Thus \(\lambda\) is analogous to the universal and existential quantifiers \(\forall\) and \(\exists\) of first-order logic. One can define, analogously, the notions of free and bound variable in the expected way, as follows.