Rescuing Foundations of Computation

2 points

5 years ago

[Church 1934] remarked that the assumption that theorems must computationally enumerable leads to inconsistency for a foundational theory T that can axiomatize computation and provability by the following remarkable powerful proof:

    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.