#### 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 Mathematicabe ω-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 *n*th 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 Mathematicsthat 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).