 In the second paper (Church 1933), the problem about Russell’s paradox was corrected. But Kleene and Rosser (1935) established that both systems—those of Church 1932 and 1933—as well as related early systems of combinatory logic fell prey to Richard’s paradox. The mere part—the pure untyped λ-calculus—is, however, consistent in the sense that not all equations between λ terms are derivable. This follows from an early result due to Church himself and Rosser (1936)—the Church-Rosser theorem (see the entry on the  lambda calculus  for discussion). Significant mathematical models for the λ-calculus were developed later (Scott and Strachey 1971; Plotkin 1993; see Hindley &amp; Seldin 2008: ch. 16). Church also proved the consistency of a variant of the system of (1933) by elementary means (1934), thus escaping, as he hoped, the incompleteness theorems of Gödel (1931). But this system was too weak to satisfy requirement (2), and Church abandoned the system. (A type-free system with a similar motivation was proposed later by Myhill 1975.) It is remarkable that in his failed struggle to produce a consistent, type-free foundational system, Church nevertheless introduced ideas that have profoundly affected the development of logic.