 Is the \(\lambda\)-calculus consistent? The question might not be well-posed. The \(\lambda\)-calculus is not a logic for reasoning about propositions; there is no apparent notion of contradiction \((\bot)\) or a method of forming absurd propositions (e.g., \(p \wedge \neg p)\). Thus ‘inconsistency’ of the \(\lambda\)-calculus cannot mean that \(\bot\), or some formula tantamount to \(\bot\), is derivable. A suitable notion of ‘consistent’ is, however, available. Intuitively, a logic is inconsistent if it permits us to derive too much. The theory \(\lambda\) is a theory of equations. We can thus take inconsistency of \(\lambda\) to mean: all equations are derivable. Such a property, if it were true of \(\lambda\), would clearly show that \(\lambda\) is of little use as a formal theory.