Generator

3 rounds on chains of 4 and 5

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

`show: "words"`

Where a word of m letters stops being distinguishable from one of m + 1. A row for each quantifier depth and a cell for each length, shaded where Duplicator survives the game between words of that length and one longer.

`show: "monoid"`

Three regular languages, and the one no first-order sentence defines. A table of three languages with the size of each one's syntactic monoid, the largest period found among its elements, and whether that makes the language first-order definable.

`show: "local"`

What a sentence of depth 2 can reach. Two rings of points, of 14 and 19 points, each with a run of 9 consecutive points marked as the neighbourhood a sentence of depth 2 can inspect.

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
at depth 1 the words must be 1 letters before Duplicator survives ×3
by the largest size drawn, Duplicator survives 2 rounds on every pair sampled ×2
Duplicator survives 3 rounds on a cycle of 22 against two of 11 ×2
the search agrees with the rule that says Duplicator survives 3 rounds from 5 points up ×2
a star splits at the first round ×1
an even number of edges is a coin toss at every size, as the flip bijection says it must be ×1
and does not at the smallest ×1
and does not survive the three-pebble one ×1
and Duplicator survives at every length past it ×1
and it does grow ×1
and once Duplicator survives at one length it survives at every longer one ×1
and so do two triangles, which is why refinement cannot separate them ×1
and that object is a path ×1
and the group has order two ×1
and the share rises with the size rather than wandering ×1
and the two graphs have the same number of edges ×1
at every depth there is a length past which the two words cannot be separated ×1
between fifty and four hundred graphs at each size ×1
between four and twelve pairs of graphs at each size ×1
between ten and eighty graphs are sampled at each size ×1
between three and six graph sizes, each of four to sixty points ×1
between three and six rounds shown ×1
between three and six sizes, each of four to forty-four points ×1
between three and six sizes, each of three to forty points ×1
between two and four depths ×1
between two and three round counts are tabulated ×1
Duplicator survives the two-pebble bijective game ×1
every point of both graphs has two neighbours ×1
exactly half of the 64 graphs on 4 points have an even number of edges ×1
large ones almost never do ×1
one graph is connected and the other is not, so a sentence separating them would express connectedness ×1
one or two round counts, each of at most three ×1
one-dimensional refinement gives both graphs the same colours and cannot tell them apart ×1
small graphs usually fail the property ×1
so the count grows like a logarithm rather than like the length ×1
the cycle stays one colour at every round, since every point looks alike ×1
the deeper game needs a larger graph before Duplicator always survives it ×1
the depth is between one and three ×1
the first-order property "every pair has a common neighbour" has settled on 1 by the largest size drawn ×1
the first-order property "some point joined to nothing" has settled on 0 by the largest size drawn ×1
the first-order property "three points all joined" has settled on 1 by the largest size drawn ×1
the game agrees with the neighbourhood argument about who wins ×1
the game is played to at most three rounds, which is as far as a search finishes ×1
the game runs between one and four rounds ×1
the measured share agrees with the count of expected failures ×1
the number of colours never falls ×1
the number of rounds Spoiler needs is computed ×1
the other two monoids are aperiodic, so both languages are first-order definable ×1
the parity language's monoid contains a non-trivial group, so no first-order sentence says it ×1
the rounds needed against a chain one longer follow the logarithm of its length ×1
the sizes are listed in increasing order ×1
the sweep runs over between three and eight cycle lengths ×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 two cycles are of different lengths ×1
the two cycles have three points each ×1
the two graphs have the same number of points and the same number of edges ×1
the two neighbourhoods are the same object, computed from the cycles rather than named ×1
the two small cycles run to between three and thirteen points ×1
the view is one the family draws ×1
two chains of between two and nine elements ×1
two cycles of between five and thirty points ×1
two-dimensional refinement does tell them apart ×1
words up to between four and six letters ×1
words up to between six and twelve letters ×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 language that can name a set

Allow a sentence to quantify over sets of positions as well as positions, and on words the answer changes completely: the sets buy exactly the languages a finite automaton recognises. Whether the number of letters is even is the smallest example of what the sets are for.

Logic

Nearly always, or nearly never

Toss a coin for every pair of points and ask whether the graph that results has some property. For a property a first-order sentence can state, the answer in the limit is never a genuine probability — it is zero or it is one, and the game is what proves it.

Logic

The distance a sentence can see

A first-order sentence with three quantifiers cannot notice anything about a graph beyond a fixed distance from the points it names. That single limitation is why it cannot say connected, and why the failure survives every attempt to add more quantifiers.

Logic

The game the algorithm was playing

Change what Duplicator has to offer — a whole bijection instead of one element — and the game stops measuring first-order logic and starts measuring colour refinement, the algorithm every practical graph-isomorphism test begins with. Two subjects that grew apart are one game with the moves relabelled.

The whole library · What the figures prove