 If \(\bA_{\alpha}\) is a wff of type α in which \(\bu_{\alpha \beta}\) is not free, the function (associated with) \(\bu_{\alpha \beta}\) such that \(\forall \bv_{\beta}[\bu_{\alpha \beta}\bv_{\beta} = \bA_{\alpha}]\) is denoted by \([\lambda \bv_{\beta}\bA_{\alpha}]\). Thus \(\lambda \bv_{\beta}\) is a variable-binder, like \(\forall \bv_{\beta}\) or \(\exists \bv_{\beta}\) (but with a quite different meaning, of course); λ is known as an abstraction operator. \([\lambda \bv_{\beta}\bA_{\alpha}]\) denotes the function whose value on any argument \(\bv_{\beta}\) is \(\bA_{\alpha}\), where \(\bv_{\beta}\) may occur free in \(\bA_{\alpha}\). For example, \([\lambda n_{\sigma}[4\cdot n_{\sigma}+3]]\) denotes the function whose value on any natural number n is \(4\cdot n+3\). Hence, when we apply this function to the number 5 we obtain \([\lambda n_{\sigma}[4\cdot n_{\sigma}+3]]5 = 4\cdot 5+3 = 23\).