Constructive logic

Constructive logic is a family of logics where proofs must be constructive. No “non-constructive” proofs are allowed.
The main constructive logics are the following:

1. Intuitionistic logic

Founder: L. E. J. Brouwer formalized by A. Heyting and A. N. Kolmogorov
Key Idea: Truth = having a proof. One cannot assert “ or not ” unless one can prove or prove.
Features:

No law of excluded middle.
No double negation elimination.
Implication is constructive: a proof of 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

Founder:

K F. Gödel showed that intuitionistic logic can be embedded into modal logic S4.

Interpretation : means “ is provable”.
Further: Modern provability logics build on this.

3. Minimal logic

Simpler than intuitionistic logic.
Founder: I. Johansson
Key Idea: Like intuitionistic logic but without assuming the principle of explosion.
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)

Founder: P. E. R. Martin-Löf
Key Idea: Types = propositions, terms = proofs.
Features:

Every proof is a program.
Very strict — everything must be directly constructible.

Used in: Proof assistants like Rocq, Agda.

5. Linear logic

Not strictly intuitionistic, but very constructive.
Founder: J. Girard
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.

Used in: Computer science, concurrency, quantum logic.

6. Other Constructive Systems

Constructive set theory : Builds sets constructively.Realizability Theory: Ties constructive logic to computability — proofs correspond to algorithms.Topos Logic: Internal logics of topoi are intuitionistic.