The middle that is not excluded

Either $P$ or not $P$ is not a fact about the world. It is an axiom, it can be dropped, and what is left is a logic with models that can be drawn.

Read the third bar. $U$ together with $¬U$ does not fill the line. Read the fourth: $¬¬U$ is strictly larger than $U$. Those are the two classical laws failing, in a structure made of nothing but open intervals.

What is being dropped, and what is kept #

Intuitionistic logic is classical logic minus one axiom. Everything else stays: modus ponens, conjunction, disjunction, the meaning of implication as a rule for transforming evidence.

What goes is the law of excluded middle, $P ∨ ¬P$, and with it the equivalent double-negation elimination, $¬¬P → P$. Those two are equivalent to each other and the system is the same either way.

What does not go, and this is the part people expect to and are surprised by:

• $¬(P ∧ ¬P)$ — nothing is both true and false. Contradiction is still forbidden.
• $P → ¬¬P$ — one direction of double negation still holds.
• $¬¬¬P → ¬P$ — and back. Three negations collapse to one, even though two do not collapse to none.
• De Morgan’s law in one direction, and the other one only for negated statements.

That last cluster is the tell that something structured is going on rather than a rule being weakened at random. If negation were simply unreliable, three negations would be no better than two. They are, and the reason is visible in the figure.

Why open sets #

The model in the figure is not an analogy. The open sets of any topological space form a model of intuitionistic logic, exactly, and the correspondence is:

• and is intersection,
• or is union,
• false is the empty set,
• not $U$ is the interior of the complement,
• $U$ implies $V$ is the largest open set whose intersection with $U$ lies inside $V$.

Everything follows from one decision: the objects are open sets, so every operation must produce an open set, and the ordinary complement of an open set is not open. Taking the interior is the smallest repair, and it is where the information goes.

Take $U = (0,1) ∪ (1,2)$, an interval with the point 1 removed. Its complement is everything at most 0, the single point 1, and everything at least 2. The interior of that throws away the isolated point, because a single point contains no interval, so $¬U = (-1,0) ∪ (2,3)$ within the ambient line.

Now $U ∪ ¬U$ misses three points: 0, 1 and 2. And $¬¬U$ is the interior of the complement of $¬U$, which is the open interval $(0,2)$ — the hole is filled, so $¬¬U$ is strictly bigger than $U$.

The boundary is where the information is lost. Negation cannot see a set’s boundary, because a boundary point is in neither the set nor the interior of its complement, and double negation restores exactly the boundary. That is a geometric statement and it is the whole explanation of the algebra.

Three negations, drawn #

The collapse at three is worth checking against the picture, because it is the fact that separates this system from a broken one.

$¬U$ is an open set with no isolated bits — it was produced by taking an interior, so it is regular in the sense that it equals the interior of the closure of itself. Applying $¬¬$ to a set of that kind changes nothing. So $¬¬(¬U) = ¬U$, which is $¬¬¬U = ¬U$.

In words: the first negation loses the boundary, and after that there is no more boundary to lose. Negation is not degrading the set a little more each time; it loses something once and then stabilises.

The finite algebra makes the same points without any geometry. $¬\{a\}$ is $\{b\}$, and $¬\{b\}$ is $\{a\}$, so $¬¬\{a\} = \{a\}$ — that one behaves classically. But $¬\{a,b\}$ is empty and $¬¬\{a,b\}$ is everything, so $\{a,b\}$ is strictly below its double negation, and $\{a,b\} ∨ ¬\{a,b\}$ is $\{a,b\}$ rather than the whole space.

A structure with these operations is a Heyting algebra, and the theorem is that intuitionistic logic proves exactly what holds in every Heyting algebra — just as classical logic proves exactly what holds in every Boolean algebra. A Boolean algebra is a Heyting algebra in which negation happens to be complement, which is the special case where nothing has a boundary.

The other model: stages of knowledge #

There is a second semantics that says what the missing middle is missing, and it is the one that makes the system feel like a position rather than a mutilation.

A world here is a state of information rather than a possible universe. An arrow means later, with more known. And the rules are:

• $p$ holds at a stage when it has been established there.
• $¬p$ holds at a stage when $p$ will never be established, at that stage or any later one.
• $p → q$ holds at a stage when every later stage establishing $p$ also establishes $q$.

Persistence is the condition that makes this coherent: once something is established it stays established, and the figure asserts it on the model it draws rather than assuming it.

Now excluded middle fails, and the reason is precise. At an early stage, $p$ is not established — so $p$ does not hold. And $¬p$ requires that $p$ never gets established, which is a claim about all later stages and is false here, since $p$ arrives later. Neither disjunct holds, so the disjunction does not.

That is not ignorance. The model is complete; nothing about it is unknown. The claim being refuted is that one of the two disjuncts must hold at that stage, and at that stage neither is available. Excluded middle is being read as a claim about what is settled, and it is not.

That comparison is the fairest way to state the disagreement. The classical picture starts from a set of assignments, each of which settles every letter, and asks which formulas survive all of them. If that is what a truth value is, then excluded middle is a triviality: a letter is one thing or the other by construction, and a formula saying so is true in every row.

The intuitionistic position is that the starting point begs the question. Assuming an assignment exists — that every statement, including ones about infinitely many objects, is definitely settled one way — is exactly the assumption in dispute, and it has been built into the machinery before any reasoning starts. The open sets and the stages are two ways of building machinery that does not assume it, and in both, excluded middle stops holding.

Which of the two settings is right is not a mathematical question and this essay does not have a view. What is mathematical, and settled, is that the second one is coherent, has models, and proves a strictly smaller set of theorems.

What a proof is taken to be #

Behind both models is a reading of the connectives that Brouwer proposed and Heyting made precise, in which a proof is a construction rather than a certificate of truth.

• A proof of $P ∧ Q$ is a proof of $P$ together with a proof of $Q$.
• A proof of $P ∨ Q$ is a proof of one of them, together with a note of which.
• A proof of $P → Q$ is a method turning any proof of $P$ into a proof of $Q$.
• A proof of $¬P$ is a method turning any proof of $P$ into a contradiction.
• A proof of there exists an $x$ with $P(x)$ is an $x$, together with a proof of $P(x)$.

Under that reading, excluded middle asserts that for every $P$ there is either a proof of $P$ or a refutation of it, and a way of saying which. That is a very strong claim about a system’s reach, and it is not one anybody would adopt casually.

The disjunction clause is where the difference is felt in practice. Classically, proving $P ∨ Q$ by showing that $¬(¬P ∧ ¬Q)$ is a complete proof. Constructively it is not, because it never produces the note saying which one. The system has the disjunction property: if it proves $P ∨ Q$ then it proves $P$ or it proves $Q$. Classical logic does not, and $P ∨ ¬P$ is the standing counterexample.

What is actually lost #

Two things go, and both are worth naming honestly.

Proof by contradiction, in one of its two forms. Assuming $¬P$ and deriving a contradiction proves $¬¬P$, which classically is $P$ and here is not. Assuming $P$ and deriving a contradiction still proves $¬P$; that direction is fine. So half of the technique survives and the more useful half does not.

Pure existence proofs. The classic pattern — either this object works or that one does, and which is left unsaid — is unavailable. There is a standard example: are there irrational $a$ and $b$ with $a^b$ rational? Take $a = b = \sqrt{2}^{\sqrt{2}}$ if that is rational, and otherwise $a = \sqrt{2}^{\sqrt{2}}, b = \sqrt{2}$. One case works, the argument does not say which, and constructively it establishes nothing.

What is gained is that every proof carries a construction. A constructive proof of an existence statement contains the object; a constructive proof of a disjunction contains the choice. That is why proof assistants and dependently typed programming languages are built on this logic — a proof in them is a program, and running it produces the witness.

The quarrel, which was not academic #

The dates and the temperature are worth recording, because this is one of the few places in modern mathematics where a foundational disagreement had institutional consequences.

Brouwer set out the position between 1907 and the 1920s: mathematics is a mental construction, existence means construction, and excluded middle is an illegitimate generalisation from finite cases to infinite ones. He also, and separately, proved the fixed-point theorem that carries his name — by classical means, and later disowned it as a proof he could not accept, which is as clear a demonstration of seriousness as the subject offers.

Hilbert’s response was not measured. “Taking the principle of excluded middle from the mathematician would be the same as prohibiting the astronomer his telescope or the boxer the use of his fists.” In 1928 he removed Brouwer from the editorial board of the Mathematische Annalen, which caused enough of a scandal that Einstein — who wanted no part of what he called the Frog-Mouse Battle — resigned from it too.

What settled the mathematics rather than the argument was Heyting’s formalisation in 1930, which gave the position a precise proof system, and the models that followed — Kolmogorov and Gödel’s translations, Tarski and Stone’s topological semantics, Kripke’s in 1965. Once there were models, the question stopped being whether the position was coherent and became a technical subject with theorems in it.

That is the standard fate of a foundational quarrel in this field, and it is the same one the parallel postulate had. The dispute is about which assumptions to adopt; it is unresolvable by argument; and building a model converts it into mathematics, after which both sides have something to work on and the heat goes out of it.

Two models, one logic, and why that matters #

The two pictures in this essay are unrelated as objects. One is made of intervals on a line, the other of arrows between states of information. Neither was derived from the other.

They validate exactly the same formulas, and that is a theorem rather than a coincidence. Intuitionistic logic proves a formula precisely when it holds in every Heyting algebra, and precisely when it holds in every Kripke model of this kind. Two completeness theorems, two entirely different notions of model, one set of theorems.

That is the same situation the disc put the parallel postulate in, and it is worth noticing that this field’s central technique has now been used for three different jobs. Against classical logic, a model shows that excluded middle is not derivable — the open sets are a structure where everything else holds and it fails. For the system itself, the class of models is what defines the theorems. And in the middle, comparing two model classes shows two definitions agree.

A last observation, which is the reason this belongs in a collection about pictures. There is a translation, due to Gödel, sending every intuitionistic formula to a classical one by inserting double negations; and under it intuitionistic logic sits inside classical logic rather than contradicting it. So the two are not rivals in the way Euclidean and hyperbolic are rivals. They are the same subject under different readings of what a proof has to hand over, and the open sets are what the difference looks like once it is drawn: the boundary, which classical logic assigns to one side or the other, and which constructive logic leaves out of both.

Where it is now #

The position stopped being a minority philosophical stance some time ago, and the reason is practical rather than philosophical.

A constructive proof of there exists an $x$ with $P(x)$ contains an $x$. A constructive proof of $P → Q$ is a method. Under the correspondence between proofs and programs, those are not analogies: a proof in a suitable formal system is a program, its statement is the program’s type, and running it produces the witness. Every proof assistant in serious use — and the machine-checked proofs of the four-colour theorem and the Feit–Thompson theorem were done in one — is built on a constructive core, with excluded middle available as an assumption a user may add where it is wanted.

That is the modern arrangement and it is more sensible than either side of the 1928 quarrel. Excluded middle is a hypothesis rather than a law: statements proved without it are stronger, because they carry constructions; statements proved with it are still proved, and are marked as having used it. A system that tracks which theorems needed the assumption knows more than one that cannot ask.

The open sets on this page are the reason that arrangement is coherent rather than merely convenient. Without a model, dropping an axiom is a refusal; with one, it is a move to a structure where the axiom is false, and everything that follows is ordinary mathematics about that structure.