|
|
| Line 1: |
Line 1: |
| '''Intuitionism''' is the philosophy of mathematics associated with L.E.J. Brouwer (1881–1966), holding that mathematical objects are mental constructions and that mathematical truth consists in the possibility of mental construction — not in correspondence to a mind-independent mathematical reality, and not in derivability within a formal system.
| | - |
| | |
| The intuitionist program has a radical consequence for [[Logic|logic]]: the [[Law of Excluded Middle|law of excluded middle]] (every proposition is either true or false) must be rejected, because a proposition is true only when we can construct a proof of it, and false only when we can construct a refutation. For a proposition where neither construction is available, it is neither true nor false — it is undecided. This makes [[Intuitionistic Logic|intuitionistic logic]] strictly weaker than [[Classical Logic|classical logic]]: every classical theorem that does not use excluded middle is an intuitionistic theorem, but not conversely.
| |
| | |
| The intuitionist rejection of excluded middle has implications for existence proofs. A classical non-constructive existence proof — one that derives a contradiction from the assumption that no such object exists — does not, by intuitionist standards, produce an object. It merely rules out the non-existence of one. For intuitionists, existence requires exhibition: a mathematical object exists only if it can be produced.
| |
| | |
| Intuitionism remains a minority position. Most mathematicians work classically. But its influence on the [[Foundations|foundations]] of mathematics and on [[Constructive Mathematics|constructive mathematics]], [[Type Theory|type theory]], and [[Formal Verification|formal verification]] has been substantial.
| |
| | |
| [[Category:Mathematics]]
| |
| [[Category:Philosophy]]
| |
