 The identification of λ-definability with intuitive computability was certainly not “evident immediately”. In fact, Church’s student, Stephen Cole Kleene, reports that it only gradually dawned on Church, Rosser (J. Barkley Rosser, also Church’s student), and himself that λ-definability may serve as a precise counterpart of intuitive computability (Kleene 1981). Kleene also describes the difficulty of giving λ-definitions of certain basic number theoretic functions—particularly the predecessor function—given the particular way Church gives λ-expressions standing for integers (1981: 56; these λ-expressions are described in  supplement D).  But the fundamental difficulty with  CT1  as Church (1936a) enunciates it is that it is given as a definition without any accompanying justification other than a brief sketch of a proof of the extensional equivalence of λ-definability and recursiveness (Kleene [1936] gives a more detailed proof). Gödel complained of exactly this: