 However, significant developments in computability theory often take the form of informal mathematics, as with the rest of mathematics. An informal method of computation is given, where it is clear that it could be replaced by a formal one although such a demonstration might be thought to be unnecessary or cumbersome. To give a simple example: Proofs of Craig’s theorem that any recursively enumerable set of formulas is recursively axiomatizable often take the form of an informal argument that the set of Craig-axioms is decidable; and then  CT1  is applied to conclude that it is recursive (cf. Craig 1953). Rogers (1967) gives many examples of the role of informal mathematics in conjunction with CT1 in computability theory. In fact, Rogers’ classic text uses informal mathematics together with Church’s thesis in its positive (non-contrapositive) form to develop recursive function theory as a whole. By contrast, Davis (1958) gives a fully formal account and so uses CT1 mainly in its contrapositive form, or, equivalently, in its positive form but resting on a reductio assumption. A third role of CT1 has been to motivate the proofs that certain basic sets and relations are recursive. For example, membership in the set of formulas of a standard formalized language is intuitively computable. Hence by CT1 it must be recursive, but a proof that it is recursive can be surprisingly complex (see Boolos et al. 2007: Ch. 15).