Generator

j is one more than i, counting round — as a grid, with both quantifier readings

A generator in the logic library, called 22 times across 7 essays. Below: what it draws at its defaults and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

relation-grid 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.

At its defaults

j is one more than i, counting round — as a grid, with both quantifier readings. A grid of marks for a relation, with the row and column facts the two quantifier orders ask about.

`show: "membership"`

Does this set contain that one — and the row that is missing. A membership table with the diagonal marked, and beneath it the complement of the diagonal, which is not among the rows.

`show: "diagonal"`

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.

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.

a full column forces every row to carry a mark, so one reading implies the other ×1
no drawn row agrees with the built row everywhere it has been checked ×1
no row of the table is the Russell row ×1
the built row differs from row n in place n ×1
the drawn window is at least as wide as it is tall ×1
the labelling is one this figure knows ×1
the number of columns is a whole number between 2 and 14 ×1
the number of drawn columns is a whole number between 3 and 16 ×1
the number of drawn rows is a whole number between 3 and 12 ×1
the number of rows is a whole number between 2 and 14 ×1
the number of sets in the table is a whole number between 3 and 10 ×1
the relation is one this figure knows how to draw ×1
the Russell row disagrees with row k at column k ×1

Where it is called

Changing this generator changes every figure on this list. That is what makes the list worth publishing rather than keeping in a check script.

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 list that cannot contain itself

The set of all sets that do not contain themselves is not a set. The argument is the diagonal again, applied to a table whose rows and columns are the same objects, and it destroyed the foundations of mathematics in a postcard.

Logic

An infinite tree has an infinite path

A tree that goes on forever, in which every node has only finitely many children, must contain a single branch that goes on forever. The proof is a rule for walking, and the rule is the whole of why finite information can decide an infinite question.

Logic

Every row, or one column

For every person there is someone who loves them, and there is someone who loves everyone, are the same six words in a different order. Draw the relation as a grid and they become two obviously different questions — one about rows, one about columns.

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 row that is not on the list

Write down a list of infinite sequences, any list at all, and there is a rule that builds a sequence missing from it. The rule reads one entry from each row, and it is the single most reused argument in this field.

Logic

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.

The whole library · What the figures prove