Proof of the law of excluded middle extended to the infinite

Proof

Brouwer viewed this loss of constructibility as bad, but worse when applied to a generalized "proof of consistency" for all of mathematics. In his 1900 address Hilbert had specified, as the second of his 23 problems for the twentieth century, the quest for a generalized proof of (procedure for determining) the consistency of the axioms of arithmetic. Hilbert, unlike Brouwer, believed that the formalized notion of mathematical induction could be applied in the search for the generalized consistency proof.

If this proof/procedure P was found, given any arbitrary mathematical theorem T (formula, procedure, proof) put to P (thus P(T)) including P itself (thus P(P)), P would determine conclusively whether or not the theorem T (and P) was provable – i.e. derivable from its premises, the axioms of arithmetic. Thus for all T, T would be provable by P or not provable by P and under all conditions (i.e. for any assignment of numerical values to T's variables). This requires the use of the Law of Excluded Middle extended over the infinite, in fact extended twice – first over all theorems (formulas, procedures, proofs) and secondly for a given theorem, for all assignment of its variables. This point, missed by Hilbert, was first pointed out to him by Poincaré and later by Weyl in his 1927 comments on Hilbert's lecture: "For after all Hilbert, too, is not merely concerned with, say 0' or 0' ', but with any 0'^... ', with an arbitrarily concretely given numeral. One may here stress the "concretely given"; on the other hand, it is just as essential that the contentual arguments in proof theory be carried out in hypothetical generality, on any proof, on any numeral. ... It seems to me that Hilbert's proof theory shows Poincaré to have been completely right on this point."

In his discussion preceding Weyl's 1927 comments, van Heijenoort explains that Hilbert insisted that he had addressed the issue of "whether a formula, taken as an axiom, leads to a contradiction, the question is whether a proof that leads to a contradiction can be presented to me".

"But [writes van Heijenoort] in a consistency proof the argument does not deal with one single specific formula; it has to be extended to all formulas. This is the point that Weyl has in mind ... ."

Given such a generalized proof, all mathematics could be replaced by an automaton consisting of two parts: (i) a formula-generator to create formulas one after the other, followed by (ii) the generalized consistency proof, which would yield "Yes – valid (i.e. provable)" or "No – not valid (not provable)" for each formula submitted to it (and every possible assignment of numbers to its variables). In other words: mathematics would cease as a creative enterprise and become a machine.