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 10 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 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.

logic · Non classical logic Four proofs about numbers, and what they compute. λn f x. n (λy. f y) (f x) computes n + 1; λn f x. n (λy. f (f y)) x computes 2n; λn f x. n (λy. n (λz. f z) y) x computes n²; λn f x. n (λy. x) (f x) computes 1 at 0, else 0.

What a proof about numbers can compute

The proofs of (o → o) → o → o without detours are the whole numbers, one for each count of how often the assumption is used. A proof of the implication from that formula to itself therefore takes a number and returns one, and removing its detours computes the answer. Enumerating all 14,659 such proofs up to size 16 finds 299 different functions — sums, products, squares, cubes, tests on zero — and not one of them subtracts. The predecessor, n − 1, is not among them, and a single line about polynomials says it never will be.

logic · Proof systems Raising the input's type, and what becomes computable. N[o]: 299 functions, 0 not extended polynomials; N[o → o]: 163 functions, 42 not extended polynomials; N[(o → o) → o]: 128 functions, 46 not extended polynomials; N[o → o → o]: 72 functions, 33 not extended polynomials.

One type up

A numeral is an iterator, and the formula it proves fixes what it may iterate. At the lowest type it can only repeat the successor, and every function it computes is a polynomial — no predecessor. Let the same numeral iterate a function on functions and 2ⁿ appears; let it iterate a function that takes a function and returns a value, and the predecessor appears at size 15; let it iterate a pair of values, and the predecessor, halving and parity all arrive at size 16. The trick is Kleene's, from 1932, and an exhaustive search finds it without being told.

logic · Proof systems Ackermann's function as one polymorphic term. A : N → N → N; A(0,0)=1 in 6 steps, A(0,1)=2 in 6 steps, A(0,2)=3 in 6 steps, A(0,3)=4 in 6 steps, A(0,4)=5 in 6 steps, A(0,5)=6 in 6 steps, A(1,0)=2 in 10 steps, A(1,1)=3 in 13 steps, A(1,2)=4 in 16 steps, A(1,3)=5 in 19 steps, A(1,4)=6 in 22 steps, A(1,5)=7 in 25 steps, A(2,0)=3 in 17 steps, A(2,1)=5 in 33 steps, A(2,2)=7 in 55 steps, A(2,3)=9 in 83 steps, A(2,4)=11 in 117 steps, A(2,5)=13 in 157 steps, A(3,0)=5 in 37 steps, A(3,1)=13 in 191 steps, A(3,2)=29 in 881 steps, A(3,3)=61 in 3795 steps, A(3,4)=125 in 15765 steps.

One type for every use

In the simply typed calculus a numeral must be told in advance what kind of thing it will iterate, and with input and output of one type it computes only polynomials with tests. Let a single type stand for every type — a numeral is then a term of type ∀X. (X → X) → X → X, used at whatever type each occasion needs — and the same few symbols compute subtraction, exponentials and Ackermann's function, which grows faster than anything built from primitive recursion. Every run still finishes, and the proof that it does lies just beyond the reach of second-order arithmetic.

logic · Proof systems

Named alongside it

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

Proof systemComputationSatisfiabilityTerminationTruth functionCompletenessHypercubeLiteralPolynomialRecursionRefutationResolution

All concepts