Matpic
mathematics, in pictures
Concept

Decidability

Whether some procedure settles every instance of a question in finite time. A logic is decidable when a non-theorem always fails in a small enough model to be found by search, which propositional systems manage and systems with quantifiers generally do not.

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

How many colourings each knot allows. Three knots, and the number of ways their arcs can be coloured with three, five and seven colours under the crossing rule, beside the determinant computed separately from the same crossings.

Colours that count more than three

Three colours prove the trefoil is knotted and say nothing at all about the figure-eight, which refuses them exactly as an unknotted loop does. The repair is to stop colouring and start counting — with five colours, or seven, and with the arithmetic done modulo the number of them.

topology · Knots 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.

logic · Non classical logic "There is an x" is a shadow: x² + ax + 1 = 0 has a solution exactly when |a| ≥ 2. A grid with a horizontal and x vertical, marking the cells the curve x squared plus a x plus one equals zero passes through; beneath it, a strip marking the columns that contain a mark, which are exactly those with a at least two in size.

A quantifier is a shadow

'There is an x such that …' asks whether a column of a grid contains a mark — which is the same as asking whether a shape casts a shadow on the axis below it. Over the real numbers every such shadow can be described without the quantifier, by polynomial inequalities: 'x² + ax + 1 = 0 has a solution' is just a² ≥ 4. Over the whole numbers the same kind of shadow can carve out the primes, and any set a computer can list.

logic · Quantifiers Addition as a machine with two states. Two-state carry automaton over columns (x, y, z): from carry 0 staying on 000 011 101, to carry 1 on 110; from carry 1 staying on 010 100 111, back on 001.

A machine that carries one bit

Write three numbers in base two, one above another, and read the columns from the right. Whether the bottom number is the sum of the top two can be checked with one bit of memory — the carry. That two-state machine is the whole of addition, and machines can be combined, negated and made to guess a missing number. So every sentence about whole numbers built from addition can be decided by building a machine for it, and the same machines can also handle 'x is a power of two', which addition alone cannot say.

logic · Quantifiers Every three-state machine and what becomes of it. halt: 1379; no halting entry: 12492; exact repeat: 361; shifted repeat: 2254; dies backwards: 36; unexplained: 27.

The machines that need a reason never to stop

Run every three-state machine on a blank tape and the ones that halt announce themselves: the longest stops after 21 steps. The work is in the others. Each needs a reason it will never stop, and four simple kinds of reason settle all but 27 of them — machines that sweep back and forth over a growing tape and defeat every check that looks for a repeat.

logic · Diagonalisation A subword can be checked with one quantifier block; a factor cannot. Subword aba: monoid 7, J-trivial, degree 3; factor aba: monoid 12, aperiodic, not J-trivial; witness abab / abba.

One block of quantifiers, read off an algebra

Which properties of words can be stated with existential quantifiers alone — 'there are positions, in this order, carrying these letters' — and Boolean combinations of such statements? Imre Simon answered in 1975: exactly those whose syntactic monoid is J-trivial. Of the 57,068 languages that automata of up to four states recognise, 848 pass the test, and every one of them is decided by which words of length three or less it contains as scattered subwords.

logic · Ehrenfeucht–Fraïssé games

Named alongside it

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

Exhaustive searchQuantifierFinite automatonAssociativityBinaryBusy beaverClassificationComputer-assisted proofCounting argumentDecision procedureDiscriminantDouble negation

All concepts