Constructive logic

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:

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: Key Idea: Truth = having a proof. One cannot assert “ P or not P ” unless one can prove P or prove \neg P . Features: No law of excluded middle ( P \lor \neg P is not generally valid). No double negation elimination ( \neg \neg\ P \to P is not valid generally). Implication is constructive: a proof of P \to Q is a method turning any proof of P into a proof of Q. Used in: type theory, constructive mathematics. 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. ==References== / Paperback: (abridged reprint in )

Text derived from https://en.wikipedia.org/w/index.php?oldid=1363230066 under CC BY-SA 4.0; modifications have been made.