Matpic
mathematics, in pictures
Generator

A set, its negation, and its double negation

A generator in the logic library, called 59 times across 11 essays. Below: what it draws with nothing chosen and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

opens is one function. Everything below came out of it during this build, at parameters taken from the essays rather than invented for this page — so a figure here is the same figure a reader meets in an essay, and if the generator changes, this page changes with it.

With nothing chosen

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.

Three truth values, two of which count as holding

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.

Which classical rules survive a contradiction

Which classical rules survive a contradiction. A table of eight classical rules checked in classical logic, the logic of paradox and Kleene's gap logic, with a countermodel wherever a rule fails.

Same tautologies, fewer consequences

Same tautologies, fewer consequences. Counts over 56 two-variable formulas: 9 tautologies classically and in the logic of paradox, none in the gap logic; 1147 of 1313 valid inferences survive.

What follows from a body of information with one contradiction

What follows from a body of information with one contradiction. A table of nine questions put to four premises containing a contradiction: classically all follow; in the logic of paradox only the premises' own claims and s ∨ ¬s do.

Belnap's four values on one diamond

Belnap's four values on one diamond. The four values true, false, both and neither arranged in a diamond: truer upwards, more information to the right; true and both shaded as holding.

What it checks while it draws

Collected by running the family and recording what it asserted, not written here. The count is how many separate times the claim was put to the test while these drawings were made.

Where it is called

Every figure on this list is drawn by the same rule, so a change to the rule changes all of them at once. That is why the list is published.

Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

 Logic

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.

The whole library · What the figures prove