In order to obtain a contradiction,
hypothesize theorems of a foundational theory
T are computationally enumerable. Then
procedures that are provably total in T are
computationally by a procedure that is
provably total in T. Consider the Boolean
procedure Diagonal defined on natural number
input n to be the result of the complement of
the result of the ith provably total
procedure on input i. The procedure Diagonal
differs from every procedure in the
enumeration of provably total procedures in
T. However, by construction, diagonal is a
provably total procedure in T, which is a
contradiction.
The dilemma led Church to conclude the following:
“Indeed, if there is no formalization of logic as a whole [theorems are not computationally enumerable], then there is no exact description of what logic is, for it is in the very nature of an exact description that it implies a formalization. And if there no exact description of logic, then there is no sound basis for supposing that there is such a thing as logic.”The argument in [Church 1934] is so powerful that [Church 1934] expressed the view that it meant the end of logic. Fortunately, there is a better use for Church's argument as follows:
Using a more powerful theory than Church/Turing computing,
[Church 1934] can be turned around to construct a true
but unprovable proposition in foundations (instead of the
nonexistent one proposed in [Gödel 1931]).
Used in this way, the argument in [Church 1934] makes a fundamental contribution to foundations instead of demolishing the possibility of foundations as [Church 1934] concluded.