Intuitionistic Logic

Definition

Intuitionistic logic is a non-classical logic that interprets truth through constructive proof. To assert a proposition is to have a construction of it; to assert a disjunction is to have a construction of one side; and to assert an implication is to have a construction transforming proofs of the premise into proofs of the conclusion.

Why It Matters

Intuitionistic logic is a core background language for proof assistants, constructive mathematics, and the Curry-Howard view of proofs as programs. It matters for Formal Methods because machine-checked proofs often track not just whether a statement is classically true, but what construction establishes it.

Formalism / Key Objects

• A proof judgment has the form

$$\Gamma ⊢P,$$

meaning proposition P is derivable from assumptions Gamma.

• Negation is usually defined as implication to contradiction:

$$\neg P:=P\to \perp .$$

• Intuitionistic logic does not accept unrestricted excluded middle,

$$P\vee \neg P,$$

nor double-negation elimination,

$$\neg \neg P\to P,$$

as general theorem schemas.

• Classical propositional logic can be recovered by adding excluded middle or an equivalent classical principle to intuitionistic logic.
• Under Curry-Howard, propositions correspond to types and proofs correspond to programs inhabiting those types.
• Intuitionistic Proof Rules records the compact introduction, elimination, and negation rules used as the formal annex for this concept.

Connections

• Formal Methods uses intuitionistic logic through proof assistants and constructive verification workflows.
• Temporal Logic and Linear Temporal Logic are usually presented classically in this wiki, but constructive variants matter when specifications are interpreted proof-theoretically.
• Dynamic Epistemic Logic gives a different kind of non-classical extension, focused on knowledge and information-changing events rather than constructive proof.
• Automata Learning is not based on intuitionistic logic, but both topics sit near the boundary between logical structure and executable computation.

Common Confusions

• Intuitionistic logic is not simply “three-valued logic.” It changes what counts as a proof of logical connectives, especially disjunction and existence.
• Rejecting unrestricted excluded middle is not the same as proving not (P lor not P) for every P.
• Context sensitivity, vagueness, and meaning failure are related philosophical issues, but they are not identical to constructive provability.

Key Sources

• AbuseOfNotation2026 - The Case Against Boolean Logic
• Intuitionistic Proof Rules