Matpic
mathematics, in pictures
Concept

Normal form

A standard way of writing an expression, chosen so that equivalent expressions written that way are identical. Having one turns the question of whether two expressions are equal into the question of whether two strings are identical.

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

(p ∨ q) ∧ ¬r, drawn on the cube of 8 assignments. The assignments as corners of a cube, joined when they differ in one variable, with the satisfying corners filled.

A formula is a corner of a cube

A formula about three letters is a set of eight rows. Written as a table that is a list; drawn on a cube it is a shape — and the shape is what almost every later question in this field turns out to be about.

logic · Truth functions ((p ∧ q) ∨ (r ∧ s)) ∨ (¬p ∧ ¬r), covered by 3 rectangles. A grid of the assignments arranged so that neighbouring squares differ in one variable.

The map that puts neighbours side by side

Reorder the rows of a truth table so that neighbouring squares differ in one letter, and finding a short formula stops being algebra and becomes the problem of covering a shape with rectangles.

logic · Truth functions A resolution refutation of four clauses on three variables. A derivation tree: the given clauses at the top, each later clause obtained by cancelling one variable between two clauses above it, ending in the empty clause.

A proof with one rule

Two clauses that disagree about exactly one variable can be combined into a third that forgets it; repeat, and if the clauses cannot all be true the empty clause eventually appears — a complete proof system with a single move.

logic · Resolution 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 5 two-literal clauses drawn as 10 arrows. The literals of four variables arranged in a circle with an arrow for each implication a two-literal clause contains, the arrows forming a path from one literal to its negation and back highlighted, beside the list of clauses and their arrows.

Two literals make an arrow

A clause of two literals, p ∨ q, says that if p is false then q is true, and if q is false then p is true — two arrows. A set of such clauses is a directed graph on the literals, and it is unsatisfiable exactly when some variable and its negation reach each other. Each of those two paths is a chain of resolution steps, and finding them takes time proportional to the size of the input.

logic · Resolution Reducing abcabc to a standard form. The gluing word abcabc rewritten step by step into one of the classification's standard forms, with the move used and the two invariants recomputed at each step.

Every word driven to a normal form

The classification is usually met as a statement: two numbers name the surface. The proof is a procedure — a short list of cut-and-reglue moves that drive any gluing word to one of the standard forms, with a measure that never rises to say why the procedure stops.

topology · Surface classification

Named alongside it

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

SatisfiabilityHypercubeLiteralRefutationResolutionTruth functionAssignmentCompletenessConnectiveCountabilityCoveringDecision procedure

All concepts