Intuitionistic Logic

Classical logic — the system underlying sentential and first-order logic as developed here — takes every statement to be either true or false independently of our ability to verify it. Intuitionistic logic rejects this. Arising from Brouwer's intuitionism and formalized by his student Heyting, it reads the logical connectives constructively: to assert a proposition is to possess a construction (a proof) of it. This single shift invalidates certain classical laws — most famously the law of excluded middle — and turns out to coincide exactly with the logic of computation.

This page assumes familiarity with the syntax of sentential and first-order logic; the language is the same, but the meaning of the connectives and the valid inferences differ.

The constructive reading (BHK)

The intended meaning of the connectives is given not by truth tables but by the Brouwer–Heyting–Kolmogorov (BHK) interpretation, which explains what counts as a proof of each compound:

• a proof of $\phi \wedge \psi$ is a pair: a proof of $\phi$ together with a proof of $\psi$;
• a proof of $\phi \vee \psi$ is a proof of $\phi$ or a proof of $\psi$, together with a tag saying which — disjunction carries explicit witnessing information;
• a proof of $\phi \to \psi$ is a method (construction) transforming any proof of $\phi$ into a proof of $\psi$;
• a proof of $\exists x\phi (x)$ is a pair: a witness $t$ together with a proof of $\phi (t)$;
• a proof of $\forall x\phi (x)$ is a method producing, for each $t$, a proof of $\phi (t)$;
• negation is defined as $\neg \phi \equiv (\phi \to \perp )$, where $\perp$ (falsum) has no proof; so a proof of $\neg \phi$ is a method converting any hypothetical proof of $\phi$ into a proof of the absurd.

There is no clause for a "true but unproven" proposition: assertion is provability. This is why the classical bivalence $\phi \vee \neg \phi$ is not generally warranted — to assert it constructively would require, for every $\phi$, either a proof or a refutation, which we do not have in general.

What changes from classical logic

Intuitionistic logic is strictly weaker than classical logic: every intuitionistic theorem is a classical theorem, but not conversely. The classically valid principles that fail intuitionistically are all interderivable with each other over the intuitionistic base:

• Excluded middle (LEM): $\phi \vee \neg \phi$;
• Double-negation elimination: $\neg \neg \phi \to \phi$;
• Proof by contradiction in its classical form: from $\neg \phi \to \perp$ infer $\phi$;
• Peirce's law: $((\phi \to \psi )\to \phi )\to \phi$;
• one De Morgan direction: $\neg (\phi \wedge \psi )\to (\neg \phi \vee \neg \psi )$;
• the classical quantifier shift $\neg \forall x\phi \to \exists x\neg \phi$.

What survives is everything constructively justified. In particular the following hold intuitionistically:

• one direction of double negation, $\phi \to \neg \neg \phi$ (but not the converse);
• $\neg \neg (\phi \vee \neg \phi )$ — excluded middle is not refutable, merely not assertible;
• ex falso quodlibet, $\perp \to \phi$ (intuitionistic logic is still explosive — this is minimal logic's point of departure, which drops even this).

One must also take care with the axiom of choice: although AC is independent of classical ZF, over intuitionistic logic the full set-theoretic AC actually implies excluded middle (Diaconescu's theorem), so it cannot be adopted constructively without collapsing back to classical logic — see The Axiom of Choice and Excluded Middle.

A hallmark of the constructive reading is the disjunction and existence properties, which classical logic lacks:

• Disjunction property: if $⊢\phi \vee \psi$ then $⊢\phi$ or $⊢\psi$;
• Existence property: if $⊢\exists x\phi (x)$ then $⊢\phi (t)$ for some explicit term $t$.

These say that a constructive proof of an alternative or an existential always carries the witnessing information BHK demands.

Proof theory

Intuitionistic logic is obtained from a classical proof system by removing exactly one principle. In natural deduction, classical logic is intuitionistic logic plus the double-negation elimination (or LEM, or reductio) rule; dropping that rule — keeping introduction/elimination rules and ex falso — yields intuitionistic natural deduction $\mathbf{NJ}$ (versus classical $\mathbf{NK}$). In the sequent calculus, Gentzen's $\mathbf{LK}$ becomes intuitionistic $\mathbf{LJ}$ by the elegant structural restriction that each sequent has at most one formula on the right ($\Gamma ⊢\Delta$ with $|\Delta |\le 1$). Both calculi enjoy cut elimination, from which the disjunction and existence properties follow.

The Curry–Howard correspondence

The deepest fact about intuitionistic logic is its identity with computation. Under the Curry–Howard correspondence:

$$\text{propositions}\leftrightarrow \text{types},\text{proofs}\leftrightarrow \text{programs},\text{proof normalization}\leftrightarrow \text{program evaluation}.$$

Intuitionistic implication $\phi \to \psi$ corresponds to the function type, $\wedge$ to the product type, $\vee$ to the sum type, $\perp$ to the empty type, and $\forall$/$\exists$ to dependent product/sum types. A proof in intuitionistic natural deduction is a typed $\lambda$-term, and normalizing the proof is running the program. This is why intuitionistic logic — not classical logic — is the logic of type theory and of proof assistants such as Coq/Rocq, Agda, and Lean: a constructive existence proof literally yields a program computing the witness. (Classical reasoning corresponds, via Griffin's extension, to control operators like call/cc.)

Semantics: Kripke models

Truth-table (two-valued) semantics cannot characterize intuitionistic logic — it is not truth-functional. The standard semantics is instead Kripke semantics, which models the growth of knowledge over time.

A Kripke model is a partially ordered set $(W,\le )$ of worlds (epistemic states of information), each world $w$ assigned a domain and a set of atoms it forces, subject to monotonicity (persistence): if $w\le w^{\prime }$ and $w$ forces $p$, then $w^{\prime }$ forces $p$ (knowledge once established is never lost). Forcing $w⊩\phi$ is defined by recursion, the key non-classical clauses being:

• $w⊩\phi \to \psi$ iff for every $w^{\prime }\ge w$, if $w^{\prime }⊩\phi$ then $w^{\prime }⊩\psi$ — implication quantifies over all future states;
• $w⊩\neg \phi$ iff for every $w^{\prime }\ge w$, $w^{\prime }/⊩\phi$;
• $w⊩\exists x\phi$ requires an actual witness in $w$'s domain; $w⊩\forall x\phi$ quantifies over all future domains.

A formula is intuitionistically valid iff it is forced at every world of every Kripke model. Excluded middle fails because a world may force neither $p$ nor $\neg p$: $p$ is not yet established, but a later world might establish it, so $\neg p$ is not forced either. Intuitionistic logic is sound and complete for Kripke semantics, and (like classical first-order logic) its validity is undecidable in the first-order case but decidable in the propositional case — though propositional intuitionistic validity is $\mathsf{PSPACE}$-complete (see Computational Complexity Theory), harder than the $\mathsf{coNP}$-complete classical case.

An alternative algebraic semantics replaces the two-element Boolean algebra of classical logic with Heyting algebras (bounded lattices with a relative pseudo-complement $\Rightarrow$); classical logic is the special case where the Heyting algebra is Boolean. The open-set lattice of any topological space is a Heyting algebra, giving intuitionistic logic a natural topological interpretation.

Relation to classical logic

Intuitionistic logic does not contradict classical logic; it refines it. Two precise bridges:

• Glivenko's theorem (propositional): $\phi$ is a classical tautology iff $\neg \neg \phi$ is an intuitionistic theorem. Classical truth is exactly intuitionistic double-negation truth.
• Gödel–Gentzen negative translation: every classical first-order theorem has a double-negation–decorated translation ${\phi }^N$ that is intuitionistically provable. Thus classical logic embeds into intuitionistic logic — anything classical mathematics proves, constructive mathematics can prove about its negative translation. This shows intuitionistic logic is not weaker in consistency strength, only in what it asserts outright.

Adding any of the failed classical principles (LEM, double-negation elimination, Peirce's law, …) to the intuitionistic base recovers full classical logic.

Intuitionistic logic is paracomplete — it gives up excluded middle, allowing truth-value gaps (a proposition need be neither proven nor refuted) — but it remains explosive: a contradiction still entails everything (ex falso quodlibet). Its formal dual is paraconsistent logic, which instead gives up explosion, allowing truth-value gluts.

Worked examples

Five small illustrations make the abstract results concrete.

Why $\phi \vee \neg \phi$ is not assertible: an open problem

The cleanest illustration is a Brouwerian counterexample built from an unsolved problem. Let

$$G=\text{“every even integer}>2\text{ is a sum of two primes”}(\text{Goldbach’s conjecture}).$$

Classically $G\vee \neg G$ is trivially true. Intuitionistically one may assert it only by proving $G$ or refuting it — and we can presently do neither, so this instance of excluded middle is not warranted. To assert $\phi \vee \neg \phi$ in general would be to claim every proposition is already decided. We still cannot refute the instance, matching the earlier point that $\neg \neg (\phi \vee \neg \phi )$ holds: excluded middle is not assertible, but not refutable either.

Why the existence property has teeth: $a^b$ rational

A celebrated non-constructive proof. Claim: there exist irrationals $a,b$ with $a^b$ rational.

Consider ${\sqrt{2}}^{\sqrt{2}}$. Either it is rational — then take $a=b=\sqrt{2}$. Or it is irrational — then take $a={\sqrt{2}}^{\sqrt{2}}$ and $b=\sqrt{2}$, giving $a^b={\sqrt{2}}^2=2$.

The argument is classically airtight, yet it invokes LEM on "is ${\sqrt{2}}^{\sqrt{2}}$ rational?" and concludes without saying which pair works. It establishes $\exists a,b(\dots )$ with no witness — exactly what the intuitionistic existence property forbids. A constructive proof must exhibit a pair outright, e.g. $a=\sqrt{2}$, $b=2{\log }_{2}3$ (then $a^b=3$).

The smallest countermodel: two worlds

The entire Kripke semantics fits in one picture. Take $W=\{w_0,w_1\}$ with $w_0\le w_1$, where $w_0$ forces no atoms and $w_1$ forces $p$:

$$w_0⟶w_1(w_1⊩p).$$

At $w_0$, the atom $p$ is not forced (not yet established), and $\neg p$ is not forced either — the future world $w_1$ forces $p$, violating the negation clause. Hence $w_0/⊩p\vee \neg p$: two worlds suffice to refute excluded middle, and the diagram literally depicts the "growth of knowledge" reading.

Curry–Howard you can hold in your hand

At the smallest types, the proofs-as-programs slogan is fully concrete:

• a proof of $A\to A$ is the identity function $\lambda x.x$;
• a proof of $A\wedge B\to A$ is the first projection $\lambda p.{\pi }_{1}p$;
• a proof of $A\to (B\to A)$ is the constant function $\lambda x.\lambda y.x$.

The gap with classical logic appears exactly where there is no program: there is no closed term of type $A\vee (A\to \perp )$ for an abstract $A$ — excluded middle simply has no computational content.

Classical theorems that break constructively

Two "fugitive real" counterexamples show why analysis changes. Build a real $x$ whose definition encodes an undecided problem — say $x={\sum }_n\pm 2^{-n}$ where the sign at stage $n$ depends on whether Goldbach holds up to $n$:

• Trichotomy fails. The law $x<0\vee x=0\vee x>0$ is not constructively valid — deciding which disjunct holds would settle the encoded problem.
• The intermediate value theorem fails in its classical form: a constructive continuous function that crosses zero may have no locatable root if it lingers at $0$, yielding $\neg \neg (\exists \text{root})$ but not the root. Constructive analysis recovers an approximate IVT instead.

Both dramatize the slogan that intuitionistic logic keeps only what one can build.

Summary

Intuitionistic logic is what remains of classical logic when one insists that to assert is to construct. It costs the law of excluded middle and the classical equivalences that depend on it, and in return gains the disjunction and existence properties, a precise correspondence with computation, and a refined semantics of evolving knowledge. It is the native logic of constructive mathematics and of modern type-theoretic proof assistants.