Generator

ef-game

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

ef-game 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

3 rounds on chains of 4 and 5. Two chains of dots with pebbles placed in turn, and the transcript of a play: Spoiler picks an element of one chain, Duplicator answers in the other, and the pebbles must keep the same order.

`show: "table"`

`show: "depth"`

Rounds needed to tell a chain from one element longer. A bar for each chain length, showing how many rounds of the game Spoiler needs to distinguish it from a chain with one more element. The counts climb like a logarithm.

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.

at 1 rounds the search agrees with the rule that says same length or both at least 1 ×3
and it does grow ×1
between two and three round counts are tabulated ×1
so the count grows like a logarithm rather than like the length ×1
the game runs between one and four rounds ×1
the number of rounds Spoiler needs is computed ×1
the rounds needed against a chain one longer follow the logarithm of its length ×1
the sweep runs to between five and nine ×1
the table runs to between four and nine ×1
the transcript ends the way the exhaustive search says the game ends ×1
the view is one the family draws ×1
two chains of between two and nine elements ×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.

The whole library · What the figures prove