 It turned out that despite this restriction a form of Russell’s paradox is derivable in the system of 1932. Nevertheless, it was here that Church first formulated the (untyped) λ-calculus as a mere part of the whole system. This part turned out to be of great importance for the theory of computation, formal semantics and for the foundations of mathematics in general. So much for inconsistency! (See  supplement D  for a description of the λ-calculus).