Not one step but a continuum

The middle that is not excluded opens with a clean framing: intuitionistic logic is classical logic minus one axiom. That is true, it is the right way in, and it leaves an impression that is false — that there are two logics with one step between them.

Adding excluded middle to the constructive system is one step. There are many smaller ones.

An axiom is a class of algebras #

The middle that is not excluded records the theorem the whole apparatus rests on: intuitionistic logic proves exactly what holds in every Heyting algebra. So the system is determined by the class of all Heyting algebras, and adding an axiom restricts the class to those validating it.

Classical logic is what is left when the class is cut down to the Boolean algebras — the ones where negation is complement and nothing has a boundary. Between the two lies every class that can be cut out by axioms, and a logic in this sense is such a class.

That reformulation is what makes the question answerable. Two axioms give the same logic exactly when they cut out the same class, and they give different logics exactly when some algebra validates one and not the other. So proving two logics different means exhibiting one algebra — and the algebras can be small.

Three axioms, and what separates them #

The hero figure’s four rows are the three genuine candidates plus a control, and each is worth naming.

Excluded middle, $p \vee \neg p$, is the strong one and fails in every algebra with a boundary. The three-element chain refutes it: taking $p$ to be the middle element, $\neg p$ is the bottom and the join is the middle, not the top.

The weak law, $\neg p \vee \neg \neg p$, is strictly weaker. It says that a statement is either refutable or not-refutable — which is excluded middle applied to negated statements, and negated statements are where the two logics agree. The three-element chain validates it, so it is genuinely weaker; the five-element algebra of two incomparable points below one top refutes it, since there the two atoms’ negations are each other and their join falls short of the top.

The linearity axiom, $(p \to q) \vee (q \to p)$, says that any two statements are comparable. It holds in every algebra that is a chain and fails as soon as two elements are incomparable, which the same five-element algebra provides.

And three negations collapsing, $\neg\neg\neg p \to \neg p$, is the control. It is a theorem of the constructive system, so it must hold in every Heyting algebra, and a table showing it failing anywhere would mean the algebras were built wrongly. The figure requires that it holds in all four.

The weak law, worked through one algebra #

The weak law is the one worth following in detail, because it is the axiom that sounds like excluded middle and is not.

Take the five-element algebra of two incomparable points $x$, $y$ below a top $t$. Its downsets are $\emptyset$, $\{x\}$, $\{y\}$, $\{x,y\}$ and everything. Now $\neg\{x\}$ is the largest downset whose intersection with $\{x\}$ is empty, which is $\{y\}$; and $\neg\{y\}$ is $\{x\}$. So $\neg\neg\{x\} = \neg\{y\} = \{x\}$, and

$$\neg\{x\} \vee \neg\neg\{x\} = \{y\} \vee \{x\} = \{x, y\},$$

which is not the top. The weak law fails.

What the same algebra says about the other axioms is the interesting part. Excluded middle fails there too, of course. Linearity fails, since $\{x\}$ and $\{y\}$ are incomparable. And three negations collapse, as they must. So one five-element algebra refutes three axioms at once and validates the theorem — which is why a table of a few algebras against a few axioms separates as much as it does.

The infinite algebra that essay draws behaves differently, and the difference is instructive. In the open sets of a line the weak law holds: the negation of an open set is always a regular open set, and the double negation of a regular set is itself, so $\neg U \vee \neg\neg U$ is a union of two regular sets whose closures cover the line. So no picture of intervals refutes the weak law, and a finite algebra with incomparable atoms does it in five elements.

How many logics there are #

The three axioms give three different logics and the count does not stop there. The theorem is that there are uncountably many logics between the constructive system and the classical one — a continuum of them — and the shape of the proof is worth having because it is a counting argument rather than a construction of each.

Take an infinite family of finite algebras, each refuting a formula that the others validate. Then for every subset of the family there is a logic — the one whose axioms are the formulas the subset’s algebras validate — and different subsets give different logics, because an algebra in one and not the other separates them. Uncountably many subsets, uncountably many logics.

Constructing such a family is the work, and Jankov did it in 1968 by building, for each finite algebra, a formula that fails in that algebra and holds in every algebra not containing it as a piece. Those formulas are independent in exactly the sense the counting needs.

So “classical logic is constructive logic plus one axiom” is true and says nothing about the distance, in the same way that “the reals are the rationals plus the limits” is true and hides a continuum. The one step is a long one and the space inside it is not sparse.

The named ones, and why they are named #

Uncountably many logics exist and a handful have names, which is the usual situation. The named ones are the ones with a model class somebody recognised.

Gödel–Dummett logic is the constructive system plus linearity, and its algebras are exactly the chains. That is a clean description and it is why the logic has a name: a linearly ordered Heyting algebra is a natural object, and the logic is what those validate.

Jankov’s logic is the constructive system plus the weak law, and its algebras are the ones in which the elements with no boundary are dense — a condition on the topology of the model rather than on its order.

Kreisel–Putnam logic adds an axiom about how a negation distributes over a disjunction, and it is named because of what it does not do: it was expected to imply the disjunction property’s failure and does not, so it was the first example of a logic strictly between with the disjunction property intact.

Each name marks a class somebody found worth describing, and the uncountably many others are the ones nobody has had a reason to name. That is a statement about mathematical attention rather than about logic, and it is worth keeping in view when a list of named systems is mistaken for a list of systems.

Where the open sets fit #

The excluded middle draws its algebras as open sets of a line, and every algebra on this page is of that kind — the downsets of a finite order are the opens of a finite topological space, and Birkhoff’s theorem says every finite Heyting algebra arises this way.

So the finite part of the theory is entirely topological, and the axioms become conditions on a space. Excluded middle says every open set is its own double negation, which for a space means every open set is dense in its closure’s interior — the boundaries have to be empty. The weak law says the sets with empty boundary are dense. Linearity says the opens are linearly ordered, so the space is a chain.

The figures check that each algebra really is a Heyting algebra rather than assuming it: for every triple of elements they verify that the implication is the largest element whose meet with the antecedent lies below the consequent, which is the defining property and is what would fail if the construction were wrong.

The Boolean algebras, as the far end #

It is worth checking what the apparatus says about the classical system, because the answer is that classical logic is a class of algebras like any other and its class is small.

A Heyting algebra validating excluded middle has $\neg\neg a = a$ for every element, which is the statement that every element is regular — and a Heyting algebra in which every element is regular is a Boolean algebra. Conversely every Boolean algebra validates excluded middle. So the classical logic’s class is exactly the Boolean algebras.

The finite ones are the powers of two: the downsets of an antichain of $n$ points, which are all $2^n$ subsets. So among finite algebras the Boolean ones are exactly those of size a power of two arising from a poset with no relations, and every other finite Heyting algebra refutes excluded middle.

That is a complete answer at the top of the space and the shape of it is worth noticing. The class is closed under the operations that build new algebras, it is defined by a single equation, and it is as small as a non-trivial class can be. Nothing similar is available in the middle of the space, where a logic’s class is cut out by an axiom nobody has a structural description of.

The chain of size two is the smallest Boolean algebra and is the one a truth table computes in: two values, and a formula is a function of its variables. Every classical tautology is a statement about that one algebra, and the reason the constructive system proves fewer is that it has to satisfy all the others as well.

What the finite algebras cannot do #

They cannot give every logic. A logic is determined by all its algebras and some logics are not determined by their finite ones — a formula can hold in every finite algebra validating the axioms and fail in an infinite one. Such a logic lacks the finite model property, and refutable in something small is about the ones that have it.

And they cannot be enumerated usefully past a few points. The search here runs over every order on up to four points, which is twenty-three algebras — the search the small refutations run. Five points is a few hundred orders and a few hundred algebras; ten points is out of reach, and the interesting separations for the less-familiar axioms need larger algebras than any exhaustive search reaches.

Nor do they say which axioms are natural. Every one of the uncountably many logics is a perfectly good formal system, and nothing in the apparatus distinguishes Gödel–Dummett logic from an arbitrary member of the continuum. What distinguishes them is that somebody recognised the model class, which is not a property the algebras carry.

What the pictures cannot show #

The tables are finite and the claim about a continuum is not a claim about anything drawable. What the figures establish is that particular axioms are different, which is the ingredient the counting argument needs; the argument itself is a bijection with the subsets of an infinite set.

The algebras are drawn as element counts rather than as lattices, so their shape has to be read from the order’s description. A five-element algebra of two points below one is a specific lattice and the figure names it without drawing it, which is a real loss — the incomparability that refutes linearity is a picture and appears here as a word.

And nothing here shows an infinite algebra. The open sets of a line, which the excluded middle draws, form an infinite Heyting algebra, and the difference between what the finite ones validate and what all of them validate is the subject of the essay on small refutations and is invisible at any finite size.

The counting argument, in a little more detail #

The claim that there are uncountably many logics deserves one more paragraph, because the argument is short and the shape of it is reusable.

For each finite algebra $H$, Jankov’s construction gives a formula $\chi_H$ that fails in $H$ and holds in every algebra that does not contain $H$ as a quotient of a subalgebra. Now take an infinite family of finite algebras, no one of which is such a piece of another — an antichain of algebras under that relation.

For any subset $S$ of the family, consider the logic axiomatised by $\{\chi_H : H \notin S\}$. An algebra $K$ in the family validates all of those exactly when $K \in S$, since $\chi_K$ is in the axiom set precisely when $K \notin S$. So different subsets give logics with different members of the family, hence different logics.

The whole argument is that an antichain of algebras gives an independent family of axioms, and the rest is that a set has more subsets than elements. What has to be constructed is the antichain, and constructing an infinite antichain of finite Heyting algebras is where the work is — the standard one is built from a sequence of frames shaped so that none embeds in another.

That shape of argument is worth recognising because it is how a space of systems is shown to be large in general. Find an independent family of statements; the subsets give the systems; the count follows. Nothing about logic enters beyond the independence, which is why the same argument gives uncountably many modal logics, uncountably many varieties of algebra, and so on.

Still open: which logics have which properties #

The continuum of logics is not a catalogue and the properties that matter are distributed across it in ways that are only partly understood.

The disjunction property — that a proved disjunction has a proved disjunct — holds for the constructive system and fails for the classical one, and which intermediate logics have it is not settled. Kreisel–Putnam logic has it, infinitely many logics have it, and a characterisation of the ones that do is open.

Decidability is distributed too. The constructive system is decidable, the classical one is decidable, and there are intermediate logics that are not — which is a striking thing to be able to say about the space between two decidable systems, and it is proved by encoding an undecidable problem into the choice of axioms.

The question with the cleanest statement concerns the top of the space. Classical logic has exactly one logic immediately below it, which is the one Jankov identified, so the space has a well-defined penultimate level. How the space looks near the bottom — immediately above the constructive system — is much less clear, and the number of logics immediately above it is known to be infinite.

A second model class, for the same reason as before #

An earlier essay makes a point about having two model classes for one logic — open sets and stages of knowledge — and the same holds for every logic on this page, which is worth stating because it doubles what each axiom means.

A Kripke model is an ordered set of stages, and the downsets of that order are exactly a Heyting algebra. So the algebras here are Kripke frames: the four-element algebra is the three-stage chain, and the five-element one is the frame with two incomparable stages below a later one.

Read that way, each axiom is a condition on the frame. Excluded middle needs every stage to be final, since a stage with a later one has something not yet established and not refutable. Linearity needs the stages to be linearly ordered. And the weak law needs every stage to have a unique maximal continuation — which is a condition nobody would write down from the algebra and is immediate from the frame.

So an axiom has two readings and neither is the definition. The algebra says which computations the connectives perform; the frame says what the axiom requires of how knowledge can branch. The second is usually the one that explains why anybody would adopt the axiom, and the first is the one a search can check.

What the framing cost #

Classical logic is constructive logic plus one axiom is a good sentence and it misleads in one specific way: it suggests the two systems are adjacent. They are not, and the correction is not a technicality — it changes what the subject is about.

If there were two logics, the question would be which is right. With a continuum of them the question becomes which model class one is working in, and that is a mathematical question with a mathematical answer in each case: the chains, the spaces with dense interiors, the Boolean algebras. The dispute the excluded middle records as a quarrel becomes a choice of structure, and a choice of structure is what exhibiting a model always converts a dispute into.

The habit worth carrying is about the shape of the correction. When a system is described as another plus one axiom, the useful question is what the axioms between them are — and if the two are separated by a class of models rather than by a proof, the answer is usually a great many.