Alonzo Church made major contributions to foundations by creating the lambda calculus and proving the computational undecidability of whether an expression halts. In 1934, he published a remarkable article in which proclaimed that he had discovered a contradiction in foundations that meant the end of his field as follows:
[Church 1934] noted 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 contradiction in the Church/Turing theory of computation 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.”
In other words, the argument in [Church 1934] is so powerful that it meant the end of logic!
Left unresolved the contradiction could provide the basis for cyberattacks as explained here:
“Epistemology Cyberattacks”
https://papers.ssrn.com/abstract=3603021
Fortunately, there is a better use for [Church 1934] as follows: it can be adapted to construct a true but unprovable proposition in foundations (instead of the nonexistent one proposed in [Gödel 1931]). Used in this way, [Church 1934] makes a fundamental contribution to foundations instead of demolishing the possibility of foundations as [Church 1934] concluded.
