 These considerations among others raised the issue of what constitutes a properly formal theory. Gödel paid very special attention to it when giving his Princeton Lectures in 1934. At the very end he introduced the general recursive functions. This class of number theoretic functions was shown to be co-extensional with Church’s λ-definable ones by Church and Kleene. In Church 1936 an “identification” of effective calculability and general recursiveness was proposed, what is usually called Church’s thesis. Turing, of course, proposed his machine computability for a very similar purpose and proved its equivalence to λ-definability in an appendix to his 1936. Church and Turing used their respective notion to establish the undecidability of first-order logic. For Gödel, this was the background for formulating the incompleteness theorems in “full generality” for all formal theories (containing a modicum of number or set theory); see the Postscriptum to the Princeton Lectures Gödel wrote in 1964: