Intuitionistic logic

Intuitionistic logic is a system of logic developed by L.E.J. Brouwer and formalized by Arend Heyting, which rejects the law of the excluded middle (every proposition is either true or false) and the principle of double negation elimination. In intuitionistic logic, a proposition is proved true only by explicit construction or direct evidence; indirect proofs that show a proposition cannot be false are insufficient. This makes intuitionistic logic the logical backbone of constructive mathematics, where existence claims require algorithms rather than mere non-contradiction.

The intuitionistic critique was aimed squarely at David Hilbert's formalism and at the set-theoretic foundations that Georg Cantor had built. Brouwer argued that mathematical objects are mental constructions, not formal symbols, and that reasoning about infinite totalities as if they were completed entities is illegitimate. The dispute split the foundations of mathematics into camps that remain unreconciled: the intuitionists demand proof by construction, while classical mathematicians accept proof by contradiction.

Intuitionistic logic is not a weaker version of classical logic. It is a different logic, with its own semantics (Kripke models, realizability), its own proof theory, and its own computational interpretation — the Curry-Howard correspondence identifies intuitionistic proofs with typed lambda calculus programs. In this sense, intuitionistic logic is the logic of computation, while classical logic is the logic of eternal, pre-given truth.

Intuitionistic Logic and the Limits of Verification

The Curry-Howard correspondence identifies intuitionistic proofs with typed lambda calculus programs, establishing that every constructive proof is a program and every program is a proof. This is not merely a philosophical alignment. It is a structural identity that has operational consequences. In classical logic, a proof of existence does not necessarily provide a witness. In intuitionistic logic, existence is constructive: to prove that something exists, one must produce it. This makes intuitionistic logic the natural language of algorithmic verification, where claims about program behavior must be backed by executable evidence.

But the computational interpretation of intuitionistic logic also reveals its limits. The Brouwer-Heyting-Kolmogorov (BHK) interpretation requires that a proof of an implication A → B be a function that transforms evidence for A into evidence for B. This is a strong requirement. It means that intuitionistic logic cannot express certain forms of reasoning that are commonplace in classical mathematics — reasoning by contradiction, reasoning about infinite sets via non-constructive selection, reasoning that exploits the law of excluded middle in contexts where no computational path is available.

These limitations are not defects. They are boundaries. Intuitionistic logic marks the edge of what can be computed, and in doing so, it maps the territory of the uncomputable. The principle that "every function is computable" — which holds in certain intuitionistic frameworks — is not a claim about the physical world. It is a claim about the world as it can be described by finite, step-by-step procedures. In this sense, intuitionistic logic is not an alternative to classical logic. It is a coarse-graining of classical logic: a restriction to the descriptions that can be operationalized by an observer with finite computational resources.

The connection to observer selection is direct. Classical logic presupposes an observer who can survey all possibilities at once — a God's-eye view that is not available to any finite computational process. Intuitionistic logic presupposes an observer who builds knowledge step by step, who cannot appeal to what has not yet been constructed. The debate between the two is not a debate about truth. It is a debate about which observers are possible, and what they can know.