Consider the following decision problem, over the equality symmetry.

Input: an orbit-finite system of linear equations over

Decide: does have a solution (not necessarily finitely-supported)?

Inspired by Eryk’s beautiful solution of this problem, we present another solution, using an amazing theorem from topological dynamics.

Example 1. The variables are pairs where . The system is

This system has a solution: for each unordered  pair  assign the value to exactly one of . In other words, the solution is a choice function from . There is no finitely supported solution.

It is clear (by a compactness argument) that a system has a solution if and only if every finite subsystem of has a solution. However, it is not clear how to verify whether this is the case.

Example 2. Consider the system This system has a constant solution, mapping every variable to . One can prove  – this is an interesting challenge – that in every solution, the values of and are the same. In other words, the system has no solution (where and are variables). However, the smallest subsystem of this system which has no solution seems to be quite large (we found one with 5 variables and 9 equations).

We posed the problem of decidability of a given system has a solution to Eryk. At 5 am the next morning, Eryk came up with a beautiful solution. His solution uses the following observations.

Lemma 1. An orbit-finite system of linear equations in the symmetry is also an orbit-finite system of linear equations in the symmetry .

This fact can be easily seen if one identifies orbit-finite sets with sets definable using quantifier-free formulas in the underlying relational structure. Then it is obvious that any set which is definable using quantifier-free formulas in is also definable in . Another proof is to observe that any single-orbit set in  splits into several, but finitely many orbits in .

Lemma 2. In the symmetry , if a system has some solution, then it has a solution which is equivariant, i.e., invariant under the action of the automorphism group .

(Note that passing to the symmetry is crucial, due to Example 1.)

Finally, testing whether there is an equivariant solution of an orbit-finite system in the symmetry is easy – simply test all (finitely many) possible equivariant valuations, and for each of them, test whether it is a solution. The running time of this algorithm is roughly where is the number of orbits of the set of variables in the symmetry .

Eryk’s proof of Lemma 2 uses a very neat Ramsey argument. We will not present his proof here. Instead, we present an alternative proof, which uses the following result due to Pestov, which itself is proved using Ramsey’s theorem, but follows easily from a beautiful theorem from this paper of Kechris, Pestov and Todorcevic.

Theorem (Pestov, 98).  Every continuous action of the automorphism group on a compact space has a fixpoint.

Recall that a continuous action of a group on a topological space is a continuous mapping , denoted , with the property that and for all and .

 inherits its topology from with the product topology. [The product topology on (where are two sets) is given by specifying as a basic open set any set of the form , where is a fixed finite partial mapping , and is the set of mappings from to extending . If is finite, then is a compact space, by Tychonoff’s theorem.]

We now show that Lemma 2 is an immediate consequence of the above result.

Proof of Lemma 2. Let denote the set of all variables of the system . Consider the set of all valuations of those variables. This set is a compact space by Tychonoff’s theorem. Moreover, the group acts on by renaming the names of the variables, i.e., for and , is the valuation which assigns to a variable the value . It is easy to check that this action is continuous, as expected.

The set of solutions of is its subset:

and it is easy to see that it is a closed subset. [This follows from the fact that a single equation defines the set of valuations satisfying , and this set is closed, as it is a finite positive boolean combination of conditions of the form , where is some variable and . Therefore is a finite positive boolean combination of complements of basic open sets, so a closed set. In turn, the set of solutions is equal to , so is an (infinite) intersection of closed sets, so a closed set.]

In effect, the set of solutions is a compact set, which is invariant under the action of , since the system itself is invariant. Therefore, acts continuously on the compact set of solutions. Hence, by the theorem above, there is a fixpoint  of this action, that is, an invariant solution!