Intuitionism and Mathematical Construction

Hilbert sought to justify the use of ideal mathematics through a controlled investigation of proofs. L. E. J. Brouwer questioned a different assumption: that the meaning of a mathematical assertion could be separated from the construction that establishes it.

On the intuitionistic view, mathematics is grounded in constructions, and logic records legitimate patterns within that activity. A formal calculus does not create the mathematical constructions merely by allowing expressions that describe them.

This position shaped Brouwer's 1907 dissertation and his 1908 criticism of unrestricted applications of logical principles. It also led to a productive tension. Brouwer did not regard a formal calculus as an exhaustive account of mathematics, yet other researchers developed formal intuitionistic logic and studied its properties mathematically.

Existence and the information a proof provides

Suppose we assert that there is a natural number $n$ satisfying a condition $P(n)$. A constructive proof should provide a way to obtain a witness and establish that it has the required property.

For a simple example, let $P(n)$ say that $n$ is an even number greater than $100$. The witness $102$, together with the relevant calculation, settles the claim. The statement and its evidence are closely connected.

Classical reasoning can also prove an existential statement by ruling out the possibility that no witness exists. The difference becomes important when that contradiction argument supplies no method for identifying the witness.

A familiar illustration concerns irrational numbers $a,b$ for which $a^b$ is rational. Set $r=(\sqrt2)^{\sqrt2}$. If $r$ is rational, take $a=b=\sqrt2$. If $r$ is irrational, take $a=r$ and $b=\sqrt2$, obtaining

This proves the existential assertion by a classical division into cases. As presented, it does not decide which pair it supplies. The point is about the information carried by this particular argument, not about whether the nature of $r$ can be settled by other mathematics.

A constructive criticism asks for the missing decision or for another proof with explicit witnesses. It does not deny that the classical derivation is valid according to classical rules.

Why excluded middle is the central example

The law of excluded middle states

For a proposition with an effective decision procedure, a constructive justification is straightforward: run the procedure and report the outcome. Brouwer's objection concerns treating this schema as automatically justified for arbitrary mathematical questions, especially those involving open-ended infinite processes.

If $P$ says that some natural number satisfies a decidable condition, a search will confirm $P$ when it finds a witness. If no witness exists, the search may continue indefinitely. Decidability of each individual case does not yield decidability of the existential statement.

Intuitionistic logic therefore does not accept excluded middle without qualification. It still permits proofs of particular instances and arguments by contradiction that establish a negation.

The important distinction is between showing $\neg P$ by deriving an absurdity from $P$, and deriving $P$ merely from $\neg\neg P$. The first pattern is intuitionistically acceptable; the second is not available as an unrestricted rule.

Heyting's calculus and the interpretation of connectives

Arend Heyting supplied an influential formal axiomatization of intuitionistic logic in 1930. Kolmogorov's 1925 work and Glivenko's 1929 results were important earlier developments in the relationship between classical and constructive reasoning.

The informal account now called the Brouwer–Heyting–Kolmogorov interpretation explains connectives through the evidence required for them:

The interpretation explains why conjunction and implication resemble pairs and functions. It is not yet a fully formal definition of proof or construction. Different attempts to make those notions precise produce different mathematical interpretations.

This distinction preserves Brouwer's concern. A formal description of evidence can be valuable without being accepted as the complete philosophical meaning of mathematical construction.

A small countermodel to excluded middle

Kripke semantics, developed later, provides a precise way to study intuitionistic validity. Its points can be interpreted as stages of information ordered by extension. Atomic information persists: once established, it remains established at later stages.

Consider two stages $w_0\leq w_1$. Let an atomic proposition $P$ hold at $w_1$ but not at $w_0$. Let absurdity hold nowhere.

At a stage $w$, implication $A\to B$ holds when every extension of $w$ that supports $A$ also supports $B$. Consequently, $\neg P$ holds only if no extension can support $P$.

At $w_0$, $P$ is not supported. But $\neg P$ is not supported either, because $w_1$ supports $P$. Thus

The model does not assign a mysterious third classical truth value to $P$. It changes the semantic conditions governing assertion, especially implication and negation, across an ordered structure.

It also shows why “not established” is different from “refuted.” A theory that treats the two as interchangeable loses the distinction the semantics is designed to preserve.

Classical reasoning inside constructive systems

The relationship between the two logics is more subtle than a list of forbidden classical arguments.

Glivenko's theorem states, for propositional formulas, that if $A$ is classically provable, then $\neg\neg A$ is intuitionistically provable. The restriction to propositional logic matters; the same simple formulation is not a general account of quantified logic.

More elaborate negative translations embed classical reasoning into intuitionistic systems. For suitable translations, a classical proof can be transformed into an intuitionistic proof of a translated statement. Gödel and Gentzen developed important versions of this method.

The result does not say that the original classical statement and its translation have identical constructive content. A double-negated existential assertion, for example, need not supply an explicit witness in the way a constructive existential proof does.

Translations therefore allow precise comparisons of logical strength while preserving the reason the systems differ. They also became tools in consistency analysis and proof interpretation.

Kleene's realizability

Stephen Kleene's 1945 paper introduced number realizability, assigning computational evidence to arithmetical formulas. Numbers can code programs as well as ordinary numerical data. A relation

states that $e$ realizes $A$.

For conjunction, a code can package realizers for both conjuncts. For an existential assertion, it can package a witness together with a realizer of the corresponding instance. For implication, an index $e$ denotes a partial recursive function satisfying

The requirement is that the program terminate appropriately on inputs that realize $A$. It need not terminate on every natural number. This is an essential qualification: a realizer of an implication is not required to be a globally total computable function.

Realizability supplies a mathematical interpretation of computational evidence, but it is not identical to derivability in intuitionistic arithmetic. Soundness establishes that proofs yield realizers under the specified interpretation; the converse requires separate investigation and is not supplied by the slogan that proofs are programs.

David Nelson played an important role in the early development. Kleene's paper explicitly credits Nelson's work on fundamental results. The history is consequently more accurately represented by distinguishing the proposal of the interpretation from the collaborative establishment of its properties.

Several constructive traditions

The word “constructive” covers mathematical programs with different commitments.

Brouwerian intuitionism includes investigations of choice sequences and continuity principles motivated by its account of mathematical construction. These are not obtained simply by deleting excluded middle from classical mathematics.

Errett Bishop's Foundations of Constructive Analysis of 1967 demonstrated how substantial analysis could be developed through methods emphasizing explicit mathematical content. Its approach differs from accepting the full collection of distinctive Brouwerian principles.

Russian constructive mathematics, associated with A. A. Markov and collaborators, gave algorithmic notions a central foundational role. Markov's principle permits a particular passage from double-negated existence to existence for decidable predicates. That additional principle is not accepted uniformly across all constructive schools.

Even an apparently elementary statement can therefore require clarification: what counts as a construction, which principles about algorithms are assumed, and which forms of choice or continuity are available?

Leopold Kronecker's earlier insistence on arithmetical and finite methods belongs to the background of these debates, but it should not be equated with any one later formal system.

From constructive meaning to proof structure

Intuitionistic logic created a setting in which the form of an assertion closely constrains the form of its evidence. An implication asks for a transformation; a conjunction asks for a pair; an existential claim asks for a witness.

Later proof theory and type theory would make these correspondences exact for particular calculi. Before developing that connection, however, the series needs a clear account of what it means for any calculus to match a semantics.

The next note separates derivability from truth in structures and explains how soundness and completeness relate them. Those distinctions apply to classical and intuitionistic systems alike, although the appropriate semantics differ.

Sources and further reading

• L. E. J. Brouwer, Over de grondslagen der wiskunde (1907) and “De onbetrouwbaarheid der logische principes” (1908).
• Andrey Kolmogorov, “On the Principle of Excluded Middle” (1925); Valery Glivenko, “Sur quelques points de la logique de M. Brouwer” (1929); Arend Heyting's 1930 papers on the formal rules of intuitionistic logic and mathematics.
• Stephen C. Kleene, “On the Interpretation of Intuitionistic Number Theory” (1945), including its acknowledgment of Nelson's contributions.
• Errett Bishop, Foundations of Constructive Analysis (1967); A. A. Markov, Theory of Algorithms (1954).
• The Development of Intuitionistic Logic, for the distinction between philosophical intuitionism and the development of formal calculi.