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

Features:

• No law of excluded middle ($P\; \backslash lor\; \backslash neg\; P$ is not generally valid).
• No double negation elimination ($\backslash neg\; \backslash neg\backslash \; P\; \backslash to\; P$ is not valid generally).
• Implication is constructive: a proof of $P\; \backslash to\; Q$ is a method turning any proof of P into a proof of Q.

Used in: type theory, constructive mathematics.

{{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): $\backslash Box\; P$ means “$P$ is provable” (or “necessarily $P$” in the proof sense).

Further: Modern provability logics build on this.

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

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

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

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

{{Reflist|2}}

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

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