Proof.

Figure 1

Defining an injection from a representation.

Suppose first that ${\mathcal B}_{S, T}$ is representable, and that $\theta $ is a representation. Since ${\mathcal B}_{S, T}$ is finite, we know that $\theta $ is a complete representation. As ${\sf w}$ is an atom, and hence non-zero, there must be points $x, y$ in the base of the representation $\theta $ such that $(x, y)\in {\sf w}^\theta $ (equivalently, $(x, y)_\theta ={\sf w}$ , recalling the notation from the end of Section 2.1). For each $i\in S$ the triple $({\sf g}_{i},{\sf y},{\sf w})$ is not forbidden, so ${\sf w} \leq ({\sf g}_{i}; {\sf y})$ , and there must be a point $z_i$ with $(x, z_{i})\in {\sf g}_{i}^\theta $ and $(z_{i}, y)\in {\sf y}^\theta $ . For distinct $i, i'\in S$ the atom $(z_i, z_{i'})_\theta $ must be red, by forbidden triples (I)–(III). Call this atom ${\sf r}(i, i')$ , for some element of ${\{ {\sf r}_{j, j'}: j, j'\in T\}}$ , and see the first part of Figure 1. For distinct $i_1, i_2, i_3\in S$ the first subscript of the red atom ${\sf r}(i_1, i_2)$ is the same as that of ${\sf r}(i_1, i_3)$ by forbidden triple (IV), see the second part of Figure 1. Fixing $i\in S$ , it follows that each $i'\in S$ corresponds to a point $\iota (i')\in T$ such that $(z_i, z_{i'})_\theta = {\sf r}_{\iota (i), \iota (i')}$ . As we have just noted, examining the second part of Figure 1 we see that $\iota (i)$ is uniquely specified. Moreover, by the second forbidden triple of (V), all indices $\iota (i')$ (for $i'\in S$ ) are distinct, hence the map $\iota :S \rightarrow T$ is an injection, and so $|S|\leq |T|$ .

Figure 2

For each $w\in N\setminus \{x,y\}$ , $\exists $ must assign the label $c_w=N'(w,z)$ .

For the converse, suppose $2\leq |S|\leq |T|$ . We aim to show that ${\mathcal B}_{S, T}$ is completely representable. As discussed above, it is sufficient to show that $\exists $ has a winning strategy in the complete representation game for ${\mathcal B}_{S, T}$ . We assume that $\forall $ never plays a trivial move, as $\exists $ can safely respond by leaving the current network unchanged. In particular we assume he never plays $(x, y, a, b)$ if $a= 1'$ or $b= 1'$ .

Suppose then that in a play of this game the current atomic labelling is N, and $\forall $ has just played the move $(x,y,a,b)$ . In her response, $\exists $ adds a new node z to N to create $N' = N\cup \{z\}$ , and assigns labels to every node $w\in N\setminus \{x,y\}$ (see Figure 2). Her strategy is as follows:

1. (a) If $N(w, x)$ and a are not both green, and $N(w, y), b$ are not both green, she sets $N'(w, z)={\sf w}$ .

2. (b) If $N(w, x), a$ are both green but $N(w, y),b$ are not both yellow, or if $N(w, y), b$ are both green but $N(w, x), a$ are not both yellow, she sets $N'(w, z)={\sf b}$ .

3. (c) The remaining case is where, for some $i, i'\in S$ , we have $N(x, w)={\sf g}_{i},\;a={\sf g}_{i'},\; N(w, y)=b={\sf y}$ (or similar with $x, y$ swapped). Since we are assuming that $\forall $ makes no trivial moves, we can assume $i\neq i'$ . In this case $\exists $ can only use a red label for $N'(w,z)$ , as the other colours are precluded by the forbidden triple rules. To complete the definition of the strategy it remains to provide the two subscripts $j, j'\in T$ of the red atom she chooses for $N'(w, z)$ .

   To help us here we introduce some notation, and make a few preliminary observations. Given an atomic network N for ${\mathcal B}_{S, T}$ and nodes $x, y\in {\sf nodes}(N)$ let

   $$\begin{align*}R_N(x, y)={\{ z\in{\sf nodes}(N): N(x, z)\mbox{ is green and } N(y, z)={\sf y}\}}.\end{align*}$$
   Observe that $R_N(x, y)$ depends only on the green and yellow edge labels of N. A set of nodes of a network where every edge between distinct nodes has a red label is called a red clique, and it follows from the forbidden triple rules that $R_N(x, y)$ must be a red clique.

   By definition, part (c) of $\exists $ ’s strategy is relevant precisely when the new node z is added to non-empty $R_N(x,y)$ . The key idea is that every time a red clique of form $R_N(x,y)$ attains size two in the current network, $\exists $ will define an injection $h_{xy}:S\rightarrow T$ and this will be used to guide her choice of labels whenever a new z is added to $R_N(x,y)$ in later rounds. This strategy will be well defined because, as $\exists $ never uses green or yellow labels, the only way the new node z can be added to $R_N(x,y)$ is if a is green and b is yellow (or vice versa), in which case x and y are specified uniquely. Thus, given z, there is only one relevant $h_{xy}$ .

   Let N be the current atomic network in a play of the atomic representation game. Assume inductively: if $|R_N(x, y)|\geq 2$ then there is an injection $h_{xy}:S\rightarrow T$ such that for all $w\neq w'\in R_N(x, y), \; i, i'\in S$ , we have

   (1) $$ \begin{align} (N(x, w)={\sf g}_i \wedge N(x, w')={\sf g}_{i'}) \Rightarrow (i\neq i'\wedge N(w, w') = {\sf r}_{h_{xy}(i), h_{xy}(i')}). \end{align} $$
   Initially all red cliques $R_{N_0}(x', y')$ are empty so the induction hypothesis holds.

   There are three ways to extend the network N to $N'$ so that a new red clique of form $R_{N'}(x,y)$ is created with $|R_{N'}(x,y)|=2$ :

   1. (i) The first is if $|R_N(x,y)|=1$ , say $R_N(x, y)={\{ w\}}$ where $w\in N$ , and $\forall $ plays $(x,y,{\sf g}_{i'},{\sf y})$ for some $i'\in S$ . In this case, $R_{N'}(x, y)={\{ w, z\}}$ , with $N(x, w)={\sf g}_{i}$ for some $i\neq i'\in S$ . Here $\exists $ defines $h_{xy}$ to be any injection $h_{xy}:S\to T$ . Such an injection must exist as we are assuming $|S|\leq |T|$ . Then she sets $N'(w, z)={\sf r}_{h_{xy}(i), h_{xy}(i')}$ , in accordance with (1).

   2. (ii) The second way such a red clique of size two can be created is where $w\in N$ , z is the new node, and $\forall $ ’s move is $(x,y,{\sf y},{\sf y})$ , with $N(w,x)= {\sf g}_i$ and $N(w,y) = {\sf g}_{i'}$ for some $i, i'\in S$ (see Figure 3). Since N is an atomic network and $\forall $ ’s move is legal, $N(x, y)$ must be red and $i\neq i'$ (using the first forbidden triple of (V)). This creates the red clique $R_{N'}(w,z)={\{ x, y\}}$ ( ${\{ x, y\}}$ was previously a red clique, but not of the form $R_N(x', y')$ ). Note that x and y can be the only members of $R_{N'}(w,z)$ as $\exists $ never uses yellow labels, so no other network node can have a yellow edge to z. Here the label $N(x,y)$ was defined in N previously, and must be ${\sf r}_{j, j'}$ for some $j\neq j'\in T$ , as otherwise $\forall $ ’s move would be illegal. In this case $\exists $ defines $h_{wz}$ to be any injection $S\rightarrow T$ with $h_{wz}(i) = j$ and $h_{wz}(i') = j'$ .

      Figure 3

      Creating a red clique of size 2.

      

   3. (iii) The third way is similar to the second, except $\forall $ plays $(x,y,{\sf g}_i,{\sf g}_{i'})$ , and $N(w,x)=N(w,y)={\sf y}$ . This is similar to the previous case, and for $\forall $ ’s move to be legal we must have $N(x,y) = {\sf r}_{j, j'}$ for some $j\neq j'\in T$ . Again $\exists $ defines $h_{wz}$ to be any injection with $h_{wz}(i) = j$ and $h_{wz}(i') = j'$ .

   The only case where $\exists $ chooses any red labels is when $\forall $ ’s move is $(x, y, {\sf g}_i, {\sf y})$ or $(x, y, {\sf y}, {\sf g}_i)$ , for some $i\in S$ . So the only way a red clique of form $R_{N'}(x,y)$ with size $k>2$ can occur is where $|R_N(x, y)|=k-1$ and $\forall $ ’s move for the round is $(x, y, {\sf g}_i, {\sf y})$ for some $i\in S$ . Since we are assuming that no trivial moves are played, there is no $w\in R_N(x, y)$ with $N(x, w)={\sf g}_i$ . In this case $\exists $ adds a single new node z to the network and includes it in $R_{N'}(x, y)$ . Then, according the $\exists $ ’s strategy, edges $(z, w)$ have red labels if $w\in R_N(x, y)$ but either white or black labels if $w\in N\setminus R_N(x, y)$ . Note that $z\in R_{N'}(x', y')$ if and only if $x=x'$ and $y=y'$ . Since $k-1\geq 2$ we know inductively that there is an injection $h_{xy}:S\rightarrow T$ , satisfying (1). For $w\in R_N(x, y)$ where $N(x, w)={\sf g}_{i'}$ say, she lets $N(w, z) = {\sf r}_{h_{xy}(i'), h_{xy}(i)}$ (see Figure 4). This maintains (1) and completes the definition of $\exists $ ’s strategy.

   Figure 4

   The label $N'(w,z)$ in case (c).

   

We must show that this strategy is a good one by proving that $N'$ is an atomic network, i.e., that the labelling is coherent. We must check that the labeling of each triangle $(w, w^*, z)$ for $w\neq w^*\in N$ is not forbidden. If ${\{ w, w^*\}}={\{ x, y\}}$ then the triangle is consistent (else $\forall $ ’s move would be illegal), so without loss of generality we assume that $w\notin \{x,y\}$ , and so the label $N'(w,z)$ was just assigned by $\exists $ in this round. Hence $N'(w, z)$ must be either white, black or red, since she only chooses these colours. If $N'(w, z)={\sf w}$ , then the only possibility that the triangle $(w, w^*, z)$ could be forbidden comes from (II), but this requires that $N'(w^*,z)$ and $N'(w,w^*)$ be green, and thus that $w^*\in \{x,y\}$ . But then the conditions of (a) would not have been met, so $N'(w,z)$ could not be ${\sf w}$ after all. Similarly, if $N'(w, z)={\sf b}$ then the possibility of violating (III) is ruled out by case (b) conditions.

In the remaining case, $N'(w, z)$ is red, and the only forbidden triples involving red atoms are (IV) and (V). Since $w\notin \{x,y\}$ by assumption, the label $N'(w, z)$ must have been assigned according to part (c) of $\exists $ ’s strategy, so we assume that $N(x, w)={\sf g}_i,\;a={\sf g}_{i'}$ , and $N(y,w)=b ={\sf y}$ (the case where $x, y$ are swapped is symmetric). A triangle $(w, w^*, z)$ could only violate forbidden triple (IV) if all three edges were red. For this to happen we must have $N'(x,w^*) = {\sf g}_{i^*}$ for some $i^*\in S$ , and $N'(y,w^*) = {\sf y}$ , so ${\{ w, w^*\}}\subseteq R_N(x, y)$ . By our induction hypothesis, there is an injection $h_{xy}:S\rightarrow T$ satisfying (1) in N. According to part (c) of her strategy, $\exists $ set $N'(w, z)={\sf r}_{h_{xy}(i), h_{xy}(i')}$ and $N'(w^*, z)={\sf r}_{h_{xy}(i^*), h_{xy}(i')}$ . It follows that $(w, w^*, z)$ does not violate (IV) (see Figure 5).

Figure 5

The red triangle involving $w,w^*$ and z.

For rule(V), the only possible green–green–red triangle incident with z and w is $(x, w, z)$ and the edge labels $({\sf g}_i, {\sf g}_{i'},{\sf r}_{h_{xy}(i), h_{xy}(i')})$ do not violate (V), since h is injective. Hence the labelling is coherent, and $N'$ is an atomic network.⊣

Proof. Given finite sets $S, T$ where $2\leq |S|<|T|$ consider the algebras ${\mathcal B}_{S, S}$ and ${\mathcal B}_{T, S}$ . By Theorem 3.2, the former is completely representable while the latter is not, and, since they are finite, representability is the same as complete representability. Thus the atom structure of ${\mathcal B}_{S, S}$ is in ${\mathcal K}$ and that of ${\mathcal B}_{T, S}$ is not.

However, consider the well-known Ehrenfeucht–Fraïssé game for testing elementary equivalence played over a pair of relational structures using c pebbles. A full description of this game can be found in e.g., [Reference Immerman15, Chapter 6], but a brief summary is that, in each round, the player $\forall $ associates a pebble with an element of his choice from one of the structures (again of his choice), and then the player $\exists $ associates the same pebble with an element of her choice from the other structure. This association via pebbles induces a mapping between the two structures, and $\forall $ wins if at any point it fails to be a well-defined isomorphism. The key result is that $\exists $ has a strategy guaranteeing her survival in this game for at least n rounds if and only if the two structures are equivalent with respect to all formulas of quantifier depth at most n using at most c free variables (see e.g., [Reference Immerman15, Theorem 6.10]).

In our case, $\exists $ has a winning strategy in the $|S|$ -pebble, $\omega $ -round Ehrenfeucht Fraïssé-game over the atom structures of ${\mathcal B}_{S, S}$ and ${\mathcal B}_{T, S}$ , which we describe now. Whenever $\forall $ picks a non-green atom, $\exists $ picks the corresponding non-green atom in the other atom structure. If $\forall $ places a pebble where another pebble is already placed, then $\exists $ covers the corresponding pebble in the other structure. If $\forall $ picks a green atom not already in play, then $\exists $ picks any green atom in the other atom structure not currently selected. There are always enough green atoms for this, because the game only uses $|S|$ pebbles. This strategy is a winning one because a triple $({\sf g}_i, {\sf g}_{i'},{\sf r}_{j,j'})$ is forbidden iff $i=i'$ or $j=j'$ , in either atom structure. It follows that the two atom structures agree on all $|S|$ -variable formulas.⊣

Proof. This is half the well known result for relational signatures used in the proof of Corollary 3.3 (see e.g., [Reference Immerman15, Theorem 6.10]). Having functions in the signature blocks the proof of the opposite implication. We induct on n. For the base case, if $\exists $ wins $\Gamma _0({\mathcal A}, {\mathcal B}, p)$ then p induces an isomorphism from ${\mathcal A}_{\bar a}$ to ${\mathcal B}_{\bar b}$ , hence $({\mathcal A}, \bar {a})\equiv _0({\mathcal B}, \bar {b})$ .

For the inductive step, suppose $\exists $ has a winning strategy in $\Gamma _{n+1}({\mathcal A}, {\mathcal B}, p)$ , and let $\phi $ be a formula of quantifier depth $n+1$ . Note that, for all formulas $\phi _1$ and $\phi _2$ , if ${\mathcal A}$ and ${\mathcal B}$ disagree about $\phi _1\wedge \phi _2$ they must also disagree about either $\phi _1$ or $\phi _2$ , and if they disagree about $\neg \phi _1$ they must also disagree about $\phi _1$ . So we can assume without loss of generality that $\phi =\exists x_k \psi $ , where $\psi $ is a formula of quantifier depth n. If ${\mathcal A}, \bar { a}\models \exists x_k\psi $ then there is $a_k\in {\mathcal A}$ such that ${\mathcal A}, \bar { a},a_k\models \psi $ . If $\forall $ plays $a_k$ in the game, then since $\exists $ has a winning strategy there is $b_k\in {\mathcal B}$ where $\exists $ has a winning strategy in $\Gamma _n({\mathcal A}, {\mathcal B}, p')$ , where $p'$ is p with $(a_k, b_k)$ appended. Inductively, ${\mathcal B},\bar b, b_k \models \psi $ , hence ${\mathcal B}, \bar {b}\models \exists x_k \psi $ . Since the argument is symmetric, it follows that $({\mathcal A}, \bar a)$ agrees with $({\mathcal B},\bar b)$ on all formulas $\exists x_k\psi $ where $\psi $ has quantifier depth at most n, hence they agree on all formulas of quantifier depth at most $n+1$ . By induction, the lemma holds for all $n<\omega $ .⊣

Proof. If $|T|,|T'|\geq 2$ then $\exists $ wins ${\textbf {G}}_{0}(T, T')$ as $\pi _T^{p_0} = T$ and $\pi _{T'}^{p_0}=T'$ , so assume $n>0$ . Suppose $\exists $ plays according to the following principle: If the position is $p_{r}$ , for every palette $\pi \subseteq {\{ i:i<n\}}$ , she ensures that

(†r) $$\begin{align} (|\pi^{p_{r}}_{T}|< 2^{n+1-r}\vee |\pi^{p_{r}}_{T'}|< 2^{n+1-r}) \rightarrow |\pi^{p_r}_{T}|=|\pi^{p_r}_{T'}|. \end{align}$$

If $\exists $ can maintain $(\dagger _r)$ while $r\leq n$ she will survive all rounds. At the end of the final round n, $(\dagger _{n})$ ensures that (2) holds, but note that if the game were to continue for another round then she might lose, because $(\dagger _{n+1})$ does not insure her against violating (2).

We now prove by induction that $\exists $ can indeed always play so as to ensure (†_r ) holds up to and including $r=n$ . The base case is $r=0$ . The position here is $p_0$ , and by definition $\pi ^{p_0}_T= T$ and $\pi ^{p_0}_{T'}=T'$ for all palettes $\pi $ , and so $(\dagger _{0})$ holds as by assumption $|T|,|T'|\geq 2^{n+1}$ .

Suppose now that $0\leq r< n$ , that the position is $p_r$ , and that $(\dagger _{r})$ holds. Suppose without loss of generality that $\forall $ picks $T_r\subseteq T$ (the case where he chooses a subset of $T'$ is similar). For $\exists $ ’s response $T^{\prime }_r\subseteq T'$ , she will pick disjoint subsets $T^{\prime }_\pi \subseteq \pi ^{p_{r}}_{T'}$ (for each palette $\pi $ ) and then she will define $T^{\prime }_r=\bigcup _{\pi \subseteq {\{ i:i<n\}}} T^{\prime }_\pi $ . How she chooses each $T^{\prime }_\pi $ is explained next. Note that if $\pi $ is a palette, then $\pi ^{p_{r+1}}_T$ will either be $\pi ^{p_{r}}_T\cap T_{r}$ or $\pi ^{p_{r}}_T\setminus T_{r}$ , depending on whether or not $r\in \pi $ , and similar for $\pi ^{p_{r+1}}_{T'}$ . So maintaining $(\dagger _{r+1})$ comes down to ensuring these sets have the right cardinalities.

• • If $|\pi ^{p_{r}}_T\cap T_{r}|< 2^{(n+1)-(r+1)} = 2^{n-r}$ and $|\pi ^{p_{r}}_T\setminus T_{r}|< 2^{n-r}$ , then $|\pi ^{p_{r}}_T|< 2^{n+1-r}$ , so by the inductive assumption $(\dagger _{r})$ we have $|\pi ^{p_{r}}_T|=|\pi ^{p_{r}}_{T'}|$ . Here she lets $T^{\prime }_\pi $ be any subset of $\pi ^{p_{r}}_{T'}$ of size $|\pi ^{p_{r}}_T\cap T_{r}|$ . It follows that $\pi ^{p_{r}}_{T'}\setminus T^{\prime }_\pi $ has the same size as $\pi ^{p_{r}}_T\setminus T_r$ .

• • If $|\pi ^{p_{r}}_T\cap T_r|< 2^{n-r}$ but $|\pi ^{p_{r}}_T\setminus T_r|\geq 2^{n-r}$ then she lets $T^{\prime }_\pi $ be any subset of $\pi ^{p_{r}}_{T'}$ of the same size as $\pi ^{p_{r}}_T\cap T_r$ . It follows that $\pi ^{p_{r}}_{T'}\setminus T^{\prime }_\pi $ will have size at least $2^{n-r}$ , because otherwise $|\pi ^{p_r}_{T'}|<2^{n+1-r}$ , and so by $(\dagger _{r})$ we would have $|\pi ^{p_r}_{T}| = |\pi ^{p_r}_{T'}|$ , and thus $2^{n-r}\leq |\pi ^{p_{r}}_T\setminus T_r| = |\pi ^{p_{r}}_{T'}\setminus T^{\prime }_\pi |< 2^{n-r}$ , which would be a contradiction.

• • Similarly, if $|\pi ^{p_{r}}_T\setminus T_r|< 2^{n-r}$ but $|\pi ^{p_{r}}_T\cap T_r|\geq 2^{n-r}$ she chooses $T^{\prime }_\pi $ so that $\pi ^{p_{r}}_{T'}\setminus T^{\prime }_\pi $ has the same size as $\pi ^{p_{r}}_T\setminus T_r$ .

• • Finally, if both $\pi ^{p_{r}}_T\cap T_r$ and $\pi ^{p_{r}}_T\setminus T_r$ have size at least $2^{n-r}$ then $|\pi ^{p_{r}}_T|\geq 2^{n+1-r}$ , so inductively $|\pi ^{p_{r}}_{T'}|\geq 2^{n+1-r}$ . She lets $T^{\prime }_\pi \subseteq \pi ^{p_{r}}_{T'}$ be any subset of size $2^{n-r}$ , and so $|\pi ^{p_{r}}_{T'}\setminus T^{\prime }_\pi |\geq 2^{n-r}$ .

So

$$ \begin{align*} \pi^{p_{r+1}}_T&=\begin{cases} \pi^{p_{r}}_T\setminus T_r\mbox{ if }r\not\in\pi,\\ \pi^{p_{r}}\cap T_r\mbox{ if }r\in\pi, \end{cases}\\ \pi^{p_{r+1}}_{T'}&= \begin{cases} \pi^{p_{r}}_{T'}\setminus T^{\prime}_r = \pi^{p_{r}}_{T'}\setminus T^{\prime}_\pi \mbox{ if } r\not\in\pi, \\ \pi^{p_{r}}\cap T^{\prime}_r\mbox{ if }r\in\pi. \end{cases} \end{align*} $$

By the definition by cases given above, the cardinalities of these sets agree when necessary. Thus ( $\dagger _{r+1}$ ) is established for the new position $p_{r+1}$ .⊣

Proof. $\exists $ ’s strategy is to simulate a corresponding play of ${\textbf {G}}_{n}(T, T')$ in which she uses her winning strategy, and to maintain a correspondence between the plays of the games. So, if $\forall $ selects $x\in {\mathcal B}_{T, S}$ , then she selects $y\in {\mathcal B}_{T', S}$ whose non-green part is identical to that of x and whose green part is defined by her response to the $\forall $ -move $T_x$ in the play of ${\textbf {G}}_{n}(T, T')$ , and similar when he picks an element of ${\mathcal B}_{T', S}$ .

We assume that $n\geq 1$ , as the argument for the $n=0$ case is essentially the same, but simpler as all that is considered are the empty starting positions in both games. So let $p_{n}=((a_0, b_0),\ldots ,(a_{n-1},b_{n-1}))$ be the position at the end of the final round in a play of the game $\Gamma _{n}({\mathcal B}_{T, S}, {\mathcal B}_{T', S})$ in which $\exists $ uses this strategy, and let $((T_0, T^{\prime }_0),\ldots ,(T_{n-1},T^{\prime }_{n-1}))$ be the corresponding position at the end of the final round in the corresponding play of ${\textbf {G}}_{n}(T, T')$ . Note that $p_{n}$ is not a winning position for $\forall $ if and only if $p_i$ is not a winning position for him for all $i\leq n$ , so it is sufficient for us to prove that $\forall $ does not win at the end of round n.

For each $j<n$ we have $T_j = T_{a_j}\subseteq T$ , where $T_{a_j}$ is the set of elements of T indexing the green atoms below $a_j$ , and $T^{\prime }_j=T^{\prime }_{b_j}\subseteq T'$ similarly. From the assumption that $\exists $ is playing according to a winning strategy in ${\textbf {G}}_{n}(T, T')$ we have

(3) $$ \begin{align} \text{either}\ |\pi^{p_{n}}_T|=|\pi^{p_{n}}_{T'}|\ \text{or}\ |\pi^{p_{n}}_T|, |\pi^{p_{n}}_{T'}|\geq2,\ \text{for all palettes}\ \pi,\end{align} $$

and we have to prove that $p_{n}$ is not a losing position in the game $\Gamma _{n}({\mathcal B}_{T, S}, {\mathcal B}_{T', S})$ . If we define $\bar a = (a_0, \ldots , a_{n-1})$ and $\bar b = (b_0,\ldots , b_{n-1})$ , it is sufficient to show that the map $\bar a \mapsto \bar b$ induces a relation algebra isomorphism from $({\mathcal B}_{T, S})_{\bar a}$ to $({\mathcal B}_{T', S})_{\bar b}$ (recall that these are the subalgebras generated by $\bar a$ and $\bar b$ respectively).

Consider the boolean subalgebra ${\mathcal B}$ of ${\mathcal B}_{T, S}$ generated (using boolean operators) by ${\{ a_0, \ldots , a_{n-1}\}}$ and all the non-green atoms. Given a palette $\pi $ , let $\pi ^{{\mathcal B}}=\sum _{i\in \pi ^{p_{n}}_T}{\sf g}_i\in {\mathcal B}$ . If $\pi ^{p_{n}}_T=\emptyset $ then the sum is empty and $\pi ^{{\mathcal B}}=0$ , else the sum is non-empty and $\pi ^{{\mathcal B}}$ is an atom of ${\mathcal B}$ (though not usually an atom of ${\mathcal B}_{T,S}$ ). To see that non-zero $\pi ^{{\mathcal B}}$ is an atom note that it has zero intersection with every non-green atom, and its intersection with an element $a_j$ is either itself, when $j\in \pi $ , or zero otherwise. A little thought reveals that all green atoms of ${\mathcal B}$ arise from palettes in this way. Note that in the $n=0$ case, the only palette is $\pi = \emptyset $ , and $\pi ^{{\mathcal B}}=\sum _{i\in T}{\sf g}_i$ , so there is exactly one green atom in ${\mathcal B}$ .

Similarly, let ${\mathcal B}'$ be the boolean sub-algebra of ${\mathcal B}_{T', S}$ generated by the non-green atoms and ${\{ b_0,\ldots , b_{n-1}\}}$ , and let $\pi ^{{\mathcal B}'}=\sum _{i\in \pi ^{p_{n}}_{T'}}{\sf g}_i$ . Since $\pi ^{p_{n}}_T=\emptyset \iff \pi ^{p_{n}}_{T'}=\emptyset $ , for all palettes (by (3)), the map

$$\begin{align*}\phi={\{ (\pi^{{\mathcal B}}, \pi^{{\mathcal B}'}):\pi\subseteq{\{ 0, \ldots, n-1\}}\}}\setminus{\{ (0,0)\}}\end{align*}$$

is a bijection from the green atoms of ${\mathcal B}$ to those of ${\mathcal B}'$ which extends to a unique boolean isomorphism $\hat {\phi }:{\mathcal B}\rightarrow {\mathcal B}'$ fixing non-green atoms.

We will show that ${\mathcal B}$ is a relation algebra and that $\hat {\phi }$ is a relation algebra isomorphism. Note first that ${\mathcal B}$ contains the identity and is closed under conversion, since all green elements are self-converse, furthermore both identity and converse are preserved by $\hat {\phi }$ . To show that ${\mathcal B}$ is a relation algebra and to show that $\hat \phi {\;}$ is a relation algebra isomorphism, we must show, for all atoms $x, y, z\in {\mathcal B}$ that

(4) $$ \begin{align} \mbox{ either } (\times) (x;y)\cdot z=0 &\mbox{ or }(\checkmark) x;y\geq z, \mbox{ and} \end{align} $$

(5) $$ \begin{align} (x; y)\cdot z = 0 &\iff (\phi(x); \phi(y))\cdot \phi(z) =0.\end{align} $$

In (4), we indicate the two alternatives by $\times $ and $\checkmark $ .

The cases where $1'\in {\{ x, y, z\}}$ are easy, so suppose $x, y, z$ are non-identity atoms of ${\mathcal B}$ (so each has a colour). Recall that the only sets of three colours where some but not all triples of atoms of those colours are forbidden, are red–red–red and green–green–red (rules IV and V). In all other cases either all triples of atoms of those colours are forbidden and we have $\times $ (and both sides of (5) are true) or none is forbidden and we have $\checkmark $ (and both sides are false). If z is red we get $\checkmark $ or $\times $ automatically since z is an atom of ${\mathcal B}_{T, S}$ . We also have (5) as, if x and y are red, then $\hat {\phi }$ fixes them, since they are non-green. Alternatively, if x and y are green then $x = \pi _1^{{\mathcal B}}$ and $y=\pi _2^{{\mathcal B}}$ for some palettes $\pi _1$ and $\pi _2$ . In this case $(x; y)\cdot z \neq 0$ if and only if there is $i\neq i'\in T$ with ${\sf g}_i\leq x$ and ${\sf g}_{i'}\leq y$ (by rule (V)), which occurs if and only if $\pi _1^{{\mathcal B}}$ and $\pi _2^{{\mathcal B}}$ are non-empty and are either distinct or have size at least two, if and only if $\pi _1^{{\mathcal B}'}$ and $\pi _2^{{\mathcal B}'}$ are non-empty and are either distinct or have size at least two (by the assumption that $\exists $ is using a winning strategy in ${\textbf {G}}_{n}(T, T')$ ), if and only if $(\phi (x); \phi (y))\cdot \phi (z) \neq 0$ .

So, without loss of generality suppose that $x = \pi _1^{{\mathcal B}}$ and $z=\pi _2^{{\mathcal B}}$ are green and $y={\sf r}_{j',j}$ is red (for some $j, j'\in S$ ). We are interested in $(\pi _1^{{\mathcal B}}; {\sf r}_{j',j})\cdot \pi _2^{{\mathcal B}}$ . We want to show that either for every green atom ${\sf g}_i$ (of ${\mathcal B}_{T, S}$ ) below $\pi _2^{{\mathcal B}}$ there is a green atom ${\sf g}_{i'}$ below $\pi _1^{{\mathcal B}}$ such that $({\sf g}_{i'},{\sf r}_{j',j},{\sf g}_{i})$ is not forbidden (for $\checkmark $ ), or that for every green atom ${\sf g}_i$ (of ${\mathcal B}_{T, S}$ ) below $\pi _2^{{\mathcal B}}$ and for every green atom ${\sf g}_{i'}$ below $\pi _1^{{\mathcal B}}$ , the triple $({\sf g}_{i'},{\sf r}_{j',j},{\sf g}_{i})$ is forbidden (for $\times $ ).

Applying the Peircean equivalences, the triple under consideration here is equivalent to $({\sf g}_i,{\sf g}_{i'},{\sf r}_{j,j'})$ . According to rule (V), this will be forbidden if and only if either $i=i'$ , or $j=j'$ . If $j=j'$ , then $({\sf g}_i,{\sf g}_{i'},{\sf r}_{j,j})$ is always forbidden (regardless of $i, i'$ ), so we have $\times $ , and both sides of (5) are true. Alternatively, suppose $j\neq j'$ and let ${\sf g}_i\leq \pi _2^{{\mathcal B}}$ . If $x = z$ , i.e., if $\pi _1=\pi _2$ , then either $\pi _1^{\mathcal B}=\pi _2^{\mathcal B}={\sf g}_i$ for some $i\in T$ , in which case we have $\times $ as $({\sf g}_i,{\sf g}_{i},{\sf r}_{j,j'})$ is forbidden, or $\pi _1^{\mathcal B}=\pi _2^{\mathcal B}$ is above at least two distinct green atoms, in which case we have $\checkmark $ as $({\sf g}_i,{\sf g}_{i'},{\sf r}_{j,j'})$ is not forbidden when $i\neq i'$ and $j\neq j'$ . As before, both sides of (5) are true, or they are both false in each case. Similarly, if $x\neq z$ , i.e., if $\pi _1\neq \pi _2$ , then as $\pi _1^{\mathcal B}\neq 0$ and palettes are disjoint, for each green atom ${\sf g}_i$ below $\pi _2^{\mathcal B}$ , there must be ${\sf g}_{i'}\leq \pi _1^{\mathcal B}$ distinct from ${\sf g}_i$ . As $({\sf g}_i,{\sf g}_{i'},{\sf r}_{j,j'})$ is not forbidden this proves $\checkmark $ , and both sides of (5) are false.

It follows that ${\mathcal B}$ is closed under all relation algebra operations, and is a sub-relation algebra of ${\mathcal B}_{T, S}$ . Since ${\{ a_0,\ldots ,a_{n-1}\}}\subseteq {\mathcal B}$ we have the inclusion of relation algebras, $({\mathcal B}_{T, S} )_{\bar a} \subseteq {\mathcal B}\subseteq {\mathcal B}_{T, S}$ . Similarly, the boolean subalgebra ${\mathcal B}'$ of ${\mathcal B}_{T', S}$ generated by non-green atoms and ${\{ b_0,\ldots , b_{n-1}\}}$ is a sub-relation algebra of ${\mathcal B}_{T', S}$ extending $({\mathcal B}_{T', S})_{\bar b}$ . By (5), $\hat \phi {\;}$ is a relation algebra isomorphism from ${\mathcal B}$ onto ${\mathcal B}'$ .

Moreover, for all $i<n$ we have $\hat {\phi }(a_i) = b_i$ , as $\exists $ ’s strategy in $\Gamma _{n}({\mathcal B}_{T, S}, {\mathcal B}_{T', S})$ ensures this is true. It follows that the restriction of $\hat {\phi }$ to $({\mathcal B}_{T, S})_{\bar a}$ , which, as we have just proved, is an isomorphism onto $({\mathcal B}_{T', S})_{\bar b}$ , is generated by ${\{ (a_i, b_i):i<n\}}$ . This proves the result.⊣

Proof. By Lemma 4.3 $\exists $ has a winning strategy in ${\textbf {G}}_{n}(T, T')$ . So, by Proposition 4.4 she has a winning strategy in $\Gamma _{n}({\mathcal B}_{T, S}, {\mathcal B}_{T', S})$ . It follows by Lemma 4.2 that ${\mathcal B}_{T, S}\equiv _{n}{\mathcal B}_{T',S}$ .⊣

Proof. Let $T, S$ be sets where $|S|=2^{n+1},\; |T|=2^{n+1}+1$ . Then ${\mathcal B}_{S, S}\in RRA$ but ${\mathcal B}_{T, S}\not \in RRA$ , by Theorem 3.2, and ${\mathcal B}_{S, S}\equiv _{n}{\mathcal B}_{T, S}$ by Corollary 4.5. It follows that RRA cannot be axiomatised by any theory consisting of sentences of quantifier depth at most n.⊣