◄ Index 
◄
Main essay
Why Brouwer was right in suggesting that Hilbert’s Law
of the Excluded Middle needed qualification
Interpreting the universal quantifier
Turing-verifiably
Bhupinder Singh Anand[1]
(A .pdf file of this essay before the current update is available at http://arXiv.org/abs/math.GM/0603604)
We
reproduce Hilbert’s axiomatic formalization of Number Theory, and argue that
his enunciation of the Law of the Excluded Middle is inconsistent with a
Turing-verifiable model of the axioms under the standard interpretation.
1. Introduction
In Section 2, p1-9, we reproduce Hilbert’s
axiomatic formalization of Number Theory. In Section 3, p6-7, we vindicate
Brouwer’s objection, to Hilbert’s enunciation of the Law of the Excluded Middle
as a logical principle even for quantified expressions, by showing that this
enunciation is inconsistent with a Turing-verifiable model of Hilbert’s axioms
under the standard interpretation. In Sections 4 and 5, p8-9, we highlight the continuing,
and seemingly removable, ambiguity in current interpretations of classical
theory.
2. Hilbert's formalisation of Number Theory
The following outline of Hilbert's axiomatic formalisation of Number Theory is excerpted from [Hi27].
I shall now present the fundamental idea of my proof theory.
All the propositions that constitute mathematics are converted into formulas, so that mathematics proper becomes an inventory of formulas. These differ from the ordinary formulas of mathematics only in that, besides the ordinary signs, the logical signs:
→ & v ~ (∀x) (∃x)
implies and or not for all there exists
also occur in them. Certain formulas, which serve as building blocks for the formal edifice of mathematics, are called axioms. A proof is an array that must be given as such to our perceptual intuition of it of inferences according to the schema:
Š
Š → Ý
Ý
where each of the premises, that is, the formulae, Š and Š → Ý in the array either is an axiom or follows directly from an axiom by substitution, or else coincides with the end formula of an inference occurring earlier in the proof or results from it by substitution. A formula is said to be provable if it is either an axiom or the end formula of a proof.
The axioms and provable propositions, that is, the formulas resulting from this procedure, are copies of the thoughts constituting customary mathematics as it has developed till now.
Through the program outlined here the choice of axioms for our proof theory is already indicated; we arrange them as follows.
I. Axioms of implication
1. A → (B → A) (introduction of an assumption)
2. (A → (A → B)) → (A → B) (omission of an assumption)
3. (A → (B → C)) → (B → (A → C)) (interchange of assumptions)
4. (B → C) → ((A → B) → (A → C)) (elimination of a proposition)
II. Axioms about & and v
5. A & B → A
6. A & B → B
7. A → (B → A & B)
8. A → A v B
9. B → A v B
10. ((A → C) & (B → C)) → ((A v B) → C))
III. Axioms of negation
11. (A → B & ~B) → ~A (principle of contradiction);
12. ~(~A)) → A (principle of double negation)
The axioms of groups I, II, and III are nothing but the axioms of the propositional calculus. From 11 and 12 there follows, in particular, the formula:
(A & ~(A)) → B
and, further, the logical principle of excluded middle:
((A → B) & (~A → B)) → B
IV. The logical ε-axiom
13. A(a) → A(ε(A))
Here ε(A) stands for an object of which the proposition A(a) certainly holds if it holds of any object at all; let us call ε the logical ε-function. To elucidate the role of the logical ε-function let us make the following remarks.
In the formal system the ε-function is used in three ways.
1. By means of ε, “all” and “there exists” can be defined, namely, as follows:
(∀a) A(a) ↔ A(ε(~A))
(∃a) A(a) ↔ A(ε(A))
Here the double arrow (↔) stands for a combination of two implication formulas; in its place we shall henceforth use the "equivalence" sign (≡).
On the basis of this definition the ε-axiom IV(13) yields the logical relations that hold for the universal and the existential quantifier, such as:
(∀a) A(a) → A(b) (Aristotle's dictum),
and:
~((∀a) A(a)) → (∃a)(~A(a)) (principle of excluded middle).
2. If a proposition Y holds of one and only one object, then ε(Y) is the object of which Y(a) holds.
The ε-function thus enables us to resolve a proposition such as Y(a), when it holds of only one object, so as to obtain:
a = ε(Y)
3. Beyond this, ε takes on the role of the choice function; that is, in case A(a) holds of several objects, ε(Y) is some one of the objects a of which Y(a) holds.
In addition to these purely logical axioms we have the following specifically mathematical axioms.
V. Axioms of equality
14. a = a
15. (a = b) → (A(a) → A(b))
VI. Axioms of Number
16. a' ≠ 0; (≠ for “not =”)
17. (A(0) & (∀a) (A(a) → A(a'))) → A(b)
(principle of mathematical induction).
Here a' denotes the number following and the integers 1, 2, 3, . . . can be written in the form 0', 0'', 0''', ...
3. Why Brouwer was right
Now, instead of using Hilbert’s ε-function to define the standard interpretations of the universal and existential quantifiers, ‘(∀x)’ and ‘(∃x)’, we consider the case where, under the standard interpretation:
(i) ‘(∀x)’ is interpreted directly as ‘(There is an algorithm T such that, for any given x, T verifies …)’;
(ii) ‘(∃x)’ is defined as ‘~(∀x)~’, and interprets as ‘(There is no algorithm T such that, for any given x, T falsifies …)’
Under the above interpretation, all of Hilbert's axioms for Number Theory, including the induction axiom (the only one involving a quantifier) can be seen to interpret as not only intuitively true, but also intuitively Turing-verifiable, under the standard interpretation.
The system, thus, has an intuitively verifiable model under the standard interpretation, and, so, is intuitively consistent constructively.
However, although the ε-axiom IV(13) yields a logical relation that holds intuitively for the universal quantifier, namely:
(∀a) A(a) → A(b) (Aristotle's dictum)
the principle of the excluded middle, as enunciated by Hilbert, does not necessarily follow.
Thus, from ~((∀a) A(a)), we may only conclude that there is no algorithm such that, for any given a, A(a) holds.
As Gödel has shown [Go31a], if the system is ω-inconsistent[2], then we cannot exclude the possibility of a meta-proof that, first, A(a) is a logical consequence of the axioms of such a theory for any given a, and that, second, ~((∀a)A(a)), too, is a logical consequence of the axioms.
So, even if for variously stated reasons, Brouwer was, after all, essentially right in objecting to Hilbert's unconditional postulation of the principle of the excluded middle as a ‘logical’ consequence, namely, the implication:
~((∀a) A(a)) → (∃a)(~A(a)).
It is implicit in the objection that, if we assume only simple consistency for Hilbert's system, then we cannot unconditionally define “there exists” intuitively, under the standard interpretation, as:
(∃a) A(a) ↔ A(ε(A)).
This definition implies that the system is ω-consistent. Such a postulation through definition is not only not self-evident, it is also not apparent as being an explicit, or even implicit, condition in Hilbert’s formalization of a verifiable Number Theory, at least in 1927[3].
4. Current interpretations of classical theory
Current interpretations of classical theory, avoiding the explicitly ambiguous - and implicitly Platonic - use of Hilbert’s ε-function, define (∃a) more straightforwardly by the formal equivalence:
(∃a) A(a) ↔ ~((∀a) ~A(a)).
However, following Hilbert, they continue to deny the validity of Brouwer's objection by, implicitly, interpreting the above as A(ε(A)), in Hilbert's sense, under the standard interpretation[4].
Whether intentional or not, it is such implicit interpretation that tolerates the curious – and intuitionistically objectionable - inference of A(ε(A)) from ~((∀a)~A(a)) as a valid step in the formalization of Rosser's proof that Gödelian undecidability can be deduced in a simply consistent Peano Arithmetic ([Me64], p146, (i)(1)-(i)(4)), even though the Arithmetic does not have an axiom corresponding to Hilbert’s ‘(∃a) A(a) ↔ A(ε(A))’!
5. Conclusions
If we admit the above analysis as (possibly, implicitly) underlying Brouwer's reluctance to accept the unqualified postulation of the Law of the Excluded Middle as a logical consequence, then the choice is between an omega-inconsistent system in which the universal quantifier can be interpreted Turing-verifiably, and an omega-consistent system that is inconsistent with such an interpretation.
Clearly, if we are to abide faithfully by the principle of Occam's razor, the former must be preferred as being more in harmony with, not only Hilbert's stated goal of a verifiable proof theory, but also with current requirements and interpretations of Computability Theory.
So, despite the philosophical positions taken in their dispute over it, Brouwer's objections to the Law of the Excluded Middle should, thus, be viewed as furthering Hilbert's goal, rather than hindering it.
Moreover, we may need to review standard interpretations of classical theory to make them consistent with a Turing-verifiable interpretation of the universal quantifier, ‘(∀x)’, as ‘(There is an algorithm T such that, for any given x, T verifies …)’.
References
[Go31a] Gödel,
Kurt. 1931. On formally undecidable propositions of Principia Mathematica
and related
[Hi27] Hilbert, David. 1927. The Foundations of Mathematics. Reproduced in ‘The Emergence of Logical Empiricism’. 1996. Garland Publishing Inc.
Reference and quoted passages excerpted (with minor corrections) from the archived paper at:
http://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm
[Hi30] Hilbert, David. 1930. Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen.
Vol. 104 (1930), pp. 485–494. Reprinted in Gesammelte abhandlungen. Vol. 3. 1935.
Springer,
Reference and quoted passages
excerpted from W. W. Tait. Remarks on Finitism. In ‘Reflections on the Foundations of Mathematics:
Essays in honor of Solomon Feferman’. Ed. Wilfried Sieg and Richard Sommer and Carolyn Talcott.
http://home.uchicago.edu/~wwtx/finitism.pdf
[Me64] Mendelson,
Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand,
(Created:
