Matpic
mathematics, in pictures
Concept

Incompleteness

The fact that any consistent formal system strong enough for arithmetic has true sentences it cannot prove, and cannot prove its own consistency. Both halves follow from one modal axiom about what provability implies.

Named by 4 essays across one field — each of them below, with the objects they name alongside it.

The diagonal, and the row built to be off the list. A table of rows of ones and zeros with the diagonal marked, and beneath it the row obtained by flipping every diagonal entry.

The sentence that says it has no proof

Number every sentence and every proof, and a formal system can talk about itself. Then the diagonal is available one more time, and what it builds is a sentence that is true exactly when it is unprovable.

logic · Diagonalisation The frames on which provability makes sense, and the two that are refused. Six small frames marked by whether Löb's axiom is valid on them: transitive frames with no cycles accept it, and any frame in which a world can reach itself does not.

Necessity that means provable

Read the box as "the theory proves" and one modal logic stops being a proposal about what necessity might mean. It becomes a complete description of what a formal system can prove about its own proofs — and its frames run forward, compose, and stop.

logic · Modal logic 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 What all small machines leave on the tape. All 16777216 two-symbol Turing machines with three states, run to step 22: 7571840 halt, leaving 95 distinct strings; most common 0 (2097152), 1 (2097152), 00 (722752); the longest strings are the rarest, up to 20.85 bits.

The shortest description nobody can certify

A string's complexity is the length of the shortest program that prints it. Counting shows almost every string has no short program, and diagonal arguments show nothing can compute the length, or even prove it large for any single string past a fixed point. All 16,777,216 three-state Turing machines leave only 95 strings on their tapes, and a compressor treats π exactly as it treats random bits.

logic · Diagonalisation

Named alongside it

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

Diagonal argumentFixed pointFormal systemProvabilitySelf-referenceArithmetisationCompletenessConsistencyCounting argumentDecision procedureExhaustive searchFrame

All concepts