Supplement to Alonzo Church
A. Chuch on Computability
A.1 Church’s Unsolvable Problem
The following is a brief description of the results of Church’s (1936a) and (1936b), including a sketch of Church’s proof of the main theorem of (1936a). Without some understanding of these matters it is impossible to comprehend the content of CT and its role in logic, as Church saw it, in the midst of revolutionary developments in logic. (Note: Definitions of key concepts of the λ-calculus used in Church’s proof are taken directly from Church’s paper. For further discussion of the untyped λ-calculus, see supplement D as well as the entry on the lambda calculus.)
Church’s paper exploits notions from both the λ-calculus and the then incipient recursion theory—in particular, he uses the equivalence of recursiveness and λ-definability, which he proves. But he observes (in 1936a: fn. 3) that with little alteration, the results might be presented solely in terms of the λ-calculus. Commentators have wondered why Church chose to state his thesis in terms of recursiveness rather than λ-definability but as this footnote indicates, the reasons cannot have been purely logical or mathematical. It is likely that Church was reacting to Gödel’s doubts about λ-definability as a representation of intuitive computability. See A.2 below.
The main theorems of (1936a) read as follows:
- Theorem XVIII: There is no recursive function of a formula \(C\) whose value is 2 or 1 according as \(C\) has a normal form or not.
- Theorem XIX: There is no recursive function of two formulas \(A\) and \(B\) whose value is 2 or 1 according as \(A \conv B\) or not.
“\(A \conv B\)” (\(A\) converts to \(B\)) means that \(B\) results from \(A\) by a series of applications of the rules of λ-conversion; and to say that \(C\) is in normal form is to say that neither it nor any part of it is of the form \(\lambda x \hdot M(N)\). (For the rules of λ-conversion and the notion of being in normal form see supplement D.)
Church remarks that the content of Theorem XVIII is that “the property of a well-formed formula that it has a normal form is not recursive” (1936a [BE: 123]). (Note that there is an important difference between this property and the property of being in normal form. The latter is recursive.) This result is quite remarkable, even from a jaded contemporary point of view accustomed to proofs of undecidability. The syntax of the λ-calculus and the rules of conversion are in themselves extremely simple, as compared even with the definition of a Turing machine. And the underlying idea of a calculus representing functions and the application of function to argument is about as fundamental to mathematics as it gets. Yet Church is able to prove that the basic operation of this calculus is unsolvable. In the last paragraph, Church applies this result to the “Entscheidungsproblem”, using the latter term in a more general sense than usual. He argues that it is a corollary of Theorem XIX that any ω-consistent system of logic containing relatively weak methods of proof and definition would contain a formula \(\Psi(a, b)\) expressing that \(a\) and \(b\) are the Gödel-numbers of formulas \(A\) and \(B\) such that \(A\) is convertible to \(B\). If \(A\) is convertible to \(B\), then \(\Psi(a, b)\) is provable, and if not, then \(\Psi(a, b)\) is not provable, given that the system is assumed to be ω-consistent. (Any ω-consistent system must be consistent, but the converse is not true; see Boolos, Burgess, and Jeffrey 2007 for the relevant definitions.) Such a system, Church argues, must be undecidable, since otherwise the problem of deciding whether or not \(A\) is convertible to \(B\) would be recursive, contrary to Theorem XIX. He concludes that
In particular, if the system of Principia Mathematica be ω-consistent, its decision problem is unsolvable (1936a [BE: 125]).
Notice that Church appeals to CT1 in the positive form stating that if the problem of deciding whether or not \(A\) converts to \(B\) were solvable, then it would be recursive.
In his (1936b), Church uses the term “Entscheidungsproblem” in the now standard way to refer to the decision problem for first order logic. The proof Church gives of the undecidability of first order logic differs significantly from contemporary textbook proofs. Boolos et al provides no less than three different proofs of this result, all labeled “Church’s theorem”: one appeals to properties of Turing machines, another to properties of primitive recursive functions and a third to properties of the first-order theory \(Q\). Church’s argument most closely resembles the third of these. \(Q\) is both undecidable and finitely axiomatizable. This means that the question whether a sentence \(A\) is a theorem of \(Q\) reduces to the question whether the sentence \(Q* \supset A\) is a theorem of first order logic, where \(Q*\) is the conjunction of the axioms of \(Q\). Hence if first order logic were decidable, \(Q\) would be decidable—and it is not. Similarly, Church makes use of an undecidable and finitely axiomatizable extension of first order logic, but his argument appeals to properties of λ-conversion. Church’s version has yet to find its way into the textbooks.
Finally, it is worth mentioning that Church took himself to have proved only that provability in first-order logic is undecidable. He notes that by the completeness theorem, it follows that validity in first order logic is also undecidable, but Church objected that the completeness theorem is non-constructive in nature and so he couldn’t affirm that the decision problem for validity had been definitively solved. In a note added in 1973 he provides a means of solving the problem that does not appeal to the non-constructive completeness theorem, and in a footnote he remarks that a preference for constructive existence proofs need not involve an appeal to “Brouwerian principles”.
The proof: A unary function \(F\) of positive integers is λ-definable if there is formula \(\stF\) such that, if \(F (m) = r\) and \(\stm\) and \(\str\) are the λ-formulas for which the positive integers \(m\) and \(r\) stand, then \(\{\stF\}(\stm)\) converts to \(\str\). Thus, \(\{\stF\}(\stm) \conv \str\) is the λ-equivalent of \(F (m) = r\), and \(\stm\) and \(\str\) are the λ-formulas representing (or represented by) \(m\) and \(r\). These formulas are defined in (1936a [BE: 113]). See also supplement D. Each such formula is in normal form. That is all one needs to know about them for the proof.
Church first gives the details of his proof (1936a [BE: 122–123]), then gives a more informal outline of it. The following is an outline of the outline. First, Theorem XV asserts that there is an effective enumeration of the formulas that have a normal form—that covert to a formula in normal form. Let \(A_{1}\)…\(A_{n}\)… be such an enumeration. Secondly, assume (for reductio) that there is an effective method for determining whether or not a formula has a normal form. Then, thirdly, there is an effective procedure for determining whether or not a formula has a normal form that is one of the formulas in λ-notation representing positive integers. Call a formula with this property “reducible to a number”. The argument now is that fourth, there is a λ-definable function of positive integers whose λ-definition (1) has a normal form and (2) is not in the complete enumeration \(A_{1}\)…\(A_{n}\)…, and this is a contradiction.
This fourth step breaks down as follows: Define a function \(E\) of positive integers thus:
- \(E(n) = 1\), if \(A_{n}(n)\) is not reducible to a number; and
- \(E(n) = m + 1\), if \(A_{n}(n)\) is convertible to the numerical formula \(\stm\) (and hence reducible to a number).
The function \(E\) is effectively calculable, since it’s been assumed (for reductio) that there is an effective procedure for determining whether or not a formula is reducible to a number. Hence, \(E\) must be λ-definable by a formula \(\ste\)—a direct appeal to Church’s thesis exactly as it is enunciates it in section 7. But \(\ste\) has a normal form since \(\ste(1)\) does. The latter is true since \(\ste(1)\) reduces to a number, whichever clause (a) or (b) of the definition of \(E\) applies. Moreover, suppose that \(\ste\) is in the effective enumeration of formulas having a normal form—say \(\ste\) is the nth such formula, \(A_{n}\). Then \(\ste(n)\) must be the same as \(A_{n}(n)\). But if clause (a) applies, then \(\ste(n)\) converts to 1 but \(A_{n}(n)\) is not reducible to a number. If clause b applies, then \(\ste(n)\) converts to a number one greater than the number \(m\) that \(A_{n}(n)\) converts to. Hence, \(E(n)\) cannot be the same as \(A_{n}(n)\).
Therefore, the set of Gödel numbers of formulas having a normal form is not recursive and so by CT1, its characteristic function is not intuitively computable.
The term “Church’s theorem” is often applied to the result of Church’s (1936b) giving the negative solution to the official Entscheidungsproblem. But sometimes the term is applied to a more general result closer to Theorem XVIII. For example, in Shoenfield (1967: 125), the term is given to the theorem that every consistent extension of the weak first order number theoretic system, \(N\), is undecidable. Shoenfield’s proof of this theorem is only vaguely related (on the surface, anyway) to Church’s proof of Theorem XVIII—both are diagonal arguments. Shoenfield’s argument—like similar arguments in other texts—relies on a prior proof that all recursive functions are representable in \(N\) (or \(Q\)). Church’s proof does not rely on this kind of result (see Rosser 1939; Davis 1965: 227; Rosser explicitly notes that such results are not required for Church’s proof). But it remains to be seen whether Church’s proof can be made to play a more central role than it has in fact played in the textbook development of basic theorems on undecidability. Theorem XVIII plays an important role in Church’s proof in his (1936b), but as mentioned this is ignored in many treatments of the undecidability of first order logic. A detailed study of Church’s proofs in his (1936a) and (1936b) would seem to be desirable.
A.2 Church’s “Step by recursive Step” Argument
Church considers a “symbolic logic” containing notations for equality, application of a unary function of positive integers to its argument, and names for positive integers. He requires that the axioms and rules of inference be effectively enumerable and that the relation between numeral and number be computable. He then suggests that these various metamathematical relations may be “interpreted” to be recursive (via Gödel numbering) and hence that the theorems are recursively enumerable. He then defines a unary function \(f\) of positive integers to be “calculable in the system” if there is an expression \(f\) in the logic such that \(f(u) = v\) is a theorem when and only when \(f(m) = n\), where \(u\) and \(v\) are the names of \(m\) and \(n\) respectively. He concludes that by Theorem IV—which asserts the recursiveness of Kleene’s rho-function now known as the μ-function (which conducts an unbounded search for the least number satisfying some condition), \(f\) must be recursive.
Church has been criticized by Sieg and others for his suggestion that the metamathematical functions required to be intuitively computable (effectively calculable) in the foregoing argument may be “interpreted” to be recursive. Sieg complains that “the crucial interpretive step is not argued for at all!” and that “here we encounter the real stumbling block for Church’s analysis” (1997: 165). Presumably, Sieg will have the same complaint about Kleene’s summary, in his (1952: 323), of Church’s argument—as well as about Kripke’s argument discussed in the text. Both of these arguments assume that the steps of a valid calculation are recursive. Sieg goes on to mention that an argument quite similar to Church’s is given in Hilbert and Bernays (1934), and yet he does not suggest that there is some “stumbling block” to accepting their argument. Church’s argument is that if the provability predicate of a logic is semirecursive, then functions such as f must be recursive; that is, any function “reckonable” in a logic is recursive (Kleene 1952: 323). Of course, the converse can be established too, provided the logic is sufficiently strong. There does not seem to be anything circular or otherwise deficient in this argument.
However, Gandy brings the objection more sharply into focus. He argues that it may seem conceivable that:
an entirely new kind of rule of proof, might proceed by (irreducible) steps which were not recursive. How can one make unassailable predictions about the future development of mathematics? (Turing showed how.) (1992: 73)
The stumbling block, then, is that there might be some totally new kind of proof whose steps are not recursive. Church was well aware of this objection but he did not think that the discovery of such a new rule of proof was a real possibility. In a letter to the Polish logician Pepis, Church makes a vivid appeal to his “step by recursive step” argument. Pepis had submitted a paper to the Journal of Symbolic Logic claiming that there must be intuitively computable functions that are not recursive. Church responded as follows:
I would say at the present time, however, that I have the impression that you do not fully appreciate the consequences which would follow from the construction of an effectively calculable non-recursive function.
For instance, I think I may assume that we are agreed that if a numerical function \(f\) is effectively calculable then for every positive integer \(a\) there must exist a positive integer \(b\) such that a valid proof can be given of the proposition \(f(a) = b\) (at least if we are not agreed on this then our ideas of effective calculability are so different as to leave no common ground for discussion). But it is proved in my paper in the American Journal of Mathematics that if the system of Principia Mathematica is omega-consistent, and if the numerical function \(f\) is not general recursive, then, whatever permissible choice is made of a formal definition of \(f\) within the system of Principia, there must be a positive integer \(a\) such that for no positive integer \(b\) is the proposition \(f(a) = b\) provable within the system of Principia. Moreover, this remains true if instead of the system of Principia we substitute one of the extensions of Principia which have been proposed (e.g., allowing transfinite types), or any one of the forms of the Zermelo set theory, or indeed any system of symbolic logic whatsoever which to my knowledge has ever been proposed.
Therefore, to discover a function which was effectively calculable but not general recursive would imply the discovery of an utterly new principle of logic. (this letter is quoted in full in Sieg 1997; it is not published in BE)
Church’s argument reduces intuitive computability (effective calculability) to a certain restricted kind of deduction in a formal logical system (reckoning, or “calculability within the system” (Kleene 1952)), and then reduces this to general recursion. Church’s quite dramatic conclusion is that if a computable but not recursive function were discovered this would imply the discovery of a “new principle of logic”. Gandy gives a thorough account of Turing’s analysis of computation in terms of the behavior of a human computor, and argues that Turing’s analysis amounts to an informal proof that forecloses the possibility of a computable function that is not Turing computable and hence not recursive; and therefore, presumably, also forecloses the possibility of a totally new kind of rule of logic—one that would not even conform to the standard of informal proof in mathematics. A distinctive feature of Church’s argument, like Kripke’s, is that it focuses on the relation between computability and proof. If \(f\) is not recursive, then while it may be true that \(f(a) = b\), this fact will not be provable in any system of logic of any known type (cf. exercise 15.10 of Boolos, Burgess, & Jeffrey 2007).