Constructive logic
Constructive logic is a family of logics where proofs must be constructive (i.e., proving something means one must build or exhibit it, not just argue it "must exist" abstractly). No "non-constructive" proofs are allowed (like the classic proof by contradiction without a witness).
The main constructive logics are the following:
1. Intuitionistic logic
[edit ]Founder: L. E. J. Brouwer (1908, philosophy)[1] [2] formalized by A. Heyting (1930)[3] and A. N. Kolmogorov (1932)[4]
Key Idea: Truth = having a proof. One cannot assert "{\displaystyle P} or not {\displaystyle P}" unless one can prove {\displaystyle P} or prove {\displaystyle \neg \neg P}.
Features:
- No law of excluded middle ({\displaystyle P\lor \neg P} is not generally valid).
- No double negation elimination ({\displaystyle \neg \neg \ P\to P} is not valid generally).
- Implication is constructive: a proof of {\displaystyle P\to Q} is a method turning any proof of P into a proof of Q.
Used in: type theory, constructive mathematics.
2. Modal logics for constructive reasoning
[edit ]Founder(s):
- K F. Gödel (1933) showed that intuitionistic logic can be embedded into modal logic S4.[5]
- (other systems)
Interpretation (Gödel): {\displaystyle \Box P} means "{\displaystyle P} is provable" (or "necessarily {\displaystyle P}" in the proof sense).
Further: Modern provability logics build on this.
3. Minimal logic
[edit ]Simpler than intuitionistic logic.
Founder: I. Johansson (1937)[6]
Key Idea: Like intuitionistic logic but without assuming the principle of explosion (ex falso quodlibet, "from falsehood, anything follows").
Features:
- Doesn’t automatically infer any proposition from a contradiction.
Used for: Studying logics without commitment to contradictions blowing up the system.
4. Intuitionistic type theory (Martin-Löf type theory)
[edit ]Founder: P. E. R. Martin-Löf (1970s)
Key Idea: Types = propositions, terms = proofs (this is the Curry–Howard correspondence).
Features:
- Every proof is a program (and vice versa).
- Very strict — everything must be directly constructible.
Used in: Proof assistants like Rocq, Agda.
5. Linear logic
[edit ]Not strictly intuitionistic, but very constructive.
Key Idea: Resource sensitivity — one can only use an assumption once unless one specifically says it can be reused.
Features:
- Tracks "how many times" one can use a proof.
- Splits conjunction/disjunction into multiple types (e.g., additive vs. multiplicative).
Used in: Computer science, concurrency, quantum logic.
6. Other Constructive Systems
[edit ]- Constructive set theory (e.g., CZF — Constructive Zermelo–Fraenkel set theory): Builds sets constructively.
- Realizability Theory : Ties constructive logic to computability — proofs correspond to algorithms.
- Topos Logic : Internal logics of topoi (generalized spaces) are intuitionistic.
See also
[edit ]Notes
[edit ]- ^ Brouwer 1908.
- ^ Brouwer 1913.
- ^ Heyting 1930.
- ^ Kolmogorov 1932.
- ^ Gödel 1986, pp. 300–302.
- ^ Johansson 1937.
- ^ Girard 1987.
References
[edit ]- Berka, Karel; Kreiser, Lothar, eds. (1986). Logik-Texte. De Gruyter. doi:10.1515/9783112645826. ISBN 978-3-11-264582-6.
- Brouwer, Luitzen Egbertus Jan (1908). Over de Grondslagen der Wiskunde (in Dutch). N.V. Uitgeversmaatschappij Sijthoff.
- Brouwer, Luitzen Egbertus Jan (1913). "Intuitionism and Formalism" (PDF). Bulletin of the American Mathematical Society . 19 (6): 191–194.
- Girard, Jean-Yves (1987). "Linear logic". Theoretical Computer Science. 50 (1). Elsevier: 1–101. doi:10.1016/0304-3975(87)90045-4 .
- Gödel, Kurt (1986) [1933]. "Eine Interpretation des intuitionistischen Aussagenkalkiils". In Feferman, Solomon; Dawson, Jr., John W.; Kleene, Stephen C.; Moore, Gregory H.; Solovay, Robert M.; Van Heijenoort, Jean (eds.). Publications 1929–1936 (PDF). Collected Works. Vol. I. New York: Oxford University Press. ISBN 978-0-19-503964-1. / Paperback: ISBN 978-0-19-514720-9
- Heyting, Arend (1930). "Die formalen Regeln der intuitionistischen Logik". Sitzungsberichte der preußischen Akademie der Wissenschaften, phys.-math. Klasse (in German): 42–56, 57–71, 158–169. OCLC 601568391.
(abridged reprint in Berka & Kreiser 1986, pp. 188–192)
- Johansson, Ingebrigt (1937). "Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus". Compositio Mathematica (in German). 4: 119–136.
- Kolmogorov, Andrey (1932). "On the Principle of Excluded Middle". Mathematical Logic Quarterly. 10: 65–74.