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

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 “ $P$ or not $P$ ” unless one can prove $P$ or prove $\neg \neg P$ .

Features:

No law of excluded middle ( $P\lor \neg P$ is not generally valid).
No double negation elimination ( $\neg \neg \ P\to P$ is not valid generally).
Implication is constructive: a proof of $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

Founder(s):

K F. Gödel (1933) showed that intuitionistic logic can be embedded into modal logic S4.^[5]
(other systems)

Interpretation (Gödel): $\Box P$ means “ $P$ is provable” (or “necessarily $P$ ” in the proof sense).

Further: Modern provability logics build on this.

3. Minimal logic

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)

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 Coq, Agda.

5. Linear logic

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.

6. Other Constructive Systems

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.

Notes

^ Brouwer 1908.
^ Brouwer 1913.
^ Heyting 1930.
^ Kolmogorov 1932.
^ Gödel 1986, pp. 300–302.
^ Johansson 1937.
^ Girard 1987.

References

Berka, Karel; Kreiser, Lothar, eds. (1986). Logik-Texte. De Gruyter. doi:10.1515/9783112645826.

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)