Generator

Order types drawn on the line: ω, ω+1, ω·2, ω²

A generator in the logic library, called 35 times across 9 essays. Below: what it draws with nothing chosen and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

ordinal is one function. Everything below came out of it during this build, at parameters taken from the essays rather than invented for this page — so a figure here is the same figure a reader meets in an essay, and if the generator changes, this page changes with it.

With nothing chosen

Order types drawn on the line: ω, ω+1, ω·2, ω². Number lines with tick marks accumulating at limit points, one line per order type.

The Goodstein sequence from 3, with the ordinal beside each term

The Goodstein sequence from 3, with the ordinal beside each term. A table of the Goodstein sequence with each term's hereditary representation and the ordinal obtained by replacing the base with omega.

The fast-growing hierarchy at its first few ordinals

The fast-growing hierarchy at its first few ordinals. A table of the fast-growing hierarchy: one row per ordinal index, one column per argument, with the cells too large to evaluate marked as such.

Limit ordinals and the sequences that approach them

Limit ordinals and the sequences that approach them. Several ordinals with the first terms of their fundamental sequences, and the successors marked as having a predecessor instead.

The numbers to 18 in hereditary base 2, and their ordinals

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.

Ordinal sums and products, in normal form

Ordinal sums and products, in normal form. A table of ordinal expressions with their Cantor normal forms and whether the two sides of each pair are equal, above two tick lines drawing one such pair.

What it checks while it draws

Collected by running the family and recording what it asserted, not written here. The count is how many separate times the claim was put to the test while these drawings were made.

Where it is called

Every figure on this list is drawn by the same rule, so a change to the rule changes all of them at once. That is why the list is published.

Logic

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

A sequence that explodes and still stops

Goodstein's sequence starting at 4 climbs past any number you care to name and reaches zero after about ten to the hundred and twenty million steps. The proof that it stops is a second sequence, running alongside it, that goes down.

Logic

An ordinal as a growth rate

Index a family of functions by the ordinals, each one iterating the last, and the index becomes a measure of how fast a function grows. The point where the index leaves what arithmetic can prove is exactly where the Goodstein sequence became unprovable.

Logic

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

One step in front of infinitely many

Put one step before an infinite run of them and nothing has changed; put it after and something has. Ordinal addition records that difference, which is why it is not commutative — and why it keeps information that counting throws away.

Logic

Reached from below, or not at all

Every limit ordinal anybody meets is the end of an increasing sequence — ω, ω·2, ω^ω, all of them approached one step at a time. The first uncountable ordinal is not, and the reason it is not constrains the size of the continuum.

Logic

The arithmetic that loses subtraction

Adding one to an infinite collection changes nothing, and neither does doubling it, or squaring it. What that costs is the two operations that were doing the work — an equation between infinite sizes cannot be cancelled, and how many are left stops being a question.

Logic

The choice nobody can write down

Given finitely many pairs, picking one thing from each is a finite list of decisions and needs no justification. Given infinitely many, the list cannot be finished — and whether one exists anyway is an axiom, independent of everything else, whose consequences include a theorem most people refuse to believe.

Logic

The size that cannot be pinned down

There is no largest infinity, because no collection has as many members as it has sub-collections. What is not settled is whether anything sits between the first two — and that is not an open problem but a proved absence of an answer.

The whole library · What the figures prove