Constructive logic

Quality 0.50 · 7 views · Updated 2 months ago

title: "Constructive logic" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["logic-in-computer-science", "non-classical-logic", "constructivism-(philosophy-of-mathematics)", "systems-of-formal-logic", "intuitionism"] topic_path: "philosophy" source: "https://en.wikipedia.org/wiki/Constructive_logic" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

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

Main article: Intuitionistic logic

Founder: L. E. J. Brouwer (1908, philosophy) formalized by A. Heyting (1930) and A. N. Kolmogorov (1932)

Key Idea: Truth = having a proof. One cannot assert “P or not P” unless one can prove P or prove \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

Main article: Modal companion

Founder(s):

K F. Gödel (1933) showed that intuitionistic logic can be embedded into modal logic S4.
(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

Main article: Minimal logic

Simpler than intuitionistic logic.

Founder: I. Johansson (1937)

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)

Main article: Intuitionistic 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 Rocq, Agda.

5. Linear logic

Main article: Linear logic

Not strictly intuitionistic, but very constructive.

Founder: J. Girard (1987)

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

References

{{cite book | editor1-last = Berka | editor1-first = Karel | editor2-last = Kreiser | editor2-first = Lothar | title = Logik-Texte | publisher = De Gruyter | date=1986 | doi=10.1515/9783112645826 | isbn = 978-3-11-264582-6
{{cite book | last = Brouwer | first = Luitzen Egbertus Jan | author-link = L. E. J. Brouwer | title = Over de Grondslagen der Wiskunde | publisher = N.V. Uitgeversmaatschappij Sijthoff | year = 1908 | language = Dutch
{{cite journal | last = Brouwer | first = Luitzen Egbertus Jan | author-link = L. E. J. Brouwer | title = Intuitionism and Formalism | url = https://www.ams.org/journals/bull/2000-37-01/S0273-0979-99-00802-2/S0273-0979-99-00802-2.pdf | journal = Bulletin of the American Mathematical Society | volume = 19 | number = 6 | pages = 191–194 | year = 1913
{{cite journal | last = Girard | first = Jean-Yves | author-link = Jean-Yves Girard | title = Linear logic | journal = Theoretical Computer Science | volume = 50 | issue = 1 | pages = 1–101 | year = 1987 | doi = 10.1016/0304-3975(87)90045-4 | publisher = Elsevier | doi-access = free
{{cite book | last = Gödel | first = Kurt | author-link = Kurt Gödel | series = Collected Works | volume = I | year = 1986 | orig-year = 1933 | chapter = Eine Interpretation des intuitionistischen Aussagenkalkiils | title = Publications 1929–1936 | url = https://antilogicalism.com/wp-content/uploads/2021/12/Godel-1.pdf | editor1-last = Feferman | editor1-first = Solomon | editor1-link = Solomon Feferman | editor2-last = Dawson, Jr. | editor2-first = John W. | editor2-link = John W. Dawson Jr. | editor3-last = Kleene | editor3-first = Stephen C. | editor3-link = Stephen Cole Kleene | editor4-last = Moore | editor4-first = Gregory H. | editor5-last = Solovay | editor5-first = Robert M. | editor5-link = Robert M. Solovay | editor6-last = Van Heijenoort | editor6-first = Jean | editor6-link = Jean van Heijenoort | location = New York | publisher = Oxford University Press | isbn = 978-0-19-503964-1
{{cite journal | last = Heyting | first = Arend | author-link = Arend Heyting | year = 1930 | title = Die formalen Regeln der intuitionistischen Logik | language = de | journal = Sitzungsberichte der preußischen Akademie der Wissenschaften, phys.-math. Klasse | pages = 42–56, 57–71, 158–169 | oclc = 601568391
{{cite journal | last = Johansson | first = Ingebrigt | author-link = Ingebrigt Johansson | year = 1937 | title = Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus | url = http://www.numdam.org/item/CM_1937__4__119_0 | journal = Compositio Mathematica | volume = 4 | pages = 119–136 | language = de
{{cite journal | last = Kolmogorov | first = Andrey | author-link = Andrey Kolmogorov | title = On the Principle of Excluded Middle | journal = Mathematical Logic Quarterly | volume = 10 | pages = 65–74 | year = 1932

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::