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:

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 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.

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.

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.

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.

Not strictly intuitionistic, but very constructive.

Founder: J. Girard (1987)^[7]

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.

• 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.

• Constructivism (philosophy of mathematics)

• 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) . "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.