Editing Constructive logic

{{use dmy dates|date=April 2025}}
'''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|Intuitionistic logic}}
'''Founder''': [[L. E. J. Brouwer]] (1908, philosophy){{sfn|Brouwer|1908}}{{sfn|Brouwer|1913}} formalized by [[Arend Heyting|A. Heyting]] (1930){{sfn|Heyting|1930}} and [[Andrey Kolmogorov|A. N. Kolmogorov]] (1932){{sfn|Kolmogorov|1932}}

'''Key Idea''': Truth = having a proof. One cannot assert “<math>P</math> or not <math>P</math>” unless one can prove <math>P</math> or prove <math>\neg \neg P</math>.

'''Features''':
* No [[law of excluded middle]] (<math>P \lor \neg P</math> is not generally valid).
* No [[Double negation#Elimination and introduction|double negation elimination]] (<math>\neg \neg\ P \to P</math> is not valid generally).
* [[Material conditional|Implication]] is constructive: a proof of <math>P \to Q</math> is a method turning any proof of P into a proof of Q.

'''Used in''': [[type theory]], [[Constructivism (philosophy of mathematics)|constructive mathematics]].

== 2. Modal logics for constructive reasoning ==
{{main|Modal companion}}
'''Founder(s)''':
* [[Kurt Gödel|K F. Gödel]] (1933) showed that intuitionistic logic can be embedded into [[Modal logic|modal logic S4]].{{sfn|Gödel|1986|pages=300-302}}
* (other systems)

'''Interpretation''' (Gödel): <math>\Box P</math> means “<math>P</math> is provable” (or “necessarily <math>P</math>” in the proof sense).

'''Further''': Modern provability logics build on this.

== 3. Minimal logic ==
{{main|Minimal logic}}
Simpler than intuitionistic logic.

'''Founder''': [[Ingebrigt Johansson|I. Johansson]] (1937){{sfn|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|Intuitionistic type theory}}
'''Founder''': [[Per Martin-Löf|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|Coq]], [[Agda (programming language)|Agda]].

== 5. Linear logic ==
{{main|Linear logic}}
Not strictly intuitionistic, but very constructive.

'''Founder''': [[Jean-Yves Girard|J. Girard]] (1987){{sfn|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|Realizability Theory]]''': Ties constructive logic to computability — proofs correspond to algorithms.

* '''[[Topos|Topos Logic]]''': Internal logics of topoi (generalized spaces) are intuitionistic.

== See also ==
* [[Constructivism (philosophy of mathematics)]]

== Notes ==
{{Reflist|2}}

==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
}}

*{{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
}} / Paperback: {{isbn|978-0-19-514720-9}}

* {{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
}}<br/>(abridged reprint in {{harvnb|Berka|Kreiser|1986|pages=188-192}})

*{{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
}}

{{Non-classical logic}}

{{Authority control}}

[[Category:Logic in computer science]]
[[Category:Non-classical logic]]
[[Category:Constructivism (mathematics)]]
[[Category:Systems of formal logic]]
[[Category:Intuitionism]]