Generator

A closed interval and an open one, matched point for point

A generator in the logic library, called 13 times across 3 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.

chains 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

A closed interval and an open one, matched point for point. Two number lines, one closed and one open, with arrows showing the countable sequence of points that has to move.

`show: "choose"`

Every way of choosing one thing from each of 4 pairs. A table with one row per choice function on a small family of pairs, each row giving what it takes from each pair, with the row a stated rule names picked out.

`show: "sets"`

Two injections shifted by 2 and 3, and the chains they cut. Two rows of dots with arrows for each injection, coloured by which chain each element belongs to.

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 choice from each of the pairs is one of two to the power of their number ×1
between two and five pairs, each of two named things ×1
each element belongs to exactly one chain ×1
every moved point lands strictly inside the open interval ×1
every point the map has to reach is reached ×1
no two moved points land on the same place ×1
the assembled map sends no two elements to the same place ×1
the left-to-right map sends different elements to different places ×1
the left-to-right shift is a whole number between 1 and 4 ×1
the members of a pair are named apart exactly when an order is claimed ×1
the number of elements drawn from each side is a whole number between 5 and 14 ×1
the number of sequence terms drawn is a whole number between 4 and 12 ×1
the pairs either carry an order or they do not ×1
the right-to-left map sends different elements to different places ×1
the right-to-left shift is a whole number between 1 and 4 ×1
the rule fits two to the power of the pairs it cannot tell apart ×1
the rule names exactly one of the rows exactly when the pairs carry an order ×1
the two maps are different, or there are no chains to see ×1
the view is one the family draws ×1
the window shows at least three chains ×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 line with as many points as a square

Interleave the decimal places of two numbers and one number comes out; take every other place back and the two return. The square has no more points than the segment, and dimension turns out to be invisible to counting.

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

Two injections make a bijection

If each of two collections fits inside the other without collisions, they are the same size. That sounds obvious and is not, because neither injection needs to be onto — and the proof is a rule for deciding which of the two to follow, one chain at a time.

The whole library · What the figures prove