 Early formulations of the idea of \(\lambda\)-calculus by A. Church were indeed inconsistent; see (Barendregt, 1985, appendix 2) or (Rosser, 1985) for a discussion. To take a concrete problem: how do we know that the equation \(\bK = \mathbf{I}\) is not a theorem of \(\lambda\)? The two terms are obviously intuitively distinct. \(\bK\) is a function of two arguments, whereas \(\mathbf{I}\) is a function of one argument. If we could show that \(\bK = \mathbf{I}\), then we could show that \(\mathbf{KK} = \mathbf{IK}\), whence \(\mathbf{KK} = \bK\) would be a theorem of \(\lambda\), along with many other equations that strike us as intuitively unacceptable. But when we’re investigating a formal theory such as \(\lambda\), intuitive unacceptability by no means implies underivability. What is missing is a deeper understanding of \(\beta\)-reduction.