 In a footnote, Church remarked that from a classical point of view, the parenthetical condition is not required, but is in “the direction of” intuitionism, which he described as “radical”, but the proviso nonetheless was, in subsequent parts of his 1956a, always included. But such a determination must be made on the basis of a precise counterpart of the concept of an effective procedure, such as a recursive or λ-definable procedure. In case there is a positive result,  CT2  allows one to infer that a computable (effective) procedure exists; and if the result is negative,  CT1  allows the inference to its non-existence. This has been the role of CT in computability theory and the development of logic. A particularly telling example is Church’s negative solution to the Entscheidungsproblem—the decision problem for first order logic, now known as “Church’s theorem” (1936b). It was felt that a positive solution would render mathematics completely mechanical at least in principle. Every mathematical problem could in principle be solved by an algorithm. On the other hand, the shape of a negative solution was a mystery. It is reported that von Neumann declared that “We have no clue how to prove it” (Gandy 1988: 62). Church’s result rendered a negative solution conceivable and gave some hope that the solution to mathematical problems would continue to require human ingenuity. In any case, appeals to CT1 have sometimes been viewed as part of the proofs giving the solutions to decision problems and sometimes not, depending on the required degree of formalization. To prove, for example, that some axiomatic theory is undecidable is to prove that its set of theorems is not recursive (or not Turing computable, etc.) and the appeal to CT1 often comes after the strictly mathematical work. However, it has not been common to suggest that one or other of the precise counterparts of intuitive computability should actually replace it; and although Gödel comes close to such a view (in the case of Turing computability), this is not the standard view. Other reductions of intuitive notions to mathematical terms have often been viewed as replacements (cf. Mendelson 1990); but there has been resistance to this view in the case of Church’s thesis, for otherwise logicians should long ago have ceased to speak of intuitive computability (effective calculability).