Generator

3 rounds on chains of 4 and 5

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

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.

With nothing chosen

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.

Who wins the game, for every pair of chain lengths up to 8

Rounds needed to tell a chain from one element longer

Where a word of m letters stops being distinguishable from one of m + 1

Three regular languages, and the one no first-order sentence defines

What a sentence of depth 2 can reach

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 degree-three point gives four middle points ×1
a star splits at the first round ×1
a vertex's neighbours induce different shapes in the two graphs, so they are not isomorphic ×1
an even number of edges is a coin toss at every size, as the flip bijection says it must be ×1
and at every point of the second ×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 every one of them swaps an even number of edges ×1
and it does grow ×1
and no pair survives three pebbles without surviving two — more pebbles never help Duplicator ×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 so does the two-dimensional refinement, which separated the last pair at once ×1
and that object is a path ×1
and the group has order two ×1
and the shape is the same at every point of the first ×1
and the share rises with the size rather than wandering ×1
and the two graphs have the same number of edges ×1
and they have the same parameters ×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
both graphs are strongly regular ×1
Duplicator survives the two-pebble bijective game ×1
every point of both graphs has two neighbours ×1
exactly four of the eight sign patterns are realised ×1
exactly half of the 64 graphs on 4 points have an even number of edges ×1
large ones almost never do ×1
no odd pattern is realised, which is the whole of what the gadget enforces ×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
one-dimensional refinement gives them the same colours ×1
out of the eight subsets of its three edges ×1
six neighbours each ×1
sixteen points each ×1
small graphs usually fail the property ×1
so the count grows like a logarithm rather than like the length ×1
some pair survives two pebbles and not three, which is the point of a third variable ×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 between two and five rounds deep ×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

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

One gadget defeats every refinement

Colour refinement fails on two triangles against a hexagon; its two-dimensional version fixes that and fails on a pair of strongly regular graphs. For every k there are two graphs the k-dimensional version cannot separate, and they are built from one local piece whose only symmetry is a parity.

Logic

The boundary at three variables

Restrict a sentence to two variable names and it can still be arbitrarily long, because the names are reused. What it cannot be is deep: every satisfiable two-variable sentence has a small model, so asking whether one is satisfiable is a bounded search. Allow a third name and the question becomes undecidable.

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