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:

Founder: L. E. J. Brouwer (1908, philosophy) formalized by A. Heyting (1930) and A. N. Kolmogorov (1932)

Key Idea: Truth = having a proof. One cannot assert “${\displaystyle P}$ or not ${\displaystyle P}$” unless one can prove ${\displaystyle P}$ or prove ${\displaystyle \neg P}$.

Features:

Used in: type theory, constructive mathematics.

Founder(s):

Interpretation (Gödel): ${\displaystyle \Box P}$ means “${\displaystyle P}$ is provable” (or “necessarily ${\displaystyle P}$” in the proof sense).