Constructive logic
From Wikipedia, the free encyclopedia
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
Founder: L. E. J. Brouwer (1908, philosophy)[1][2] formalized by A. Heyting (1930)[3] and A. N. Kolmogorov (1932)[4]
Key Idea: Truth = having a proof. One cannot assert “ or not ” unless one can prove or prove .
Features:
- No law of excluded middle ( is not generally valid).
- No double negation elimination ( is not valid generally).
- 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(s):
- K F. Gödel (1933) showed that intuitionistic logic can be embedded into modal logic S4.[5]
- (other systems)
Interpretation (Gödel): means “ is provable” (or “necessarily ” in the proof sense).
Further: Modern provability logics build on this.
3. Minimal logic
Simpler than intuitionistic logic.
Founder: I. Johansson (1937)[6]
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)
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.
5. Linear logic
Not strictly intuitionistic, but very constructive.
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
Notes
References
Wikiwand - on
Seamless Wikipedia browsing. On steroids.