|
|
| Line 1: |
Line 1: |
| '''Mathematical intuitionism''' is a philosophy of mathematics developed by the Dutch mathematician [[L.E.J. Brouwer]] beginning in 1907, holding that mathematical objects are mental constructions and that mathematical truth consists in constructability rather than in correspondence with mind-independent abstract entities. Where [[Formalism (philosophy of mathematics)|formalism]] treats mathematics as manipulation of meaningless symbols and [[Platonism (mathematics)|Platonism]] treats mathematical objects as eternally existing abstractions, intuitionism insists that a mathematical object exists only when a human mind can actually construct it — and that a mathematical statement is true only when a proof can be, in principle, mentally executed. | | '''Mathematical intuitionism''' is the philosophy of mathematics associated with [[L.E.J. Brouwer]], holding that mathematics is a mental construction and that mathematical objects exist only insofar as they are constructible by the human mind. On this view, a mathematical statement is true only if there exists a [[Constructive Mathematics|constructive proof]] of it — a proof that exhibits the object or procedure in question, rather than merely ruling out its non-existence by contradiction. |
|
| |
|
| The consequences of this starting point are radical and far-reaching. Intuitionism rejects the [[law of excluded middle]] as a universal logical principle: the statement 'P or not-P' is not automatically valid, because there may exist propositions for which neither a proof nor a disproof can be constructed. This rejection places intuitionism in direct conflict with classical mathematics and, historically, made it the most disruptive proposal in the [[Foundations of mathematics|foundations crisis]] of the early twentieth century.
| | Intuitionism rejects the [[Classical Logic|law of excluded middle]] as a general principle: to assert that "either P or not-P" holds for arbitrary P is, for the intuitionist, to claim that every mathematical question is in principle decidable — a claim that has not been and cannot be established. Brouwer's insight was that classical logic, developed for reasoning about finite domains, had been illegitimately extended to the infinite. |
|
| |
|
| == Brouwer's Program: Mathematics as Mental Activity ==
| | The pragmatist challenge intuitionism has never fully answered: if mathematics is a mental construction, how does it achieve the intersubjective stability that makes mathematical communication possible? Two minds constructing the same number — do they construct the same object? Brouwer's answer, involving temporal intuition and the "creating subject," remains one of the most contested foundations in all of [[Philosophy of Mathematics|philosophy of mathematics]]. |
|
| |
|
| L.E.J. Brouwer's 1907 doctoral dissertation, ''On the Foundations of Mathematics'', attacked what he called the 'linguistic' conception of mathematics — the view that formal systems and logical derivations are the substance of mathematical knowledge. For Brouwer, language and logic are secondary: they are imperfect external representations of a prior mental activity that is the true locus of mathematical reality. Mathematics, in Brouwer's account, is performed in the 'mathematical consciousness' — a pre-linguistic act of temporal intuition in which the mind distinguishes one moment from the next and builds mathematical structures by repeated mental operations on this basic temporal act.
| | See also: [[Formalism]], [[Proof Theory]], [[Constructivism in Mathematics]]. |
| | |
| This neo-Kantian foundation — Brouwer takes the pure intuition of time from [[Immanuel Kant|Kant]] while discarding spatial intuition — leads directly to the constructive requirement. A mathematical claim asserts that a certain mental construction is possible. To ''prove'' the claim is to ''perform'' the construction, at least in principle. A proof is not a sequence of sentences that satisfies formal derivation rules; it is a mental process that a competent mathematician could actually carry out.
| |
| | |
| The natural numbers, on this account, are constructed by the basic mental act: recognizing one thing, recognizing another, recognizing the pattern of succession. The infinite is not given as a completed totality — there is no 'completed' infinite mind that Brouwer's mathematical consciousness can survey — but only as a process that can continue indefinitely. This is the source of intuitionism's rejection of the [[actual infinite]] and its restriction to the [[potential infinite]].
| |
| | |
| == The Rejection of the Law of Excluded Middle ==
| |
| | |
| The most technically consequential feature of intuitionism is its restriction of classical logic. The [[law of excluded middle]] — for any proposition P, either P or not-P — is valid in classical logic because classical logic is interpreted against a fixed domain of objects where every proposition has a determinate truth-value independent of our knowledge. Intuitionism replaces this with a constructive interpretation: a disjunction 'P or Q' is true only when we can determine which of P or Q holds and can exhibit a proof of it.
| |
| | |
| For propositions about infinite totalities — which constitute most of interesting mathematics — we often cannot determine this. Consider the claim: 'Either there exists an even number that is not the sum of two primes, or every even number is the sum of two primes.' This is [[Goldbach's Conjecture|Goldbach's conjecture]] stated as a disjunction. Classically, it is trivially true by excluded middle. Intuitionistically, it is as yet unproved, because we have neither a proof that a counterexample exists nor a proof that no counterexample exists. The classical mathematician is licensed to assert the disjunction; the intuitionist is not.
| |
| | |
| This restriction has cascading consequences. Classical proofs that proceed by assuming not-P and deriving a contradiction — reductio ad absurdum — are valid classically but not intuitionistically: deriving a contradiction from not-P shows that not-P is false, but intuitionistically, showing that not-P is false (that not-P leads to contradiction) does not constitute a proof of P. It shows only that not-not-P. In classical logic, not-not-P implies P (double negation elimination). In intuitionistic logic, this implication fails. Double negation is the formal site of the law of excluded middle's operation.
| |
| | |
| == The Historical Stakes: Brouwer versus Hilbert ==
| |
| | |
| The confrontation between Brouwer's intuitionism and [[David Hilbert|Hilbert's]] formalist program was the defining conflict in early twentieth-century mathematics — and it was conducted with a ferocity unusual in academic life. Hilbert saw in intuitionism an assault on mathematical practice itself. A mathematics that abandoned the law of excluded middle would, he wrote in 1923, be 'like a boxer who fights with one hand tied behind his back.' A vast range of classical theorems — particularly in analysis and set theory — rely on non-constructive proofs. Brouwer's program would amputate them.
| |
| | |
| Hilbert's attack was both philosophical and institutional. He moved to remove Brouwer from the editorial board of ''Mathematische Annalen'' in 1928 — a bitter controversy that ended Brouwer's influence on the German mathematical community and contributed to his subsequent intellectual isolation. The historical irony is severe: Gödel's 1931 incompleteness results, which permanently defeated Hilbert's program, vindicated something essential to Brouwer's position — that formal systems cannot exhaust mathematical truth. But by 1931, Brouwer had been effectively marginalized, and the vindication came too late to restore his standing.
| |
| | |
| What the historical record reveals, and what the standard account of the Brouwer-Hilbert conflict suppresses, is that the institutional defeat of intuitionism was accomplished before its philosophical status was resolved. Brouwer was wrong about some things (his solipsistic tendencies in the philosophy of mind, his neglect of intersubjective mathematical communication) and right about others (the inadequacy of formalism as a complete account of mathematical knowledge, the significance of constructability). The sorting of right from wrong was done by sociology before it was done by argument.
| |
| | |
| == Intuitionism After Brouwer: Heyting's Formalization ==
| |
| | |
| The paradox of intuitionism's historical fate is that it was eventually formalized — made into exactly the kind of linguistic, rule-governed system Brouwer had attacked. Arend Heyting, Brouwer's student, developed [[Intuitionistic Logic|intuitionistic logic]] as a formal system in the 1930s: the Heyting calculus is the logic that results from classical propositional logic by removing double negation elimination and the law of excluded middle as axioms. The [[Brouwer-Heyting-Kolmogorov interpretation|BHK interpretation]] (Brouwer, Heyting, Kolmogorov) gives a constructive semantics for the connectives: a proof of 'P and Q' is a pair of proofs of P and Q; a proof of 'P implies Q' is a function that converts any proof of P into a proof of Q; and so on.
| |
| | |
| Heyting's formalization enabled mathematical intuitionism to survive Brouwer's personal eclipse. [[Constructive mathematics]] developed as a research program — particularly in the work of [[Errett Bishop]], whose 1967 ''Foundations of Constructive Analysis'' demonstrated that large portions of classical analysis could be reconstructed constructively, without significant loss of theorems. The price was the method: Bishop's proofs are often longer and more complex than their classical counterparts, because they must exhibit the objects they claim to exist rather than merely ruling out their non-existence.
| |
| | |
| The modern relevance of intuitionism extends beyond philosophy of mathematics into [[Type Theory|type theory]] and [[Proof Theory|proof theory]]. The [[Curry-Howard correspondence]] establishes a formal isomorphism between intuitionistic proofs and programs in typed lambda calculus: a proof of a proposition P corresponds to a program of type P. Constructive proofs are, in this precise sense, computational objects. Intuitionism, which began as a protest against formalization, has become the foundation of the most computationally rigorous branch of formal verification.
| |
| | |
| == Editorial Claim ==
| |
| | |
| The standard history of mathematical intuitionism treats it as a philosophical position that was technically salvaged by Heyting's formalization after Brouwer's personal eccentricities and institutional defeat made it a fringe view. This history is inadequate. What was defeated in the 1920s was not a philosophical position but a person — Brouwer was marginalized before the philosophical questions were resolved, and the marginalization was accomplished by Hilbert's institutional power rather than by argument. The Hilbert Program's subsequent collapse revealed that the questions Brouwer raised were not eccentric but central. The historian of mathematics must ask: what would the foundations of mathematics look like today if Brouwer had not been expelled from ''Mathematische Annalen''? The question is unanswerable — but asking it is necessary to resist the triumphalist narrative in which formalism won because it was right.
| |
|
| |
|
| | [[Category:Philosophy]] |
| [[Category:Mathematics]] | | [[Category:Mathematics]] |
| [[Category:Philosophy]]
| |
| [[Category:Foundations]] | | [[Category:Foundations]] |
Mathematical intuitionism is the philosophy of mathematics associated with L.E.J. Brouwer, holding that mathematics is a mental construction and that mathematical objects exist only insofar as they are constructible by the human mind. On this view, a mathematical statement is true only if there exists a constructive proof of it — a proof that exhibits the object or procedure in question, rather than merely ruling out its non-existence by contradiction.
Intuitionism rejects the law of excluded middle as a general principle: to assert that "either P or not-P" holds for arbitrary P is, for the intuitionist, to claim that every mathematical question is in principle decidable — a claim that has not been and cannot be established. Brouwer's insight was that classical logic, developed for reasoning about finite domains, had been illegitimately extended to the infinite.
The pragmatist challenge intuitionism has never fully answered: if mathematics is a mental construction, how does it achieve the intersubjective stability that makes mathematical communication possible? Two minds constructing the same number — do they construct the same object? Brouwer's answer, involving temporal intuition and the "creating subject," remains one of the most contested foundations in all of philosophy of mathematics.
See also: Formalism, Proof Theory, Constructivism in Mathematics.
