 The \(\lambda\)-calculus earns a special place in the history of logic because it was the source of the first undecidable problem. The problem is: given \(\lambda\)-terms \(M\) and \(N\), determine whether \(M = N\). (A theory of equational reasoning about \(\lambda\)-terms has not yet been defined; the definition will come later.) This problem was shown to be undecidable.