Intuitionistic Logic

Entry conditions

Use intuitionistic logic when:

• You need to reason about evidence, construction, or partial information rather than absolute truth and falsity.
• You want logical operations that have computational content — where a proof of “there exists an $x$” must exhibit the $x$.
• You are working in a Heyting algebra rather than a Boolean algebra.

The key difference from classical logic

Classical propositional logic assumes the law of excluded middle: for every proposition $P$, either $P$ or $\neg P$ holds. Intuitionistic logic drops this assumption. A proposition is true when you have a construction (a proof, a witness, an exhibit) that establishes it. A proposition is false when you have a construction showing it leads to contradiction. A proposition for which you have neither is simply undecided — it is not forced into one bin or the other.

This is not a restriction for the sake of austerity. It reflects the structure of situations where knowledge is partial: the meaning of a sign may be underdetermined; a measurement may be inconclusive; a claim may have evidence for it without that evidence being decisive. Intuitionistic logic gives these situations a formal language.

The BHK interpretation

The Brouwer-Heyting-Kolmogorov (BHK) interpretation defines the meaning of each connective in terms of constructions (Troelstra & van Dalen, 1988):

• A proof of $A\wedge B$ is a pair: 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$, together with an indication of which.
• A proof of $A\Rightarrow B$ is a method that transforms any proof of $A$ into a proof of $B$.
• A proof of $\neg A$ is a method that transforms any proof of $A$ into a proof of $\perp$ (absurdity).
• There is no proof of $\perp$.

Under this reading, $A\vee \neg A$ requires that you can either prove $A$ or derive a contradiction from $A$. For many propositions, you can do neither, so excluded middle fails.

What changes without excluded middle

Several classically valid principles become unavailable:

Principle	Classical	Intuitionistic
$A\vee \neg A$ (excluded middle)	valid	not generally valid
$\neg \neg A\Rightarrow A$ (double negation elimination)	valid	not generally valid
$(\neg B\Rightarrow \neg A)\Rightarrow (A\Rightarrow B)$ (contraposition, strong form)	valid	not generally valid
$(A\Rightarrow B)\vee (B\Rightarrow A)$ (linearity)	valid	not generally valid

What remains valid includes: $A\Rightarrow \neg \neg A$, the deduction theorem, modus ponens, and all reasoning that proceeds by constructing witnesses rather than eliminating alternatives.

Kripke semantics

Intuitionistic logic has a natural semantics using Kripke frames, with one additional requirement: the accessibility relation is a partial order, and truth is monotone — once a proposition becomes true at a world, it stays true at all accessible (later, more-informed) worlds (van Dalen, 2013).

A Kripke model for intuitionistic logic is a triple $(W,\le ,V)$ where:

• $W$ is a set of worlds (think: states of knowledge).
• $\le$ is a partial order on $W$ (think: increasing information).
• $V$ assigns to each atomic proposition the set of worlds where it holds, with the constraint that $V(p)$ is upward-closed: if $w\in V(p)$ and $w\le w^{\prime }$, then $w^{\prime }\in V(p)$.

The forcing relation $w⊩A$ is defined inductively:

• $w⊩p$ iff $w\in V(p)$.
• $w⊩A\wedge B$ iff $w⊩A$ and $w⊩B$.
• $w⊩A\vee B$ iff $w⊩A$ or $w⊩B$.
• $w⊩A\Rightarrow B$ iff for every $w^{\prime }\ge w$, if $w^{\prime }⊩A$ then $w^{\prime }⊩B$.
• $w⊩\neg A$ iff for every $w^{\prime }\ge w$, $w^{\prime }⊮A$.

Notice: excluded middle fails because there may be a world $w$ where $A$ does not yet hold, but some extension of $w$ makes $A$ true — so $\neg A$ does not hold at $w$ either.

The algebraic connection

The Lindenbaum-Tarski construction shows that the equivalence classes of formulas under intuitionistic provability form a Heyting algebra. Conversely, every Heyting algebra provides a sound and complete semantics for intuitionistic propositional logic (Dummett, 2000).

This correspondence is exact: intuitionistic logic IS the internal logic of Heyting algebras, just as classical logic is the internal logic of Boolean algebras.

Worked example

Consider two worlds: $w_0$ (initial knowledge) and $w_1$ (extended knowledge), with $w_0\le w_1$. Let $p$ be the proposition “the sample contains iron.”

• At $w_0$: the initial test is inconclusive. $p$ does not hold — the evidence is insufficient. But $\neg p$ does not hold either, because further testing at $w_1$ might confirm $p$.
• At $w_1$: a more sensitive test is run and $p$ holds.

At $w_0$, neither $p$ nor $\neg p$ is forced. Excluded middle fails. The Heyting implication $p\Rightarrow p$ still holds everywhere (trivially), and $\neg p\Rightarrow \neg p$ holds everywhere, but $p\vee \neg p$ does not hold at $w_0$.

Common mistakes

• Treating intuitionistic logic as “weaker” classical logic. It is a different logic with different valid principles, not a subset of classical theorems. Intuitionistic proofs carry computational content that classical proofs do not.
• Assuming $\neg \neg A$ gives you $A$. Double negation elimination fails. You can show $A$ is not refutable without having a proof of $A$.
• Forgetting monotonicity in Kripke models. If $p$ holds at world $w$, it must hold at all worlds above $w$. Truth can grow but not shrink.

Minimal data

• A set of atomic propositions.
• Connectives $\wedge ,\vee ,\Rightarrow ,\neg$ with BHK reading.
• An inference system (e.g. natural deduction for intuitionistic logic) that lacks excluded middle and double negation elimination.

Dummett, M. (2000). Elements of Intuitionism (2nd ed.). Oxford University Press.

Troelstra, A. S., & van Dalen, D. (1988). Constructivism in Mathematics: An Introduction. North-Holland.

van Dalen, D. (2013). Logic and Structure (5th ed.). Springer.