Intuitionistic Logic

logic intuitionistic-logic

Definition

Intuitionistic Logic

Intuitionistic logic (or constructive logic) is a formal system of logic that differs from classical logic by rejecting the universal validity of the Law of Excluded Middle ($A\vee \neg A$). In intuitionistic logic, a statement is considered true only if there is a direct construction or proof for it.

Principles

The fundamental shift in intuitionistic logic is the interpretation of truth as provability rather than an objective state of the universe.

BHK Interpretation

The semantics of intuitionistic logic can be described by the Brouwer–Heyting–Kolmogorov interpretation:

• A proof of $A\wedge B$ is a pair consisting of a proof of $A$ and a proof of $B$.
• A proof of $A\vee B$ is a proof of $A$ or a proof of $B$, along with an indication of which one was proved.
• A proof of $A⟹B$ is a construction (function) that transforms any proof of $A$ into a proof of $B$.
• A proof of $\neg A$ is a construction that transforms any proof of $A$ into a proof of a contradiction ($\perp$).
• A proof of $\exists xP(x)$ is an element $d$ and a proof of $P(d)$ (constructivity).

Deviations from Classical Logic

Several principles of classical logic do not hold intuitionistically:

1. Law of Excluded Middle: $A\vee \neg A$ is not a tautology.
2. Double Negation Elimination: $\neg \neg A⟹A$ is not generally valid (though $A⟹\neg \neg A$ is).
3. Existence: To prove $\exists xP(x)$, one must be able to construct a specific witness $d$ such that $P(d)$ holds.

Relation to Computation

Through the Curry-Howard Correspondence, intuitionistic logic has a deep connection to computer science: propositions correspond to types, and proofs correspond to programs. This makes it the foundation for many interactive theorem provers.