Concept

Decision procedure

A method guaranteed to halt on every input and report a correct yes or no. Whether one exists is a separate question from whether the answer is determined, and for some questions it provably does not.

Named by 20 essays across 5 fields — each of them below, with the objects they name alongside it.

The 256 syllogistic forms, and the 24 that work. A grid with one cell per syllogistic form, marked according to whether it is valid and what it needs to be valid.

Twenty-four out of two hundred and fifty-six

Aristotle's syllogisms are four sentence forms in four arrangements, which makes 256 patterns of argument. Fifteen of them are valid. Nine more become valid if you assume the things being talked about exist, and the gap between those numbers is a two-thousand-year-old disagreement.

logic · Class diagrams
A tableau for ((p → q) ∧ (q → r)) → (p → r). A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.

The tree that closes

To prove a formula, assume it false and take it apart. Every branch ends in a contradiction, or one of them describes exactly how it could have been false — and either way the tree is the answer, drawn.

logic · Proof systems
The syndrome of 1011010, and the bit it names. A parity-check matrix over a received word, with the resulting syndrome matched against the table of single-error syndromes.

Finding the error without reading the message

Three parity checks on a seven-bit word produce three bits. If they are all zero nothing is wrong; otherwise they are the number of the position that broke. The message is never consulted, because the answer does not depend on it.

computation · Error-correcting codes
5,040 orders, 7 thresholds, one best rule. For each number of candidates passed over, the share of the 5,040 possible arrival orders in which the rule ends up with the best of the 7. The count is exhaustive.

When to stop looking

Candidates arrive one at a time in a random order. Each must be accepted or rejected on the spot, with no going back and no way to know what is still to come. The best possible rule is to look at about a third of them and then take the first one that beats everything seen — and it works about a third of the time, however many there are.

probability · Optimal stopping
3 rounds on chains of 4 and 5. Two chains of dots with pebbles placed in turn, and the transcript of a play: Spoiler picks an element of one chain, Duplicator answers in the other, and the pebbles must keep the same order.

A game that decides what can be said

Two players take turns pointing at elements of two structures; if the second can survive k rounds, then no sentence with k quantifiers tells the structures apart — a statement about infinitely many formulas, settled by a finite search.

logic · Ehrenfeucht–Fraïssé games
The numbers to 18 in hereditary base 2, and their ordinals. A table of small whole numbers written in hereditary base notation beside the ordinal obtained by replacing the base with omega.

Every ordinal in base omega

Every ordinal below a certain point is a descending sum of powers of ω, in exactly one way. That notation makes comparison mechanical, it is what hereditary base notation becomes when the base is replaced, and it stops at the first ordinal it cannot name.

logic · Ordinals
A path of 4 bounces that closes, in a triangle of 100°, 40°, 40°. A triangular billiard table with a periodic path found by an exhaustive sweep of starting positions and directions.

The triangle nobody can settle

Does every triangular billiard table have a path that closes on itself? Acute triangles do, right triangles do, triangles with rational angles do — and for the rest the question has been open since it was asked.

dynamics · Billiards
Two models the modal language cannot separate, and two it can. Four Kripke models in two pairs: the upper pair joined by a bisimulation and agreeing on every formula, the lower pair separated by a formula found by search.

Two diagrams the language cannot tell apart

A modal formula sees a diagram of worlds and arrows through a very narrow window. Exactly how narrow is settled by a game: where one player can answer every move, no formula whatever separates the two starting worlds, however different the diagrams look.

logic · Modal logic
A model whose worlds are sets of sentences. Worlds labelled by which of a fixed finite set of formulas they accept, with an arrow wherever every boxed formula accepted by one has its inside accepted by the other.

Worlds built out of sentences

A Kripke model needs worlds, and nothing so far has said where worlds come from. They can be made of the syntax: a world is a set of formulas it commits to, one world sees another when the boxed commitments line up, and in the model that results every formula is true exactly where it was assumed.

logic · Modal logic
A chain of 18 worlds, and the 3 the formulas can tell apart. A row of 18 circles for the worlds of the model, shaded by which of the 3 classes each falls into, above the quotient model's 3 worlds with the arrows the collapse gives them.

How many worlds a formula can need

A modal formula can be true in a model with infinitely many worlds. It can also be true in a small one — and the small one is built from the large one by throwing away every distinction the formula was never able to make.

logic · Modal logic
A lemma, and the proof that never mentions one. Two derivations of ((p → q) ∧ (q → r)) → (p → r) compared: the cut-free one uses 8 nodes and only subformulas of the goal, and the one through a lemma uses 21 and mentions a formula the goal does not contain.

A lemma, and the proof that never mentions one

Proving something by first proving a lemma is what makes mathematics readable, and it is exactly what makes a proof system impossible to search — because the lemma can be any formula at all. Gentzen proved the step can always be removed, and the removal is not free.

logic · Proof systems
Closed after 3 uses of the universal. The Herbrand expansion of a first-order question at 5 stages, with the number of remaining models at each. It reaches nought after 3 instantiations.

The instance that has to be guessed

Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.

logic · Proof systems
58.6% at 46 candidates, against 37% without the values. The chance of ending with the best candidate when the values are shown, against the number of candidates, for 10 sizes. It falls towards 0.5802 rather than towards 1/e.

When the numbers are shown

The secretary rule wins a third of the time and cannot do better, because it is told only who is ahead. Show the actual values and say where they came from, and the same problem is won three times in five — by a standard that falls as the end approaches.

probability · Optimal stopping
About the fourth-best, whatever the size of the field. The smallest expected rank achievable by an online rule, against the number of candidates, for 10 sizes. It rises to 3.8516 at 2500 candidates and its limit is 3.8695.

Giving up on the best

The secretary rule treats landing the second-best exactly as badly as landing the worst, which is a strange thing to want. Ask instead for the smallest average rank and the answer is about the fourth-best candidate — whatever the size of the field, and whether it is ten or ten million.

probability · Optimal stopping
An online rule taking nine tenths of what an oracle takes. The share of the oracle's expected maximum secured by the best single threshold, and by the threshold at the median of the maximum, for 8 field sizes of independent uniform values.

Half of what an oracle takes

Compare an online rule not against the best it could have done but against a rule that has seen every value in advance. One fixed threshold secures half of what the oracle collects, whatever the distributions are — and there is an example on which half is all there is.

probability · Optimal stopping
6 vertices folded to 4, and a graph that decides. The graph built from 3 generator words, folded until no vertex has two edges of one label leaving it. Reading a word from the base vertex decides membership, and 6 words are tested.

Folding a graph until it decides

A subgroup of a free group usually arrives as a list of words, and almost nothing about it is readable from the list. Draw the words as loops, merge every pair of edges with the same label leaving one point, and what is left is a machine that decides membership by reading.

topology · Covering spaces
Who survives with two pebbles and who with three, over 4 rounds. A table of three pairs of graphs with, for each, whether the duplicating player survives a two-pebble game and a three-pebble game played to a fixed depth.

The boundary at three variables

Restrict a sentence to two variable names and it can still be arbitrarily long, because the names are reused. What it cannot be is deep: every satisfiable two-variable sentence has a small model, so asking whether one is satisfiable is a bounded search. Allow a third name and the question becomes undecidable.

logic · Ehrenfeucht–Fraïssé games
A local rule taking a vote. A space-time diagram of the GKL rule on 149 cells from a random row with 69 ones. Black and white regions grow and meet along slanting boundaries, and after 69 steps the whole ring is 0.

No local rule can count the votes

A ring of cells, each holding 0 or 1, has to agree on whichever value is in the majority — every cell seeing only its neighbours. The best-known rule gets it right most of the time and wrong near a tie; no rule of any radius gets it right always. Yet two rules run one after the other do, on every ring, and the first of them is the traffic rule.

dynamics · Cellular automata
A smallest model of ∀x (Ax → ∃y (By ∧ ¬Cy)) ∧ ∃x (Ax ∧ Cx) ∧ ∀x (Bx → ¬Ax). Three overlapping circles with some regions shaded as empty and a single dot in each occupied region, forming a model of a sentence of monadic first-order logic.

One thing in each region is enough

Give first-order logic its full apparatus of nested quantifiers but only one-place predicates, and every question about truth is still settled by the regions of a diagram. A predicate cannot tell apart two things in the same region, so no model ever needs more than one thing per region — and with three predicates there are only 255 models to try.

logic · Class diagrams
Whole-number points in a strip, and the shadow they cast. The lattice points satisfying 2x ≤ 5y ≤ 2x + 1 for x from 0 to 30, and their projection onto the x-axis, which repeats every 5.

Arithmetic with addition alone

Over the real numbers, a quantifier's shadow is described by inequalities. Over the whole numbers with addition and multiplication, a shadow can be any set a computer can list. In between lies arithmetic with addition and no multiplication, and there the shadows are always the same kind of thing: a finite exception, then a pattern that repeats. The whole numbers made from coins worth 6, 9 and 20 are every number from 44 on; the squares, which need multiplication, never repeat at all.

logic · Quantifiers

Named alongside it

The objects these essays reach for when they reach for this one.

CompletenessExhaustive searchQuantifierConditional probabilityExpectationIrrevocable decisionModelOptimal stoppingProof systemThreshold ruleCounterexampleExpressive power

All concepts