Intuitionistic Logic and Constructivism
Intuitionistic logic rejects the law of excluded middle, holding that a mathematical statement is true only if we can construct a proof of it.
Definition
Intuitionistic logic is the logic of constructive proof, in which a disjunction requires a proof of one disjunct and an existential claim requires a construction of a witness, so that excluded middle and proof by contradiction for existence claims are not generally valid.
Scope
This topic covers intuitionistic logic and the constructivist philosophy of mathematics that motivates it. It treats Brouwer's view of mathematics as mental construction, Heyting's formalization and the proof-conditional (BHK) interpretation of the connectives, the failure of excluded middle and double-negation elimination, the Kripke and topological semantics for intuitionistic logic, and Dummett's meaning-theoretic argument that anti-realism about truth supports intuitionistic logic generally.
Core questions
- Why should the law of excluded middle fail, and for which statements?
- What is the constructive interpretation of the logical connectives?
- Is the case for intuitionism specifically mathematical, or does it generalize via the theory of meaning?
- How do Kripke and topological models illuminate intuitionistic validity?
Key concepts
- law of excluded middle
- constructive proof
- BHK interpretation
- double-negation translation
- Kripke models for intuitionism
- verificationism
Key theories
- BHK (proof-conditional) interpretation
- The Brouwer-Heyting-Kolmogorov interpretation explains each connective by what counts as a proof of a compound statement, so that 'A or B' requires a proof of A or a proof of B, which blocks unrestricted excluded middle.
- Dummett's anti-realist argument
- Dummett argues that a theory of meaning constrained by what speakers can manifest favours verification-conditional over truth-conditional semantics, and that this anti-realism mandates intuitionistic logic across the board, not just in mathematics.
History
Brouwer founded intuitionism in the 1900s-1920s as a constructivist rejection of classical mathematics; Heyting formalized intuitionistic logic in 1930. Kolmogorov's calculus of problems and the BHK interpretation clarified its meaning, Kripke later supplied a relational semantics, and Dummett recast intuitionism as a general consequence of semantic anti-realism.
Debates
- Does anti-realism generalize intuitionism beyond mathematics?
- Whether Dummett's meaning-theoretic argument successfully extends the case for intuitionistic logic from mathematics to discourse in general, or whether the original motivation is essentially tied to the constructive nature of mathematical objects.
Key figures
- L. E. J. Brouwer
- Arend Heyting
- Michael Dummett
- Andrey Kolmogorov
- Per Martin-Lof
Related topics
Seminal works
- heyting1956
- dummett2000
Frequently asked questions
- Does intuitionistic logic reject all proofs by contradiction?
- Not all. Intuitionists accept proving a negation by deriving a contradiction from the assumption, since that is how negation is defined. What they reject is establishing a positive existence or disjunction claim merely by refuting its negation, because that yields no constructive witness and relies on double-negation elimination, which is not intuitionistically valid.