Constructive logic

Template:Use dmy dates 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

{{#invoke:Labelled list hatnote|labelledList|Main article|Main articles|Main page|Main pages}} Founder: L. E. J. Brouwer (1908, philosophy)Template:SfnTemplate:Sfn formalized by A. Heyting (1930)Template:Sfn and A. N. Kolmogorov (1932)Template:Sfn

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

{{#invoke:Labelled list hatnote|labelledList|Main article|Main articles|Main page|Main pages}} Founder(s):

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

{{#invoke:Labelled list hatnote|labelledList|Main article|Main articles|Main page|Main pages}} Simpler than intuitionistic logic.

Founder: I. Johansson (1937)Template:Sfn

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)

{{#invoke:Labelled list hatnote|labelledList|Main article|Main articles|Main page|Main pages}} 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

{{#invoke:Labelled list hatnote|labelledList|Main article|Main articles|Main page|Main pages}} Not strictly intuitionistic, but very constructive.

Founder: J. Girard (1987)Template:Sfn

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)

References

• Template:Cite book

• Template:Cite book

• Template:Cite journal

• Template:Cite journal

• Template:Cite book / Paperback: Template:Isbn

• Template:Cite journal
  (abridged reprint in Template:Harvnb)

• Template:Cite journal

• Template:Cite journal