Editing Law of excluded middle (section)

=== Formalists versus Intuitionists ===
From the late 1800s through the 1930s, a bitter, persistent debate raged between Hilbert and his followers versus [[Hermann Weyl]] and [[L. E. J. Brouwer]]. Brouwer's philosophy, called [[intuitionism]], started in earnest with [[Leopold Kronecker]] in the late 1800s.

Hilbert intensely disliked Kronecker's ideas:

{{quote|Kronecker insisted that there could be no existence without construction. For him, as for Paul Gordan [another elderly mathematician], Hilbert's proof of the finiteness of the basis of the invariant system was simply not mathematics. Hilbert, on the other hand, throughout his life was to insist that if one can prove that the attributes assigned to a concept will never lead to a contradiction, the mathematical existence of the concept is thereby established (Reid p. 34)}}

{{quote|It was his [Kronecker's] contention that nothing could be said to have mathematical existence unless it could actually be constructed with a finite number of positive integers (Reid p. 26)}}

The debate had a profound effect on Hilbert. Reid indicates that [[Hilbert's second problem]] (one of [[Hilbert's problems]] from the Second International Conference in Paris in 1900) evolved from this debate (italics in the original):

::In his second problem, [Hilbert] had asked for a ''mathematical proof'' of the consistency of the axioms of the arithmetic of real numbers.
::To show the significance of this problem, he added the following observation:
::"If contradictory attributes be assigned to a concept, I say that ''mathematically the concept does not exist''" (Reid p. 71)

Thus, Hilbert was saying: "If ''p'' and ~''p'' are both shown to be true, then ''p'' does not exist", and was thereby invoking the law of excluded middle cast into the form of the law of contradiction.

{{quote|And finally constructivists … restricted mathematics to the study of concrete operations on finite or potentially (but not actually) infinite structures; completed infinite totalities … were rejected, as were indirect proof based on the Law of Excluded Middle. Most radical among the constructivists were the intuitionists, led by the erstwhile topologist L. E. J. Brouwer (Dawson p. 49)}}

The rancorous debate continued through the early 1900s into the 1920s; in 1927 Brouwer complained about "polemicizing against it [intuitionism] in sneering tones" (Brouwer in van Heijenoort, p.&nbsp;492). But the debate was fertile: it resulted in ''[[Principia Mathematica]]'' (1910–1913), and that work gave a precise definition to the law of excluded middle, and all this provided an intellectual setting and the tools necessary for the mathematicians of the early 20th century:

{{quote|Out of the rancor, and spawned in part by it, there arose several important logical developments; Zermelo's axiomatization of set theory (1908a), that was followed two years later by the first volume of ''Principia Mathematica'', in which Russell and Whitehead showed how, via the theory of types: much of arithmetic could be developed by logicist means (Dawson p. 49)}}

Brouwer reduced the debate to the use of proofs designed from "negative" or "non-existence" versus "constructive" proof:
::According to Brouwer, a statement that an object exists having a given property means that, and is only proved, when a method is known which in principle at least will enable such an object to be found or constructed …
::Hilbert naturally disagreed.
::"pure existence proofs have been the most important landmarks in the historical development of our science," he maintained. (Reid p. 155)

::Brouwer refused to accept the logical principle of the excluded middle, His argument was the following:

::"Suppose that A is the statement "There exists a member of the set ''S'' having the property ''P''." If the set is finite, it is possible—in principle—to examine each member of ''S'' and determine whether there is a member of ''S'' with the property ''P'' or that every member of ''S'' lacks the property ''P''." For finite sets, therefore, Brouwer accepted the principle of the excluded middle as valid. He refused to accept it for infinite sets because if the set ''S'' is infinite, we cannot—even in principle—examine each member of the set. If, during the course of our examination, we find a member of the set with the property ''P'', the first alternative is substantiated; but if we never find such a member, the second alternative is still not substantiated.
::Since mathematical theorems are often proved by establishing that the negation would involve us in a contradiction, this third possibility which Brouwer suggested would throw into question many of the mathematical statements currently accepted.
::"Taking the Principle of the Excluded Middle from the mathematician," Hilbert said, "is the same as … prohibiting the boxer the use of his fists."
::"The possible loss did not seem to bother Weyl … Brouwer's program was the coming thing, he insisted to his friends in Zürich." (Reid, p. 149)

In his lecture in 1941 at Yale and the subsequent paper, [[Gödel]] proposed a solution: "that the negation of a universal proposition was to be understood as asserting the existence … of a counterexample" (Dawson, p.&nbsp;157)

Gödel's approach to the law of excluded middle was to assert that objections against "the use of 'impredicative definitions{{'"}} had "carried more weight" than "the law of excluded middle and related theorems of the propositional calculus" (Dawson p.&nbsp;156). He proposed his "system Σ … and he concluded by mentioning several applications of his interpretation. Among them were a proof of the consistency with [[intuitionistic logic]] of the principle ~ (∀A: (A ∨ ~A)) (despite the inconsistency of the assumption ∃ A: ~ (A ∨ ~A))" (Dawson, p.&nbsp;157)

The debate seemed to weaken: mathematicians, logicians and engineers continue to use the law of excluded middle (and double negation) in their daily work.