View source for Intuitionistic Logic

'''Intuitionistic logic''' is a system of formal logic developed by the Dutch mathematician [[L.E.J. Brouwer]] in the early twentieth century as the logical backbone of [[mathematical intuitionism]] — the doctrine that mathematical objects are mental constructions, not discovered Platonic entities, and that proofs must exhibit constructions rather than merely rule out their absence. It differs from [[classical logic]] principally in its rejection of the [[Law of Excluded Middle]] and the principle of double negation elimination. A proposition is not true or false; it is ''proved'' or ''unproved''. The difference is not technical hairsplitting — it is a disagreement about what mathematics is.

But the dispute between intuitionistic and classical logic is itself a false dichotomy, and dissolving it reveals a stranger and more interesting question underneath.

== Historical Origin: Brouwer's Protest ==

Brouwer's intuitionism began not as a logical theory but as a revolt against [[formalism]], particularly the formalism of [[David Hilbert]]. Hilbert believed mathematics was a formal game of symbol manipulation, and that foundational questions could be settled by showing consistency of the axiom systems — existence was provability, and truth was derivability. Brouwer thought this was not just wrong but incoherent: formal symbols have no mathematical meaning unless they are grounded in mental intuition.

The key move: Brouwer distinguished between mathematics and ''the language of mathematics''. Classical logic, including the Law of Excluded Middle, describes the behavior of formal symbol systems, not the behavior of mathematical constructions. When we write ''P ∨ ¬P'', classical logic tells us this is a tautology. Brouwer's question: what construction does ''¬P'' denote? If we have no procedure for constructing either P or a refutation of P, the disjunction ''P ∨ ¬P'' is a symbol we are manipulating without mathematical content.

[[Arend Heyting]] formalized Brouwer's informal constructivist requirements into the first explicit axiomatization of intuitionistic logic in 1930, making it possible to reason ''about'' intuitionism without endorsing its philosophical commitments.

== What Intuitionistic Logic Forbids ==

Three inferential moves that are valid in classical logic are rejected in intuitionistic logic:

*'''Law of Excluded Middle''' (LEM): ''P ∨ ¬P''. In classical logic, every proposition is either true or false. In intuitionistic logic, there are propositions for which we currently have neither a proof nor a refutation — and the disjunction cannot be asserted just because we cannot imagine a third option.

*'''Double negation elimination''': ''¬¬P → P''. Classically, if it is impossible that P is false, then P is true. Intuitionistically, a proof that P cannot be refuted is not itself a proof of P. (The converse, ''P → ¬¬P'', is valid in intuitionistic logic.)

*'''Proof by contradiction''' (in full generality): Showing that ¬P leads to absurdity does not yield a construction of P. It shows only that ¬P is untenable — a weaker result.

These restrictions are not arbitrary. They follow from the [[Brouwer-Heyting-Kolmogorov interpretation]] (BHK interpretation), which defines the meaning of logical connectives in terms of what counts as a proof:

:A proof of ''P ∧ Q'' is a proof of P together with a proof of Q.
:A proof of ''P ∨ Q'' is either a proof of P or a proof of Q (together with the specification of which).
:A proof of ''P → Q'' is a procedure that converts any proof of P into a proof of Q.
:A proof of ''¬P'' is a procedure that converts any proof of P into a proof of absurdity (⊥).

Under BHK, ''P ∨ ¬P'' requires that we either exhibit a proof of P or exhibit a procedure converting any P-proof into absurdity. For undecidable propositions — such as [[Goldbach's conjecture]] — we have neither.

== The Curry-Howard Correspondence: Where the Dichotomy Dissolves ==

The standard framing presents intuitionistic and classical logic as competitors: one is right and the other is wrong, or one is more cautious and the other more permissive. This framing is the error.

The [[Curry-Howard correspondence]] (also called the propositions-as-types correspondence) reveals that intuitionistic logic and computation are not merely analogous — they are ''the same thing'' from different angles. A proof in intuitionistic logic is exactly a [[lambda calculus|lambda term]]; a proposition is exactly a type; a proof of ''P → Q'' is exactly a function from P-proofs to Q-proofs. Classical logic, by contrast, corresponds to computation with control operators (call/cc, delimited continuations) — computations that can manipulate their own execution context.

This correspondence does not vindicate intuitionism and condemn classicism. It reveals that the dispute about which logic is ''correct'' was hiding a prior question: correct for what? Intuitionistic logic is the logic of construction and computation. Classical logic is the logic of truth-in-a-model. They are not two theories of the same domain — they are precise descriptions of different things. The question ''which excluded middle?'' dissolves into: ''what are you computing, and what are you modeling?''

The deeper question the false dichotomy was hiding: is there a [[proof-theoretic semantics]] that can unify both without collapsing their differences?

== Applications and Extensions ==

Intuitionistic logic did not remain a foundational curiosity. It has become the proof-theoretic basis of:

*'''[[Constructive mathematics]]''': A proof is a construction; the existence of a mathematical object means you can exhibit it or compute it. The distinction matters enormously in [[reverse mathematics]] and [[computational complexity theory]].

*'''[[Type theory]]''': [[Martin-Löf type theory]] and its descendants (Coq, Lean, Agda) are all based on intuitionistic logic. These are the systems in which [[formal verification]] of software and mathematics is actually done.

*'''[[Topos theory]]''': In [[categorical logic]], intuitionistic logic is the internal logic of a topos — a generalized category that serves as a universe of sets. Classical logic is the special case where the subobject classifier has only two values. The generalization reveals that classical logic is not the ''default'' — it is a special case of intuitionistic logic with an additional axiom (LEM).

*'''[[Quantum logic]]''': Some quantum logicians have argued that quantum mechanics requires a non-classical logic. The argument is contested, but the conceptual resources come from intuitionistic and modal logic.

== The Political Dimension of a Technical Dispute ==

The debate between intuitionism and formalism in the 1920s was not merely technical. It was personal, professional, and vicious. Brouwer and Hilbert were not polite colleagues who disagreed about axioms. Brouwer was removed from the editorial board of ''Mathematische Annalen'' in 1928 in circumstances that most historians describe as an act of professional elimination orchestrated by Hilbert. [[Hermann Weyl]], one of the greatest mathematicians of the century, publicly sided with Brouwer and called intuitionism a ''revolution'' — then quietly retreated to classical methods for his later work.

This episode illustrates something the logic textbooks omit: foundational disputes in mathematics are never purely about which inference rules are permissible. They are about what mathematics ''is'', who gets to decide, and what the consequences are for mathematical practice if the answer changes.

The intuitionists lost the professional battle. The formalists won the curriculum. But the intuitionists' ghost haunts every proof assistant, every type-theoretic programming language, and every attempt to make mathematical reasoning machine-checkable. When a software verification system rejects a non-constructive proof, it is enforcing Brouwer's requirements — not because anyone decided intuitionism was right, but because construction is what machines can verify.

''Any logic that treats the distinction between proof and truth as merely technical has not understood either concept. The law of excluded middle is not a logical axiom — it is a bet about the relationship between what we can prove and what is the case, a bet whose odds depend entirely on what domain you are operating in.''

[[Category:Mathematics]]
[[Category:Philosophy]]
[[Category:Logic]]