{{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 A. Heyting (1930){{sfn|Heyting|1930}} and 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 P</math>.
'''Features''': * No law of excluded middle (<math>P \lor \neg P</math> is not generally valid). * No double negation elimination (<math>\neg \neg\ P \to P</math> is not valid generally). * 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, constructive mathematics.
== 2. Modal logics for constructive reasoning == {{main|Modal companion}} '''Founder(s)''': * K F. Gödel (1933) showed that intuitionistic logic can be embedded into 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''': 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''': 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|Linear logic}} Not strictly intuitionistic, but very constructive.
'''Founder''': 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 Theory''': Ties constructive logic to computability — proofs correspond to algorithms.
* '''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 | 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 }} / 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 (philosophy of mathematics) Category:Systems of formal logic Category:Intuitionism