 As a concrete example of this kind of approach to \(\lambda\)-calculus, consider an extension of first-order logic where one can form new atomic formulas using \(\lambda\)-terms, in the following way: