Constructive Mathematics
Overview
Mathematics that requires explicit constructions; rejects the law of excluded middle for infinite domains. Brouwer (1907) founded intuitionism; Heyting formalized intuitionistic logic.
Era: 1907–
Proposed at: Amsterdam, Netherlands
Formal structure
Domain: Proof p; proposition P; p proves P ⟺ p : P (type)
¬¬P ⟹ P rejected for infinite P; ∃x.P(x) ⟹ witness t with P(t)
Constraints: No excluded middle: P ∨ ¬P not assumed; choice sequences (Brouwer)
Objective: Constructive proofs; extract algorithms from proofs