Non classical logic — the series

A set, its negation, and its double negation. Four bars on one number line showing an open set, its negation, their union, and the double negation.

The middle that is not excluded

Either it is raining or it is not. Drop that as an axiom and what is left is still a logic — one with models made of open sets and of stages of knowledge, in which a set and its negation between them miss the boundary.

part 1 · logic

4 axioms against 4 finite algebras. A table of candidate axioms against finite Heyting algebras built from small orders, marking which algebras validate which axiom at every valuation.

Not one step but a continuum

Classical logic is the constructive system plus one axiom, which makes it sound as though there are two logics and one gap. There are uncountably many logics in that gap, each one a class of algebras, and the smallest separations between them fit in five elements.

part 2 · logic

The smallest algebra that refutes each formula. A table of formulas against the smallest finite Heyting algebra refuting each, found by searching every order on a few points, with the formulas no such algebra refutes marked.

Refutable in something small

A formula that is not a theorem of the constructive system fails in some finite algebra, and the algebra can be found by search. That single property is what makes the propositional logic decidable — and the predicate version loses the property and the decidability with it.

part 3 · logic

Gluing two countermodels: p ∨ ¬p. Two small Kripke models, each refuting one half of a disjunction, and the model made by placing both above a new first stage, at which neither half is forced.

A proof that says which half

Classical logic proves p ∨ ¬p without any idea which half is true. The constructive system never does that: whenever it proves a disjunction, it proves one of the two halves. The reason is a picture — two countermodels placed side by side above a new first stage that forces neither — and the logics between the two lose the property exactly when their pictures are not allowed to be glued.

part 4 · logic

Which chains of truth values validate Gödel's disjunctions. A grid of Gödel's pigeonhole formulas in m letters against chains of n truth values, marking which chains validate which formula, forming a staircase where m exceeds n.

No table of truth values is enough

Two truth values decide classical logic. Gödel asked in 1932 whether some longer list of values could decide the constructive system, and answered with a pigeonhole: with n values, some two of n + 1 statements must share one, so a formula saying exactly that holds in every n-valued table and is not a theorem. The chains of truth values then descend forever, and what they share is a logic of its own — the logic of the real interval.

part 5 · logic

Six formulas on the interval of truth values. Graphs on [0, 1] of six one-variable formulas of Łukasiewicz logic, each a zigzag of whole-number slopes with values 0 or 1 at the ends.

The zigzags a formula can draw

Let truth be any number from 0 to 1, and Łukasiewicz's connectives turn every formula in one variable into a graph. Every graph that appears is a zigzag of straight pieces with whole-number slopes, ending at 0 or 1 — and McNaughton proved in 1951 that every such zigzag appears. A logic of degrees of truth turns out to be a theory of piecewise-linear functions with integer coefficients.

part 6 · logic

Three truth values, two of which count as holding. Truth tables of negation, conjunction and disjunction in the logic of paradox, with the values that count as holding — both and true — shaded.

A contradiction that stays where it is

In classical logic one contradiction proves everything: from p and not-p, any q at all. Add a third truth value — both true and false — and count it as holding, and the explosion stops. The classical laws all survive as laws; what goes is exactly the reasoning that carries a contradiction somewhere it was not. Run the other way, the same three tables make a logic of gaps instead of gluts.

part 7 · logic

Nine bases that cannot each have one true direction. Eighteen vectors (0, 0, 0, 1) (0, 0, 1, 0) (1, 1, 0, 0) (1, −1, 0, 0) (0, 1, 0, 0) (1, 0, 1, 0) (1, 0, −1, 0) (1, −1, 1, −1) (1, −1, −1, 1) (0, 0, 1, 1) (1, 1, 1, 1) (0, 1, 0, −1) (1, 0, 0, 1) (1, 0, 0, −1) (0, 1, −1, 0) (1, 1, −1, 1) (1, 1, 1, −1) (1, −1, −1, −1); vector i joins bases 1–2, 1–5, 1–3, 1–7, 2–5, 2–8, 2–4, 3–4, 3–6, 3–7, 4–6, 4–8, 5–9, 5–6, 6–9, 7–8, 7–9, 8–9; near-solution true: 2, 6, 10, 11, basis B9 empty.

No way to hand out true and false

Birkhoff and von Neumann read the propositions of quantum mechanics as subspaces, with "and" the intersection and "or" the span. Three lines in a plane already break the distributive law. Kochen and Specker proved something stronger: the propositions cannot be called true and false at all, if every complete measurement is to have exactly one true outcome. Cabello's eighteen directions in four dimensions show why in one line of arithmetic — nine bases, each direction in two of them, and nine is odd — and a search of all 262,144 assignments confirms it.

part 8 · logic

Thirty-three directions nobody can label. Peres set: 33 rays, 16 triads, 72 orthogonal pairs, 0 colourings. Rays: (0, 0, 1) (0, 1, 0) (1, 0, 0) (0, 1, 1) (0, 1, −1) (1, 0, 1) (1, 0, −1) (1, 1, 0) (1, −1, 0) (0, 1, √2) (0, 1, −√2) (0, √2, 1) (0, √2, −1) (1, 0, √2) (1, 0, −√2) (1, √2, 0) (1, −√2, 0) (√2, 0, 1) (√2, 0, −1) (√2, 1, 0) (√2, −1, 0) (1, 1, √2) (1, 1, −√2) (1, −1, √2) (1, −1, −√2) (1, √2, 1) (1, √2, −1) (1, −√2, 1) (1, −√2, −1) (√2, 1, 1) (√2, 1, −1) (√2, −1, 1) (√2, −1, −1).

Thirty-one directions nobody can label

In four dimensions eighteen directions are enough to show that quantum measurements cannot have answers waiting in advance, and a parity count does it in a line. In three dimensions, where Kochen and Specker first proved it, no parity count works and the smallest known set has thirty-one directions. Peres's thirty-three can be checked by hand; Conway and Kochen's thirty-one fall out of a search through every direction with coordinates between −2 and 2; and whether thirty or fewer could ever do is still being settled by exhaustive computation, which has so far ruled out everything up to twenty-four.

part 9 · logic

Twenty-two states and 265,454 formulas. two letters, depth two: 4 final states and 18 below; 265454 up-sets; lower states q below p q, p below p q, – below p q, – below q, – below p, q below p q/q, – below p q/q, p below p q/p, – below p q/p, – below p q/–, – below q/p, – below q/–, – below p/–, – below p q/q/p, – below p q/q/–, – below p q/p/–, – below q/p/–, – below p q/q/p/–.

The second letter breaks the pattern

In one letter the constructive logic has infinitely many formulas, but they climb in a column two wide, four new ones for every step a state of knowledge can take. Add a second letter and the pattern is gone: sixteen formulas at the last step, 265,454 one step back, and more than two to the power 265,428 one step further. Every one of those is a genuine formula, and the reason the two-letter lattice has never been drawn is that each layer of the model is about as large as the number of formulas the layer above can tell apart.

part 10 · logic

Excluded middle fails at one point, and its double negation does not. Open sets of the real line as truth values: p = (0, ∞), ¬p = (−∞, 0), p ∨ ¬p misses 0, ¬(p ∨ ¬p) is empty and ¬¬(p ∨ ¬p) is the whole line.

Every tautology survives double negation

Intuitionistic logic refuses excluded middle, Peirce's law and every other classical principle that claims more than can be shown. Glivenko proved in 1929 that it refuses nothing outright: put ¬¬ in front of any classical tautology and the result is intuitionistically valid. Every Kripke model of up to four states confirms it for eight famous laws, a census of 11,451 formulas confirms it one by one, and a model with a growing domain shows where it stops.

part 11 · logic