Recursive axiomatisations from separation properties

TL;DR

This paper introduces a new logical framework for defining separation properties and demonstrates how certain classes can be finitely axiomatized within this framework, with applications to graph colorings and separation logic.

Contribution

It develops a second-order logic fragment for separation properties and proves recursive axiomatization results, linking second-order and first-order formalisms.

Findings

Separation subclasses with recursively enumerable axiomatizations can be finitely axiomatized in first-order logic.

The framework clarifies the expressive power of separation properties in logical systems.

Applications include first-order axiomatizations for classes like graph colorings and partial algebras.

Abstract

We define a fragment of monadic infinitary second-order logic corresponding to an abstract separation property. We use this to define the concept of a separation subclass. We use model theoretic techniques and games to show that separation subclasses whose axiomatisations are recursively enumerable in our second-order fragment can also be recursively axiomatised in their original first-order language. We pin down the expressive power of this formalism with respect to first-order logic, and investigate some questions relating to decidability and computational complexity. As applications of these results, by showing that certain classes can be straightforwardly defined as separation subclasses, we obtain first-order axiomatisability results for these classes. In particular we apply this technique to graph colourings and a class of partial algebras arising from separation logic.

Equations

$$\forall x\forall y\big{(}(x\leq y\wedge C(x))\rightarrow C(y)\big{)}.$$

$$\forall x\forall y\big{(}x\leq y\rightarrow(\neg C(x)\vee C(y))\big{)}.$$

$$\forall p,q\big{(}p\not\leq q\rightarrow\exists C(C(p)\wedge\neg C(q)\wedge\text{ `closure rule expressing that $C[P]$ is a prime filter'})\big{)}.$$

$$\forall\vec{y}_{M_{i}}\Big{(}\gamma(\vec{y}_{M_{i}})\rightarrow\psi(\vec{y}_{M_{i}})\Big{)},$$

$$\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x}_{N})\wedge\tau)\Big{)},$$

$$\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}\big{(}\eta(\vec{x}_{N})\wedge\bigwedge_{I}\forall\vec{y}_{M_{i}}(\gamma_{i}(\vec{y}_{M_{i}})\rightarrow\psi_{i}(\vec{y}_{M_{i}}))\big{)}\Big{)}$$

$$\tau_{0}=\forall yz\big{(}y\leq z\rightarrow(C(y)\rightarrow C(z))\big{)}.$$

$$\tau_{i}=\forall\vec{y}_{M}z\Big{(}\mathsf{m}_{M}(\vec{y}_{M},z)\rightarrow\big{(}\bigwedge_{m=1}^{M}C(y_{m})\rightarrow C(z)\big{)}\Big{)},$$

$$\tau_{i}=\forall\vec{y}_{M}z\Big{(}\mathsf{j}_{M}(\vec{y}_{M},z)\rightarrow\big{(}C(z)\rightarrow\bigvee_{m=1}^{M}C(y_{m}))\big{)}\Big{)}.$$

$$\sigma=\forall pq\Big{(}p\not\leq q\rightarrow\exists C\big{(}C(p)\wedge\neg C(q)\wedge\bigwedge_{i\in\omega}\tau_{i}\big{)}\Big{)}.$$

$$\mathcal{B}=\{A\in \mathcal{A}:\text{we can interpret the additional symbols of }{\mathcal{L}}^{\prime }\text{ so that }A\models T\}.$$

$$\sigma=\forall\vec{x}_{N}\Big{(}\mu_{\sigma}(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}\big{(}\eta_{\sigma}(\vec{x}_{N})\wedge\tau_{\sigma}\big{)}\Big{)},$$

$${\tau }_{\sigma }=\underset{I}{\bigwedge }{\tau }_{\sigma }^i.$$

$${\tau }_{\sigma }^i=\forall {\vec{y}}_{M_i}({\gamma }_{\sigma }^i({\vec{y}}_{M_i})\to {\psi }_{\sigma }^i({\vec{y}}_{M_i})).$$

$$t_{\sigma }=\forall {\vec{x}}_N({\mu }_{\sigma }({\vec{x}}_N)\to {\hat{\eta }}_{\sigma }({\vec{x}}_N)),$$

$$t_{\sigma}^{i}=\forall\vec{x}_{N}\Big{(}\mu_{\sigma}(\vec{x}_{N})\rightarrow\forall\vec{y}_{M_{i}}\big{(}\gamma_{\sigma}^{i}(\vec{y}_{M_{i}})\rightarrow\hat{\psi}_{\sigma}^{i}(\vec{y}_{M_{i}})\big{)}\Big{)},$$

$$T=\bigcup _{\sigma \in \Sigma }{T}_{\sigma }.$$

$${\mathcal{B}}^{\prime }=\{A\in \mathcal{A}:\text{we can interpret the additional symbols of }{\mathcal{L}}^{\prime }\text{ so that }A\models T\}.$$

$$C_k(a)⟺R_k({\vec{b}}_N,a),$$

$$\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}\big{(}\eta(\vec{x}_{N})\wedge\tau\big{)}\Big{)}.$$

$$R=\{({\vec{b}}_N,a):B\models \mu ({\vec{b}}_N)\wedge C_{{\vec{b}}_N}(a)\}.$$

$$A\models S_k^A(t({\vec{a}}_N))⟺t({\vec{a}}_N)\in X_k⟺t({\vec{a}}_N)\in X_k\cap B⟺B\models S_k^B(t({\vec{a}}_N)).$$

$$\sigma=\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}\big{(}\eta(\vec{x}_{N})\wedge\bigwedge_{I}\forall\vec{y}_{M_{i}}(\gamma_{i}(\vec{y}_{M_{i}})\rightarrow\psi_{i}(\vec{y}_{M_{i}}))\big{)}\Big{)},$$

$$B\models\exists\vec{C}_{K}\big{(}\eta(\vec{a}_{N})\wedge\bigwedge_{I}\forall\vec{y}_{M_{i}}(\gamma_{i}(\vec{y}_{M_{i}})\rightarrow\psi_{i}(\vec{y}_{M_{i}}))\big{)}.$$

$${\mathcal{L}}^{+}=\mathcal{L}\cup \{C_1,\dots ,C_K\},$$

$$\tau_{i}=\forall\vec{y}_{M_{i}}\Big{(}\gamma(\vec{y}_{M_{i}})\rightarrow\psi(\vec{y}_{M_{i}})\Big{)}$$

$$\sigma=\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x}_{N})\wedge\tau)\Big{)}\in\Sigma^{>0},$$

$$A,v{\models }_{\mathcal{L}}{\psi }_{{\vec{Z}}_K}(Y\cup \bigcup _{k=1}^K{Z}_k)⟺A,v{\models }_{{\mathcal{L}}^{+}}\psi (Y),$$

$$A,v\models C_k(x)⟺v(x)\in v[Z_k],$$

$${\psi }_{{\vec{Z}}_K}(Y)=\psi (Y).$$

Full text

1. Introduction

We begin with a motivating example. Precise definitions will be given in the next section. A partially ordered set (poset) is representable if it can be embedded into a powerset algebra via a map that preserves existing finite meets and joins. The class of representable posets and its infinitary variations have been studied, not always using this terminology, in [8, 29, 21, 39, 11, 13, 12, 14, 15], generalising work done in the setting of semilattices [2, 33, 9, 27], and for distributive lattices and Boolean algebras [3, 36, 31, 35, 4, 6, 7, 1, 16]. At first glance, it is far from obvious that the class of representable posets is elementary. However, it is fairly easy to show that a poset is representable if and only if it has a ‘separating’ set of ‘prime filters’. More precisely, a poset $P$ is representable if and only if whenever $p\not\leq q\in P$ there is a ‘prime filter’ of $P$ containing $p$ and not $q$. Note that there are several non-equivalent concepts of ‘prime filter of a poset’ in circulation, and we are using one in particular. A more precise definition is given in Example 2.4.

Now, given the description of the representable posets in terms of this ‘separation property’, it is possible to show that it can in fact be axiomatised in first-order logic. [11, Theorem 4.5] does this by proving closure under taking isomorphisms, ultraproducts and ultraroots and appealing to the Keisler-Shelah theorem [28, 34], and similar can be done by proving closure under taking ultraproducts and elementary substructures and appealing to [20, Theorem 2.13]. Such a non-constructive proof of existence may be regarded as being of limited practical use, however, the very fact that an axiomatisation is known to exist can be used in a neat trick to show that a certain constructively generated axiomatisation is correct. This is the main result of [15].

The method of [15], which is not novel, is to describe the ‘separation property’ of representable posets in terms of a game played between two players. The game is defined so that the number of rounds a certain player can survive in a particular game corresponds, in a sense, to how close a given poset is to being representable. First-order axioms are then written down that correspond to the player ‘having a strategy’ in a game. These axioms are shown to correctly axiomatise the class of representable posets by means of the ‘neat trick’ mentioned previously.

A similar idea appears in [24], where it is used to find an explicit axiomatisation for a certain class of partial algebras of partial functions that appears in connection with separation logic. Again we have a class which is not obviously elementary, but which can fairly easily be shown to be definable in terms of a ‘separation property’. The separation property is then used to show, non-constructively, that a first-order axiomatisation exists, and then to construct explicit axioms based on games which are, using the ‘neat trick’, shown to be an axiomatisation for the class.

The main purpose of this paper is to prove a general theorem that includes the relevant results of [24, 15] as special cases, and is also applicable in a wide variety of other situations. The strategy is to first formalise the concept of a ‘separation property’ in a way that allows the necessary results to go through, while also being intuitive enough to be useful in practice. This is done in Section 2. In particular, the basic definition of a separation subclass is made. The sense in which separation subclasses can be, for example, essentially countable, or essentially recursively enumerable, is also explained.

We formalise the concept of a separation subclass using infinitary monadic second-order logic. We show that if $\mathcal{A}$ is a class of structures and $\mathcal{B}$ is a subclass of $\mathcal{A}$ that is elementary relative to $\mathcal{A}$, then $\mathcal{B}$ can always be described as separation subclass of $\mathcal{A}$ (Proposition 2.7). More interestingly, we show that every separation subclass of an elementary class has a first-order axiomatisation relative to the superclass (Theorem 2.14). Thus the classes of separation subclasses and elementary subclasses of an elementary class coincide. However, the important difference is that descriptions as separation subclasses can often be much easier to find than first-order axiomatisations. Moreover, as we shall see, provided the superclass is elementary, we can use a description of a subclass as an essentially recursively enumerable separation subclass to automate the construction of an explicit first-order axiomatisation.

In Section 3 we describe a class of games played between two players, $\forall$ and $\exists$. The key result is that, if $\mathcal{B}$ is an essentially countable separation subclass of $\mathcal{A}$, then given $A\in\mathcal{B}$, the player $\exists$ has a strategy for never losing in every relevant game. Conversely, if $A\in\mathcal{A}$ is countable, then $\exists$ having such strategies implies that $A\in\mathcal{B}$ (Proposition 3.1).

Section 4 formalises the existence of strategies for $\exists$ in first-order logic. The main result, which is stated as Corollary 4.6, is that an essentially recursively enumerable separation subclass $\mathcal{B}$ of an elementary class $\mathcal{A}$ always has a recursive first-order axiomatisation relative to $\mathcal{A}$, which we can generate systematically by examining the relevant class of games. Moreover, we present simple sufficient conditions for the axiomatisation produced to be universal.

In Section 5 we collect together some previous results to make explicit the connections between the various kinds of separation subclasses and the various ways a class can be elementary relative to its superclass (Proposition 5.2). We also make some simple observations regarding decision problems and complexity (Propositions 5.4 and 5.6).

Finally, in Section 6 we present some applications of the general theory we have developed. First we show how the work in [24] on disjoint union partial algebras fits into the framework of separation subclasses, and how this automatically proves some of the results of that paper (Section 6.1). Following this we consider graph colourings. In particular, in Section 6.2, from the fact that the class of $N$-colourable graphs has a simple description as a separation subclass of the class of all graphs, we are able to find easy proofs of several model theoretic results relating to these structures. We present new proofs of the known results that, for all $N\geq 2$, the class of $N$-colourable graphs has a universal Horn axiomatisation, but is not finitely axiomatisable, and also that, when $N\geq 3$, the class of graphs with chromatic number $N$ is not elementary. The proofs follow directly from the general results on separation subclasses. In this sense, $N$-colourable graphs provide a good example of a class where a characterisation as a separation subclass is obvious, but where results relating to first-order axiomatisability are not so obvious.

In Sections 6.3 and 6.4 we describe the classes of graphs with $N$-clique covers, and harmonious $N$-colourings, respectively, as separation subclasses. Thus, as an immediate consequence, we can show that both classes have recursive universal axiomatisations relative to the class of all graphs. Moreover, our method proves that the class of graphs with harmonious $N$-colourings is actually finitely axiomatisable for each $N\geq 1$.

2. Separation subclasses

We adopt the convention that indexing sets are denoted by capital letters, and arbitrary indices taken from these sets use the corresponding lowercase letters. When dealing with a set $\{x_{1},\ldots,x_{N}\}$, we will use $x_{n}$ to denote an arbitrary element from this set. For variable symbols, we adopt the convention that e.g. $\vec{x}_{N}$ denotes the set $\{x_{1},\ldots,x_{N}\}$. Given a first-order formula $\phi$ and a set of variable symbols $\vec{x}_{N}$, it is common to write something like $\phi(\vec{x}_{N})$ to denote that the free variables of $\phi$ are precisely $\vec{x}_{N}$. In this paper we use a relaxed version of this convention. Here we will write e.g. $\phi(\vec{x}_{N})$ to denote that the free variables of $\phi$ are from among $\vec{x}_{N}$, but are not necessarily all of them. We will write things like $\forall\vec{x}_{N}\phi(\vec{x}_{N})$ to stand for $\forall x_{1}\ldots x_{N}\phi(\vec{x}_{N})$. Given a set of variables $X$ we may also write e.g. $\phi(X)$ to denote that the free variables of $\phi$ are from $X$.

We will also use the $\vec{\phantom{x}}$ notation in a different but closely related way as follows. If e.g. $b_{1},\ldots,b_{N}$ are not necessarily distinct elements of some $\mathscr{L}$-structure $\mathcal{B}$, we will write $\phi(\vec{b}_{N})$ to mean $\phi(\vec{x}_{N})$ where each free $x_{n}$ is interpreted as $b_{n}$ for all $n\in\{1,\ldots,N\}$. We will sometimes write something like $\vec{b}_{N}\in\mathcal{B}$ to denote a sequence $b_{1},\ldots,b_{N}$ of elements of a structure $\mathcal{B}$.

Before diving further into the technicalities, we will try to build up some intuition for what is to be done. The situation to be captured is as follows. We have some kind of a structure, e.g. a poset $P$, and we want to say that given some elements of this structure collectively meeting some condition that is definable in first-order logic, e.g. $p,q\in P$ with $p\not\leq q$, there are subsets of the original structure which can be specified to either contain or not contain the elements in question. For, example given $p\not\leq q\in P$ we may want to demand that there is a prime filter of $P$ containing $p$ and not $q$. Moreover, these sets have to satisfy first-order closure conditions. For example, prime filters must be closed upwards, among other things. It is convenient to represent these sets using new monadic predicate symbols. We will ultimately want to existentially quantify over these predicate symbols, so we consider them to be second-order variables. If $C$ is the monadic predicate standing for the prime filter in our poset example, then upward closure can be expressed using the sentence

[TABLE]

The idea is that the relationship between elements, in this case picked out by the variables $x$ and $y$, puts some constraint on their containment or otherwise in the set, in this case picked out by the second-order variable $C$. It will be useful to rewrite this so that the purely first-order part, i.e. the part not involving $C$, is the antecedent of an implication, with the part involving $C$ being the consequent. In other words, to clearly reflect the fact that the first-order relationship between the elements places constraints on the placements of the variables in the sets represented by the second-order variables. These constraints on set containment can be expressed by Boolean combinations of clauses demanding that particular elements either are or are not included in a particular set. From $(\dagger)$, for example, we can obtain the equivalent formula

[TABLE]

What we call a closure rule, and define explicitly in Definition 2.1 shortly, is just a conjunction of constraints of this form for some given sets. For example, we describe the closure properties of prime filters by conjoining $(\ddagger)$ with an infinite number of other sentences of similar form (see Example 2.4 below for the details).

In Definition 2.2 we will formally introduce what we call a separation rule. The intuition here is that a separation rule expresses that if a set of elements from the structure meet some first-order definable condition, then there exist some subsets of the structure such that 1) there are constraints on the containment of the original elements in these sets, and 2) these sets satisfy a closure rule. Given a poset $P$, for example, if given a monadic predicate $C$ we use $C[P]$ to denote $\{p\in P:C(p)\}$, the idea that given $p\not\leq q\in P$ there is a prime filter containing $p$ and not $q$ can be expressed as a separation rule as follows

[TABLE]

Definition 2.1**.**

Let $\mathscr{L}$ be a first-order signature, let $1\leq K\in\omega$, and let $C_{1},\ldots,C_{K}$ be unary predicate symbols not appearing in $\mathscr{L}$. Define $\mathscr{L}^{+}_{\vec{C}_{K}}=\mathscr{L}\cup\{C_{1},\ldots,C_{K}\}$. A $\vec{C}_{K}$-closure rule is a conjunction $\bigwedge_{I}\tau_{i}$ for some $I\neq\emptyset$, where for each $i\in I$, the formula $\tau_{i}$ is an $\mathscr{L}^{+}_{\vec{C}_{K}}$-sentence of form

[TABLE]

where $\gamma$ is a first-order $\mathscr{L}$-formula with free variables taken from $\vec{y}_{M_{i}}=\{y_{1},\ldots,y_{M_{i}}\}$, and $\psi$ is a quantifier-free first-order $\mathscr{L}^{+}_{\vec{C}_{K}}$-formula whose free variables are also taken from $\{y_{1},\ldots,y_{M_{i}}\}$. Note that $I$ may be infinite.

Definition 2.2**.**

A separation rule for a first-order signature $\mathscr{L}$ is anything falling into either of the following two categories:

1. (1)

$\mathscr{L}$-sentences. 2. (2)

Monadic second-order sentences of form

[TABLE]

where $1\leq K<\omega$, where $\mu$ is an $\mathscr{L}$-formula with free variables taken from $\vec{x}_{N}=\{x_{1},\ldots,x_{N}\}$, where $\eta$ is a quantifier-free $\mathscr{L}^{+}_{\vec{C}_{K}}$-formula whose free variables are also taken from $\vec{x}_{N}$, and where $\tau$ is either a $\vec{C}_{K}$-closure rule or the tautology $\top$.

So, in the case where $\tau\neq\top$, a separation rule has form

[TABLE]

for some set $I\neq\emptyset$ (which may be infinite).

The order of a separation rule of type (1) is said to be zero, and the order of a separation rule of type (2) is the value of $K$ used in its definition.

A separation rule $\sigma$ is said to be finite if it either has order zero, or if the order is positive with \sigma=\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x}_{N})\wedge\bigwedge_{I}\tau_{i})\Big{)} and $I$ is finite. A separation rule that is not finite is said to be infinite. Similarly, $\sigma$ is countable if it is either finite or $I$ is countable. Finally, $\sigma$ is said to be recursively enumerable (r.e.) if it is either finite or there is an algorithm for listing the formulas $\tau_{i}$. In other words, while infinite separation rules cannot be be written out in full, if they are r.e. they can at least be approximated to arbitrary precision by including more of the infinite conjunction $\bigwedge_{I}\tau_{i}$.

A set $\Sigma$ of separation rules is called a separation scheme. Informally, a separation scheme is just a set of constraints on a structure that can be expressed as separation rules. A separation scheme $\Sigma$ is said to be essentially finite if $\Sigma$ is finite and each $\sigma\in\Sigma$ is also finite. Similarly, $\Sigma$ is essentially countable if it is countable and each $\sigma\in\Sigma$ is countable. A separation scheme $\Sigma$ is said to be essentially recursively enumerable if $\Sigma=\{\sigma_{n}:n\in\omega\}$, and $\sigma_{n}$ is r.e. for each $n\in\omega$.

Definition 2.3** ($\Sigma^{>0}$).**

If $\Sigma$ is a separation scheme, we use $\Sigma^{>0}$ to denote the subset of $\Sigma$ containing all the separation rules of order strictly greater than zero (i.e. all those of type (2)).

Example 2.4**.**

As mentioned previously, there are several non-equivalent ways to generalise the concept of a prime filter from lattices to posets. For us, a ‘prime filter’ of a poset $P$ is a subset $\Gamma$ of $P$ that is closed upwards, closed under finite existing meets (greatest lower bounds), and has the ‘primality’ property that if the join (least upper bound) of a finite set $S$ of elements of $P$ is defined in $P$ and is in $\Gamma$, then $\Gamma\cap S\neq\emptyset$. We will in future refer to a subset of a poset satisfying these closure properties as an $\omega$-filter, to avoid ambiguity. We want to phrase the condition that, given a poset $P$, if $p\not\leq q\in P$, then there is an $\omega$-filter of $P$ containing $p$ but not $q$ as a separation rule. We proceed as follows.

Let $\mathscr{L}=\{\leq\}$ be the signature of ordered sets. For each $M\geq 1$ let $\vec{y}_{M}=\{y_{1},\ldots,y_{M}\}$ be a set of variable symbols, and, with a new variable symbol $z$, define $\mathsf{j}_{M}(\vec{y}_{M},z)$ and $\mathsf{m}_{M}(\vec{y}_{M},z)$ to be the universal $\mathscr{L}$-formulas stating that $z$ is the least upper bound (join) and greatest lower bound (meet) of the elements of $\vec{y}_{M}$ respectively.

We define a closure rule to capture the closure properties of $\omega$-filters. To do this we introduce a unary predicate $C$ meant to represent an $\omega$-filter. First we define a clause $\tau_{0}$ meant to capture upward closure:

[TABLE]

Now we define a clause $\tau_{i}$ for each $1\leq i<\omega$ meant to capture closure under finite meets and the ‘primality’ property. We will use even values of $i$ to capture closure under meets of the various finite cardinalities, and we will use odd values to capture the ‘primality’ properties. This division is purely an accounting device, but it is convenient.

If $i=2M$ for some $M\in\omega$, then

[TABLE]

and, if $i=2M-1$ for some $M\in\omega$, then

[TABLE]

The closure rule for $\omega$-filters is then the conjunction $\tau=\bigwedge_{i\in\omega}\tau_{i}$. We can now define our separation rule $\sigma$ as follows:

[TABLE]

Then $\sigma$ is easily seen to be a r.e. separation rule, and a poset $P$ satisfies $\sigma$ if and only if whenever $p\not\leq q\in P$ there is an $\omega$-filter of $P$ containing $p$ but not $q$, as required. Note that $\sigma$ is not finite as we need $\tau_{i}$ for all $i\in\omega$.

Definition 2.5**.**

Let $\mathscr{L}$ be a first-order signature, let $\mathcal{A}$ be a class of $\mathscr{L}$-structures, and let $\mathcal{B}$ be a subclass of $\mathcal{A}$. Then $\mathcal{B}$ is a separation subclass of $\mathcal{A}$ if there is a separation scheme $\Sigma$ such that $\mathcal{B}=\{A\in\mathcal{A}:A\models\Sigma\}$. Here $\models$ is defined using the standard semantics for second-order logic. A separation subclass is said to be essentially r.e./countable/finite when it can be defined using a separation scheme with the corresponding property. If $\mathcal{A}$ is the class of all $\mathscr{L}$-structures then we say $\mathcal{B}$ is a separation class.

Example 2.6**.**

We say a poset is $P$ is representable if there is a set $X$ and an order embedding $h:P\to\wp(X)$ such that $h$ preserves finite meets and joins from $P$ whenever they exist (here $\wp(X)$ is considered as a lattice with operations $\cup$ and $\cap$). It is easy to prove that a poset $P$ is representable if and only if whenever $p\not\leq q\in P$ there is an $\omega$-filter of $P$ containing $p$ and not $q$ (see, for example, [15, Theorem 2.4]). Thus, building on Example 2.4, we see that the class of representable posets is an essentially r.e. separation subclass of the class of posets, using the separation scheme $\Sigma=\{\sigma\}$. Note that $\Sigma$ is essentially r.e. but not essentially finite, as while it contains only a single separation rule, this separation rule is infinite.

Generalising, given any $2\leq\alpha,\beta\leq\omega$ we say a poset $P$ is $(\alpha,\beta)$-representable if there is a set $X$ and an order embedding $h:P\to\wp(X)$ such that $h$ preserves meets of cardinality strictly less than $\alpha$, and joins of cardinality strictly less than $\beta$. Adapting the previous argument we can show the class of $(\alpha,\beta)$-representable posets is an essentially r.e. separation subclass of the class of all posets, and is essentially finite when $\alpha,\beta<\omega$.

As may be expected given the definitions, the machinery of separation subclasses is not weaker than the machinery of first-order logic when it comes to specifying subclasses of classes of $\mathscr{L}$-structures. We make this precise in the following proposition. More surprisingly, it turns out that is not stronger either. This is the result of Theorem 2.14.

Proposition 2.7**.**

If $\mathcal{A}$ is a class of $\mathscr{L}$-structures, and if $\mathcal{B}\subseteq\mathcal{A}$ is elementary relative to $\mathcal{A}$, then $\mathcal{B}$ is a separation subclass of $\mathcal{A}$. Moreover, if the axiomatisation of $\mathcal{B}$ relative to $\mathcal{A}$ is finite/countable/r.e., then $\mathcal{B}$ is an essentially finite/countable/r.e. separation subclass of $\mathcal{A}$.

Proof.

Since separation rules of order zero are just $\mathscr{L}$-sentences, this is an immediate consequence of Definition 2.5. ∎

It will be useful to slightly generalise the familiar notion of a pseudoelementary class.

Definition 2.8**.**

Let $\mathcal{A}$ be a class of $\mathscr{L}$-structures, and let $\mathcal{B}\subseteq\mathcal{A}$. Then $\mathcal{B}$ is pseudoelementary relative to $\mathcal{A}$ if there is an extension $\mathscr{L}^{\prime}$ of $\mathscr{L}$, and an $\mathscr{L}^{\prime}$-theory $T$ such that

[TABLE]

If $\mathcal{A}$ is the class of all $\mathscr{L}$-structures, then being pseudoelementary relative to $\mathcal{A}$ is the same as being pseudoelementary as it is usually defined. We say a pseudoelementary class $\mathcal{B}$ is essentially finite/countable/r.e. relative to $\mathcal{A}$ if $\mathscr{L}^{\prime}$ and $T$ are both finite/countable/r.e. Classes that are essentially finite as pseudoelementary classes relative to the class of all $\mathscr{L}$-structures are often referred to as being basic pseudoelementary.

Lemma 2.9**.**

If $\mathcal{B}$ is a separation subclass of $\mathcal{A}$, then $\mathcal{B}$ is pseudoelementary relative to $\mathcal{A}$. Moreover, if $\mathcal{B}$ is essentially finite/countable/r.e. as a separation subclass of $\mathcal{A}$, then $\mathcal{B}$ is essentially finite/countable/r.e. pseudoelementary relative to $\mathcal{A}$.

Proof.

Let $\mathcal{A}$ be a class of $\mathscr{L}$-structures, let $\Sigma$ be a separation scheme defining $\mathcal{B}$ relative to $\mathcal{A}$, and let $\sigma\in\Sigma$ have order $K$ for some $K>0$ (as there is nothing to do in the case where $K=0$). So

[TABLE]

where we either have $\tau_{\sigma}=\top$ or

[TABLE]

Moreover, assuming $\tau_{\sigma}\neq\top$, for each $i\in I$, the formula $\tau_{\sigma}^{i}$ is given by

[TABLE]

Expand $\mathscr{L}$ to a new signature $\mathscr{L}^{\prime}_{\sigma}$ by adding new $(n+1)$-ary predicate symbols $R_{1},\ldots,R_{K}$. Define

[TABLE]

where $\hat{\eta}_{\sigma}$ is $\eta_{\sigma}$ but with every occurrence of $C_{k}(-)$ replaced by $R_{k}(\vec{x}_{N},-)$, for all $k\in\{1,\ldots,K\}$.

Now, assuming $\tau_{\sigma}\neq\top$, let $i\in I$, and define

[TABLE]

where $\hat{\psi}_{\sigma}^{i}$ is defined by replacing occurrences of $C_{k}(-)$ in $\psi_{\sigma}^{i}$ with $R_{k}(\vec{x}_{N},-)$ for all $k\in\{1,\ldots,K\}$.

For $\sigma\in\Sigma^{>0}$, define $T_{\sigma}=\{t_{\sigma}\}\cup\{t_{\sigma}^{i}:i\in I\}$. If the order of $\sigma$ is 0 then $\sigma$ is already an $\mathscr{L}$-sentence, so we define $T_{\sigma}=\{\sigma\}$ in this case. Define

[TABLE]

Then $T$ is a theory for the expanded signature $\mathscr{L}^{\prime}=\bigcup_{\sigma\in\Sigma}\mathscr{L}^{\prime}_{\sigma}$. We assume that if $\sigma_{1}\neq\sigma_{2}$ then the extra symbols added to $\mathscr{L}^{\prime}_{\sigma_{1}}$ and $\mathscr{L}^{\prime}_{\sigma_{2}}$ are all distinct. Define

[TABLE]

Let $B\in\mathcal{B}^{\prime}$, and let $\sigma\in\Sigma^{>0}$ have order $K$. Then we can interpret the additional symbols of $\mathscr{L}^{\prime}$ in $B$ so that $B\models T_{\sigma}$. In particular, if $\vec{b}_{N}\in B$ is such that $B\models\mu_{\sigma}(\vec{b}_{N})$, then $B\models\hat{\eta}_{\sigma}(\vec{b}_{N})$, and, assuming that $\tau_{\sigma}\neq\top$ and given $i\in I$, we also have B\models\forall\vec{y}_{M_{i}}\big{(}\gamma_{\sigma}^{i}(\vec{y}_{M_{i}})\rightarrow\hat{\psi}_{\sigma}^{i}(\vec{y}_{M_{i}})\big{)}. So, if $\mathscr{L}^{\prime}_{\sigma}=\mathscr{L}\cup\{R_{1},\ldots,R_{K}\}$, then for each $k\in\{1,\ldots,K\}$, whenever $B\models\mu_{\sigma}(\vec{b}_{N})$ we can interpret $C_{k}$ by

[TABLE]

and so a routine argument reveals that $B\models\sigma$. There is nothing to do for the case where $\sigma$ has order 0, and so it follows that $\mathcal{B}^{\prime}\subseteq\mathcal{B}$.

Conversely, if $B\in\mathcal{B}$ then we can make $B$ into an $\mathscr{L}^{\prime}$-structure by interpreting the new relations as follows. If $R$ is one such new relation, then it is associated with a unary predicate symbol $C$ appearing in some separation rule

[TABLE]

Let $\vec{b}_{N}\in B$ and suppose $B\models\mu(\vec{b}_{N})$. Then there is an associated instantiation of $C$ in $B$ which we denote $C_{\vec{b}_{N}}$. Now, define the interpretation of $R$ in $B$ using

[TABLE]

Then another routine argument reveals that $B\models T$, and thus $\mathcal{B}\subseteq\mathcal{B}^{\prime}$. So $\mathcal{B}=\mathcal{B}^{\prime}$, and $\mathcal{B}$ is pseudoelementary relative to $\mathcal{A}$ as required.

If $\mathcal{B}$ is essentially finite/countable/r.e. as a separation subclass of $\mathcal{A}$, then that $\mathcal{B}$ is essentially finite/countable pseudoelementary/r.e. relative to $\mathcal{A}$ follows immediately from the construction of $\mathscr{L}^{\prime}$ and $T$. ∎

Corollary 2.10**.**

If $\mathcal{B}$ is a separation class then $\mathcal{B}$ is pseudoelementary.

Proof.

This follows immediately from Lemma 2.9 and the definition of separation classes (Definition 2.5). ∎

Converses to Lemma 2.9 and Corollary 2.10 do not hold in general. To see this, note that we shall show that separation classes are elementary (Theorem 2.14), while pseudoelementary classes may not be.

The following lemma is a mild generalisation of the well known fact that pseudoelementary classes are closed under ultraproducts.

Lemma 2.11**.**

If $\mathcal{A}$ is closed under ultraproducts and $\mathcal{B}$ is pseudoelementary relative to $\mathcal{A}$, then $\mathcal{B}$ is closed under ultraproducts.

Proof.

Suppose $T$ is an $\mathscr{L}^{\prime}$-theory making $\mathcal{B}$ pseudoelementary relative to $\mathcal{A}$. Let $I$ be an indexing set and for each $i\in I$ let $B_{i}\in\mathcal{B}$. Let $\prod_{U}B_{i}$ be an ultraproduct. For every $i$ we can define an $\mathscr{L}^{\prime}$-structure on $B_{i}$, which we denote $B^{\prime}_{i}$, such that $B^{\prime}_{i}\models T$. Then $\prod_{U}B^{\prime}_{i}\models T$, by Łoś’s theorem [32], and as $\prod_{U}B_{i}\in\mathcal{A}$ it follows that $\prod_{U}B_{i}\in\mathcal{B}$. ∎

The aim now is to show that separation subclasses of elementary classes are elementary. In view of Lemmas 2.9 and 2.11 it will be sufficient to prove they are closed under taking elementary substructures and appeal to [20, Theorem 2.13]. This is done by the following pair of technical lemmas.

Lemma 2.12**.**

Let $\mathscr{L}$ be a first-order signature, let $A$ be an $\mathscr{L}$-structure and let $B$ be an elementary substructure of $A$. Let $a_{1},\ldots,a_{N}$ be elements of $B$, and let $S_{1},\ldots,S_{K}$ be unary predicate symbols not appearing in $\mathscr{L}$. Define $\mathscr{L}^{+}=\mathscr{L}\cup\{S_{1},\ldots,S_{K}\}$. Let $\eta(\vec{z}_{N})$ be a quantifier-free first-order $\mathscr{L}^{+}$-formula with free variables from $\vec{z}_{N}$. For each $k\in\{1,\ldots,K\}$ let $X_{k}\subseteq A$, and use these sets to make $A$ into an $\mathscr{L}^{+}$-structure by interpreting $S_{k}$ as $X_{k}$ for each $k$. Similarly, make $B$ into an $\mathscr{L}^{+}$-structure by interpreting $S_{k}$ as $X_{k}\cap B$ for each $k$. Then $A\models\eta(\vec{a}_{N})\iff B\models\eta(\vec{a}_{N})$.

Proof.

We proceed by structural induction on $\eta$. Let $\vec{a}_{N}\in B$. If $\eta$ is a pure $\mathscr{L}$-formula, i.e. if it involves none of the additional predicates, then that $A\models\eta(\vec{a}_{N})$ if and only if $B\models\eta(\vec{a}_{N})$ follows immediately from the assumption that $B$ is an elementary substructure of $A$. So the non-trivial base cases are the atomic formulas of form $S_{k}(t(\vec{a}_{N}))$ where $t(\vec{x}_{N})$ is an $\mathscr{L}$-term. As $B$ is a substructure of $A$ we have $t(\vec{a}_{N})\in B$, and so

[TABLE]

The inductive step is routine because $\eta$ is quantifier-free, and so it suffices to deal with $\neg$ and $\wedge$. ∎

Lemma 2.13**.**

If $\mathcal{B}$ is a separation subclass of $\mathcal{A}$ and $\mathcal{A}$ is closed under taking elementary substructures, then $\mathcal{B}$ is also closed under taking elementary substructures.

Proof.

Let $\mathcal{B}$ be a separation subclass of $\mathcal{A}$, let $\Sigma$ be a separation scheme defining $\mathcal{B}$ relative to $\mathcal{A}$, and suppose $\mathcal{A}$ is closed under taking elementary substructures. Let $B\in\mathcal{B}$, and let $B^{\prime}$ be an elementary substructure of $B$. Then $B^{\prime}\in\mathcal{A}$, as $\mathcal{A}$ is closed under taking elementary substructures. We aim to show that $B^{\prime}\models\Sigma$, and thus that $B^{\prime}\in\mathcal{B}$. So, given arbitrary $\sigma\in\Sigma$ we must show $B^{\prime}\models\sigma$. If the order of $\sigma$ is 0 then this follows immediately from the assumption that $B^{\prime}$ is an elementary substructure of $B$ (recall Definition 2.2). So suppose

[TABLE]

for some $I\neq\emptyset$, as the case where $\tau=\top$ is similar but easier. Let $a_{1},\ldots,a_{N}\in B^{\prime}$, and suppose $B^{\prime}\models\mu(\vec{a}_{N})$. Then, as $B^{\prime}$ is an elementary substructure of $B$ we must have $B\models\mu(\vec{a}_{N})$, and thus

[TABLE]

This is equivalent to saying that we can extend $\mathscr{L}$ with new unary predicate symbols $C_{1},\ldots,C_{K}$ to a signature $\mathscr{L}^{+}$, and make $B$ into an $\mathscr{L}^{+}$-structure in such a way that $B\models\eta(\vec{a}_{N})\wedge\bigwedge_{I}\forall\vec{y}_{M_{i}}(\gamma_{i}(\vec{y}_{M_{i}})\rightarrow\psi_{i}(\vec{y}_{M_{i}}))$ when this is treated as an $\mathscr{L}^{+}$-formula in the obvious way. We treat $B^{\prime}$ as an $\mathscr{L}^{+}$ structure by interpreting the new predicates as the restrictions of their interpretations in $B$. We aim to use Lemma 2.12.

First of all, we have $B^{\prime}\models\eta(\vec{a}_{N})$ by immediate application of Lemma 2.12. Now, let $i\in I$, let $b_{1},\ldots,b_{M_{i}}\in B^{\prime}$, and suppose $B^{\prime}\models\gamma_{i}(\vec{b}_{M_{i}})$. Then, as $B^{\prime}$ is an elementary substructure of $B$, we also have $B\models\gamma_{i}(\vec{b}_{M_{i}})$, as $\gamma_{i}$ is an $\mathscr{L}$-formula, and thus also $B\models\psi_{i}(\vec{b}_{M_{i}})$, as $B\models\sigma$. So, again by Lemma 2.12, we have $B^{\prime}\models\psi_{i}(\vec{b}_{M_{i}})$. This is true for arbitrary choices of $b_{1},\ldots,b_{M_{i}}\in B^{\prime}$, so it follows that $B^{\prime}\models\forall\vec{y}_{M_{i}}(\gamma_{i}(\vec{y}_{M_{i}})\rightarrow\psi_{i}(\vec{y}_{M_{i}}))$ as required. This is true for all $i\in I$, and so $B^{\prime}\models\sigma$. This is true for all $\sigma\in\Sigma$, and so $B^{\prime}\models\Sigma$. Since $B^{\prime}\in\mathcal{A}$ and $B^{\prime}\models\Sigma$ it follows that $B^{\prime}\in\mathcal{B}$ as required. ∎

Theorem 2.14**.**

If $\mathcal{A}$ is elementary and $\mathcal{B}$ is a separation subclass of $\mathcal{A}$ then $\mathcal{B}$ is also elementary.

Proof.

$\mathcal{B}$ is closed under taking ultraproducts, by Lemmas 2.9 and 2.11, and is also closed under elementary substructures, by Lemma 2.13, so the result follows from [20, Theorem 2.13]. ∎

Theorem 2.14 is not constructive, but we will later exploit the fact that we know that separation subclasses of elementary classes can be axiomatised to produce explicit axiomatisations.

3. The separation game

We will define games played between two players, Abelard ($\forall$) and Eloise ($\exists$). The point here is that the existence of winning strategies in these games relates to a structure’s membership in separation subclasses, in a sense to be made precise in Proposition 3.1 below, and can also be captured in first-order logic, as we explain in Section 4. So the games provide a means to translate the second-order separation rules defining separation subclasses into first-order logic.

Our games are played over a fixed $\mathscr{L}$-structure in rounds numbered by the natural numbers starting with zero. In each round, $\forall$ plays first, then $\exists$ must respond. If a player has no legal move to make when required to play, then that player loses the game immediately, and the game does not continue. If one player loses, then the other player necessarily wins. We say that $\forall$ has an $r$-strategy if he can play in a way that guarantees he wins no later than round $r$. We say $\exists$ has an $r$-strategy if she can play in a way that guarantees that $\forall$ will not win till at least the $(r+1)$th round, either by not losing, or by winning herself prior to that point. We say that $\exists$ has an $\omega$-strategy if she can play in such a way that she can either win or survive indefinitely, however $\forall$ plays.

We now define the rules of our games more precisely. Let $\mathscr{L}$ be a first-order signature, and let $\mathcal{A}$ be a class of $\mathscr{L}$-structures. Let $\Sigma$ be a separation scheme for $\mathscr{L}$, and let \sigma=\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x}_{N})\wedge\tau)\Big{)}\in\Sigma^{>0} (recall that $\Sigma^{>0}$ is the subset of $\Sigma$ containing the separation rules of positive order). Let $A\in\mathcal{A}$, and for each $k\in\{1,\ldots,K\}$ let $S_{k},\bar{S}_{k}\subseteq A$. We define the $(A,\sigma)$-game with starting position $(S_{1},\ldots,S_{K},\bar{S}_{1},\ldots,\bar{S}_{K})$. The idea is that, for each $k$, $S_{k}$ will contain elements definitely specified by the monadic predicate $C_{k}$, and $\bar{S}_{k}$ will denote a set of elements that are definitely in its complement. Over the course of the game $\exists$ is forced to decide whether elements of $A$ are, or are not, contained in $S_{k}$. Note that at any given point in the game, $\bar{S}_{k}$ will generally be a strict subset of the complement of $S_{k}$, as there will usually be elements that $\exists$ has not yet been forced to make a decision about. If $\exists$ cannot make a move that does not violate the conditions to be defined below, then she loses the game. Formally, the game is played as follows:

• •

In round 0, $\forall$ chooses $a_{1},\ldots,a_{N}\in A$ such that $A\models\mu(\vec{a}_{N})$. In response, $\exists$ must decide, for each $n\in\{1,\ldots,N\}$ and $k\in\{1,\ldots,K\}$, whether $a_{n}\in S_{k}$. If yes then $a_{n}$ is added to $S_{k}$. If no then $a_{n}$ is added to $\bar{S}_{k}$. $\exists$ must choose in such a way that:

1. (1)

$A\models\eta(\vec{a}_{N})$, where $\eta$ is treated as a formula for signature

[TABLE]

and $C_{k}$ is interpreted as $S_{k}$ for all $k$ (where $S_{k}$ includes any elements newly added by $\exists$). 2. (2)

$S_{k}\cap\bar{S}_{k}=\emptyset$ for all $k$.

• •

In round $r$ for $r>0$, $\forall$ must play a move of form $(\tau_{i},\vec{b}_{M_{i}})$, where

[TABLE]

is part of the conjunction $\tau=\bigwedge_{I}\tau_{i}$, and $b_{1},\ldots,b_{M_{i}}\in A$ such that $A\models\gamma(\vec{b}_{M_{i}})$. If $\tau=\top$ then $\forall$ cannot do this, and so he loses.

$\exists$ must respond by deciding, for each $m\in\{1,\ldots,M_{i}\}$ and $k\in\{1,\ldots,K\}$, whether $b_{m}\in S_{k}$. If yes then $b_{m}$ is added to $S_{k}$, and if no then $b_{m}$ is added to $\bar{S}_{k}$. $\exists$ must choose in such a way that:

1. (1)

$A\models\psi(\vec{b}_{M_{i}})$, where $\psi$ is treated as an $\mathscr{L}^{+}$-formula, and $C_{k}$ is interpreted as $S_{k}$ for all $k$ (where $S_{k}$ includes new elements added by $\exists$). 2. (2)

$S_{k}\cap\bar{S}_{k}=\emptyset$ for all $k$.

We sometimes refer to the $(A,\sigma)$-game with starting position $S_{k}=\bar{S}_{k}=\emptyset$ for all $k\in\{1,\ldots,K\}$ as the simple $(A,\sigma)$-game. Note that we only define these games for $\sigma$ of positive order, as in the order zero case $\sigma$ is just a first-order sentence, so there is no need ‘translate’ it into first-order logic.

Proposition 3.1**.**

Let $\mathcal{A}$ be a class of $\mathscr{L}$-structures, let $\mathcal{B}$ be a separation subclass of $\mathcal{A}$ defined by the separation scheme $\Sigma$, and let $A\in\mathcal{A}$. Then:

1. (1)

If $A\in\mathcal{B}$, then $\exists$ has an $\omega$-strategy for the simple $(A,\sigma)$-game for all $\sigma\in\Sigma^{>0}$. 2. (2)

If $\mathcal{B}$ is essentially countable and $A$ is countable, then the converse is true. I.e. if $A\models\sigma$ for all $\sigma\in\Sigma\setminus\Sigma^{>0}$, and if $\exists$ has an $\omega$-strategy for the simple $(A,\sigma)$-game for all $\sigma\in\Sigma^{>0}$, then $A\in\mathcal{B}$.

Proof.

For 1), if $A\in\mathcal{B}$ then $A\models\sigma$, so, given $\vec{a}_{N}\in A$ with $A\models\mu(\vec{a}_{N})$, there are monadic predicates $C_{1},\ldots,C_{K}$ such that $A\models\eta(\vec{a}_{N})\wedge\tau$. In this case $\exists$ can guarantee to never lose by assigning an element $b\in A$ to $S_{k}$ if $A\models C_{k}(b)$, and to $\bar{S}_{k}$ otherwise, whenever she is forced to make a choice.

For 2), suppose that $A$ is countable, and that $\exists$ has an $\omega$-strategy for the simple $(A,\sigma)$-game for every $\sigma\in\Sigma^{>0}$. Let

[TABLE]

let $a_{1},\ldots,a_{N}\in A$ with $A\models\mu(\vec{a}_{N})$, and suppose $A\not\models\mu(\vec{a}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{a}_{N})\wedge\tau)$. Then it follows that $A\not\models\exists\vec{C}_{K}(\eta(\vec{a}_{N})\wedge\tau)$.

If $\tau=\top$, then $\exists$ has no response to the opening move $\vec{a}_{N}$ by $\forall$, contradicting the assumption that she has an $\omega$-strategy in the game. So we assume that $\tau=\bigwedge_{I}\tau_{i}$ for some non-empty $I$. Since $\Sigma$ is essentially countable and $A$ is countable, we can order the moves $(\tau_{i},\vec{b}_{M})$ that $\forall$ could potentially make using the natural numbers. Suppose $\forall$ plays according to the strategy whereby in round 0 he plays $\vec{a}_{N}$, and in every subsequent round he plays the lowest ranked legal move that he has not yet played.

Consider the sets $S_{k}$ for $k\in\{1,\ldots,K\}$ constructed by $\exists$ as she follows her $\omega$-strategy against $\forall$. In other words, each $S_{k}$ is the union of the corresponding sets from the individual rounds of the game. By the rules governing the opening round of play, and the assumption that $\exists$ is playing according to an $\omega$-strategy, we must have $A\models\eta(\vec{a}_{N})$, if $C_{k}$ is interpreted as $S_{k}$ for all $k$. Thus, if $A\not\models\exists\vec{C}_{K}(\eta(\vec{a}_{N})\wedge\tau)$ there must be some $i\in I$ with \tau_{i}=\forall\vec{y}_{M_{i}}\Big{(}\gamma(\vec{y}_{M_{i}})\rightarrow\psi(\vec{y}_{M_{i}})\Big{)} such that $A\not\models\tau_{i}$, where $C_{k}$ is interpreted as $S_{k}$ for all $k$.

It follows that there must be $b_{1},\ldots,b_{M_{i}}\in A$ with $A\models\gamma(\vec{b}_{M_{i}})$ and $A\not\models\psi(\vec{b}_{M_{i}})$, again interpreting $C_{k}$ as $S_{k}$ for all $k$. But this corresponds to a legal move by $\forall$, so he must have played it at some point, as his strategy implies that he eventually plays every move that becomes available after the first round. Thus we must have $A\models\psi(\vec{b}_{M_{i}})$ when $C_{k}$ is interpreted as $S_{k}$ after all, as $\exists$ is following an $\omega$-strategy. This would be a contradiction. Thus we must have $A\models\exists\vec{C}_{K}(\eta(\vec{a}_{N})\wedge\tau)$. Since this is true for every choice of $\vec{a}_{N}$ such that $A\models\mu(\vec{a}_{N})$, we have $A\models\sigma$, and since this argument holds for all $\sigma\in\Sigma^{>0}$, and we have assumed that $A\models\sigma$ for all $\sigma\in\Sigma\setminus\Sigma^{>0}$, it follows that $A\in\mathcal{B}$ as required. ∎

Note that round 0 is conceptually distinct from the subsequent rounds. We define the reduced $(A,\sigma)$-game with starting position $(S_{1},\ldots,S_{K},\bar{S}_{1},\ldots,\bar{S}_{K})$ to be the $(A,\sigma)$-game with the same starting position, but omitting round 0. For convenience we keep the same labeling for rounds as in the normal game, so the reduced game starts with round 1, not round 0. The concept of an $r$-strategy for $r\geq 1$ carries over without modification for both players.

4. Generating recursive axiomatisations

Given a separation scheme $\Sigma$, the next step is to find a set of first-order axioms equivalent to $\exists$ having an $\omega$-strategy in the simple $(A,\sigma)$-game for all $\sigma\in\Sigma^{>0}$. We must assume that $\Sigma$ is at least essentially recursively enumerable for the main result (Theorem 4.5) to hold. We also assume for convenience that for every $\sigma\in\Sigma^{>0}$ the associated $\tau$ is of form $\bigwedge_{i\in\omega}\tau_{i}$. Recall that in practice, $\tau$ may be $\top$, or a conjunction of only finitely many formulas. We could avoid this assumption by dividing several of the definitions and proofs to come into ‘finite’ and ‘infinite’ cases, but we trust instead that the necessary alterations for the finite cases will become clear once the infinite case is understood.

Writing down these axioms will involve some quite intricate notational constructions, and we will benefit greatly later from taking the time now to prove some technical results. Recall that for distinct variable symbols $x_{1},\ldots,x_{N}$ we use the notation $\vec{x}_{N}=\{x_{1},\ldots,x_{N}\}$. If $v$ is a valuation in the model theoretic sense, we will often write e.g. $v[\vec{x}_{N}]$ to stand for $\{v(x_{1}),\ldots,v(x_{N})\}$. Similarly, if $Z$ is a set of variables we will use $v[Z]$ to denote $\{v(z):z\in Z\}$.

First we want to formalise in first-order logic the statement that $\exists$ can survive a certain finite number of rounds in an $(A,\sigma)$-game from a given starting position. We will do this by recursion. More explicitly, the statement that $\exists$ has an $(r+1)$-strategy will be formed by writing a formula to the effect that, whatever move $\forall$ makes, $\exists$ can distribute the elements picked out by $\forall$ in such a way that she has an $r$-strategy in the $(A,\sigma)$-game with the starting position that results from her choice.

To make this work, the states of the predicates $C_{k}$ for $k\in\{1,\ldots,K\}$ associated with the separation rule $\sigma$ at a given point in the game will be captured using free variables introduced for this purpose and an assignment $v$ of variables to elements of $A$. We will do this with free variables grouped into sets $Z_{1},\ldots,Z_{K}$. The idea is that for $k\in\{1,\ldots,K\}$, the set $v[Z_{k}]$ captures the elements $\exists$ has assigned to $C_{k}$. Lemma 4.1 below explains how we can translate formulas involving the predicates $C_{1},\ldots,C_{K}$ into formulas where they are captured by free variables in this way.

Lemma 4.1**.**

Let $\mathscr{L}^{+}=\mathscr{L}\cup\{C_{1},\ldots,C_{K}\}$, where each $C_{k}$ is a unary predicate symbol not appearing in $\mathscr{L}$, let $Y$ be a finite set of variable symbols, and let $\psi(Y)$ be a quantifier-free $\mathscr{L}^{+}$-formula whose free variables are taken from $Y$. For each $k\in\{1,\ldots,K\}$ let $Z_{k}$ be a finite set of variable symbols. Let $\vec{Z}_{K}=(Z_{1},\ldots,Z_{K})$. Then we can define a quantifier-free $\mathscr{L}$-formula $\psi_{\vec{Z}_{K}}$ whose free variables are from the set $Y\cup\bigcup_{k=1}^{K}Z_{k}$, such that, whenever $A$ is an $\mathscr{L}$-structure and $v$ is an assignment, we have

[TABLE]

where $A$ is treated as an $\mathscr{L}^{+}$-structure by interpreting $C_{k}$ so that

[TABLE]

for all $k\in\{1,\ldots,K\}$.

Proof.

We use induction on the construction of $\psi$. If $\psi$ is an atomic formula, then either:

1. (1)

$\psi(Y)=R(t_{1}(Y),\ldots,t_{N}(Y))$, where $R$ is some $N$-ary relation symbol from $\mathscr{L}$ and $t_{n}$ is an $\mathscr{L}$-term for each $n\in\{1.\ldots,N\}$, 2. (2)

$\psi(Y)=t_{1}(Y)\approx t_{2}(Y)$ where $t_{1}$ and $t_{2}$ are $\mathscr{L}$-terms, or 3. (3)

$\psi(Y)=C_{k}(t(Y))$, where $t$ is an $\mathscr{L}$-term and $k\in\{1,\ldots,K\}$.

In cases (1) and (2), the interpretation of the additional predicates of $\mathscr{L}^{+}$ isn’t relevant, so we can define

[TABLE]

In the third case, define

[TABLE]

Then

[TABLE]

For the inductive step, consider first $\neg\psi$ such that $\psi_{\vec{Z}_{K}}$ is known to exist for $\psi$. In this case we can just use $\neg\psi_{\vec{Z}_{K}}$, as

[TABLE]

Consider next $\psi^{1}\vee\psi^{2}$, such that appropriate $\psi^{1}_{\vec{Z}_{K}}$ and $\psi^{2}_{\vec{Z}_{K}}$ exist. We use $\psi^{1}_{\vec{Z}_{K}}\vee\psi^{2}_{\vec{Z}_{K}}$, because

[TABLE]

Since $\psi$ is quantifier-free, we are done. ∎

As explained above, the state of each $C_{k}$ during the $(A,\sigma)$-game will be captured by $v[Z_{k}]$ for some set $Z_{k}$ of variable symbols and assignment $v$. During the game, $\exists$ must assign elements both to $C_{k}$ and its complement. For each $k$, we will use a set $\bar{Z}_{k}$ of variable symbols for this purpose. Explicitly, $v[\bar{Z}_{k}]$ captures the elements that have been assigned to the complement of $C_{k}$. In each round of the game, $\exists$ is presented with new elements of $A$ that she must assign to $C_{k}$ sets or their complements. These new elements will be captured using $v$ and a new set of variable symbols, e.g. as $v[Y]$.

As discussed previously, a key idea for us is to define for each $r\geq 1$ formulas to the effect of ‘given a starting position $(v[Z_{1}],\ldots,v[Z_{K}],v[\bar{Z}_{1}],\ldots,v[\bar{Z}_{K}])$ in an $(A,\sigma)$-game, whatever move $\forall$ makes involving elements $v[Y]$, $\exists$ can for each $k$ assign each element of $v[Y]$ to either $v[Z_{k}]$ or $v[\bar{Z}_{k}]$ to obtain $v[Z^{\prime}_{k}]$ and $v[\bar{Z}^{\prime}_{k}]$ in such a way that she has an $(r-1)$-strategy in the $(A,\sigma)$-game with starting position $(v[Z^{\prime}_{1}],\ldots,v[Z^{\prime}_{K}],v[\bar{Z}^{\prime}_{1}],\ldots,v[\bar{Z}^{\prime}_{K}])$’. As mentioned above, this will be done using recursion, so the formula stating that $\exists$ has an $(r-1)$-strategy in the $(A,\sigma)$-game with starting position $(v[Z^{\prime}_{1}],\ldots,v[Z^{\prime}_{K}],v[\bar{Z}^{\prime}_{1}],\ldots,v[\bar{Z}^{\prime}_{K}])$ must involve the variables of $Y$, but now cast in specified roles as members of the sets $Z^{\prime}_{1},\ldots,Z^{\prime}_{K},\bar{Z}^{\prime}_{1},\ldots,\bar{Z}^{\prime}_{K}$ (as these sets of variables are used to track the members of $C_{1},\ldots,C_{K}$).

The next definition sets up a notation for this process of adding new variables to sets. The situation to be described is that we have sets of variables $Z_{1},\ldots,Z_{K},\bar{Z}_{1},\ldots,\bar{Z}_{k}$, and another set of variables $Y$. For each $y\in Y$ and for each $1\leq k\leq K$ we want to add $y$ to either $Z_{k}$ or to $\bar{Z}_{k}$. What we do for a given $y\in Y$ and $k\in\{1,\ldots,K\}$ is controlled by a function $f:Y\times\{1,\ldots,K\}\to\{0,1\}$. Explicitly, if $f(y,k)=1$ then we add $y$ to $Z_{k}$, otherwise we add $y$ to $\bar{Z}_{k}$. The functions $\Delta_{K}$ and $\Delta_{\bar{K}}$ in Definition 4.2 below formalise this. The input is the data of the sets $Z_{1},\ldots,Z_{K},Y$ (for $\Delta_{K}$), or $Z_{1},\ldots,Z_{K},\bar{Z}_{1},\ldots,\bar{Z}_{K},Y$ (for $\Delta_{K}^{+}$), and the ‘control’ function $f$, and the output is either $Z_{1},\ldots,Z_{K}$ (for $\Delta_{K}$), or $Z_{1},\ldots,Z_{K},\bar{Z}_{1},\ldots,\bar{Z}_{K},Y$ (for $\Delta_{K}^{+}$) after the elements of $Y$ have been added as just described. We define two functions because sometimes we care about the $C_{k}$ sets and their complements, and other times just the sets themselves.

Definition 4.2** ($\Delta_{K}$, $\Delta_{\bar{K}}$, $F^{K}_{Y}$).**

Given a set $Y$ and $1\leq K<\omega$, let $f:Y\times\{1,\ldots,K\}\to\{0,1\}$. For each $k\in\{1,\ldots,K\}$ let $Z_{k}$ and $\bar{Z}_{k}$ be sets. We use the shorthand $\vec{Z}_{K}=(Z_{1},\ldots,Z_{K})$, and $\vec{\bar{Z}}_{K}=(\bar{Z}_{1},\ldots,\bar{Z}_{K})$. Define

[TABLE]

where for $k\in\{1,\ldots,K\}$ we have

[TABLE]

Similarly, define

[TABLE]

where $Z^{\prime}_{k}$ is as above for all $k\in\{1,\ldots,K\}$, and

[TABLE]

We will use $F^{K}_{Y}$ to denote the set of functions from $Y\times\{1,\ldots,K\}$ to $\{0,1\}$.

We now define $\mathscr{L}$-formulas as follows, noting the assumptions made about $\Sigma$ stated at the start of this section. We assume we are working with a countably infinite pool of variable symbols.

1. $\bullet$

For each $1\leq K<\omega$, and for each $\vec{Z}_{K}=(Z_{1},\ldots,Z_{K})$ and $\vec{\bar{Z}}_{K}=(\bar{Z}_{1},\ldots,\bar{Z}_{K})$ such that $Z_{k}$ and $\bar{Z}_{k}$ are finite sets of variables for all $k\in\{1,\ldots,K\}$, define

[TABLE]

to be a quantifier-free $\mathscr{L}$-formula with free variables exactly $\bigcup_{k=1}^{K}(Z_{k}\cup\bar{Z}_{k})$ such that

[TABLE] 2. $\bullet$

For each $1\leq K<\omega$, for each $i\in\omega$, for each $\sigma\in\Sigma^{>0}$, and for each $(\vec{Z}_{K},\vec{\bar{Z}}_{K})$, define

[TABLE] 3. $\bullet$

For each

[TABLE]

for each $i\in\omega$, for each $1\leq r<\omega$, and for each $(\vec{Z}_{K},\vec{\bar{Z}}_{K})$, recursively define

[TABLE]

where $\psi^{j}_{\Delta_{K}(\vec{Z}_{K},f)}$ is constructed from $\psi^{j}$ as in Lemma 4.1. In other words,

[TABLE]

where each $C_{k}$ is interpreted as $v[Z^{\prime}_{k}]$, and $Z^{\prime}_{k}$ is constructed from $Z_{k}$ and $\vec{y}_{M_{j}}$ according to $f$ (recall Definition 4.2). What these formulas are intended to capture is the idea that $\exists$ can respond to all moves involving $\tau_{j}$ for $j\leq i$ played by $\forall$, and moreover can do so in such a way that she will continue to be able to respond successfully for at least $r$ rounds. This will be made precise in Lemma 4.3. Note that although it is not apparent from the notation, we are assuming that every new occurrence of $\vec{y}_{M_{j}}$ in the construction of these formulas involves only fresh variable symbols. If we allow variable symbols to be repeated then it turns out we do not properly capture the concept of ‘adding elements to $Z_{k}$’, which is what the $\Delta$ operations are supposed to be for. This is explained in the proof of the following lemma.

Lemma 4.3**.**

Let $1\leq K<\omega$, let $A\in\mathcal{A}$, let $\mathcal{B}$ be a separation subclass of $\mathcal{A}$ defined by the essentially r.e. separation scheme $\Sigma$, let $1\leq K,<\omega$, and let $\sigma\in\Sigma$ be a separation rule of order $K$. Then for all finite $Z_{1},\ldots,Z_{K},\bar{Z}_{1},\ldots,\bar{Z}_{K}$, for all assignments $v$, for all $i\in I$ and for all $1\leq r<\omega$, the following are equivalent:

1. (1)

$A,v\models\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})ri}$. 2. (2)

$\exists$* has an $r$-strategy in the reduced $(A,\sigma)$-game with starting position*

[TABLE]

where $\forall$ can only play moves involving $\tau_{j}$ when $j\leq i$.

Proof.

We use induction on $r$. For the base case ($r=1$), let $i\in\omega$ and suppose first that $A,v\models\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})1i}$. Let $v^{\prime}$ be an assignment agreeing with $v$ about everything except, possibly, $\vec{y}_{M_{j}}$, and suppose $A,v^{\prime}\models\gamma^{j}(\vec{y}_{M_{j}})$ for some $j\leq i$. Then there is $f\in F^{K}_{\vec{y}_{M_{j}}}$ such that $A,v^{\prime}\models\psi^{j}_{\vec{Z}^{\prime}_{K}}\wedge\mathsf{D}_{(\vec{Z}^{\prime}_{K},\vec{\bar{Z}}^{\prime}_{K})}$ where $(Z^{\prime}_{1},\ldots,Z^{\prime}_{K})=\Delta_{K}(Z_{1},\ldots,Z_{K},f)$ and $(Z^{\prime}_{1},\ldots,Z^{\prime}_{K},\bar{Z}^{\prime}_{1},\ldots,\bar{Z}^{\prime}_{K})=\Delta_{\bar{K}}(\vec{Z}_{K},\vec{\bar{Z}}_{K},f)$. I.e. $Z^{\prime}_{k}$ is the new value of $Z_{k}$ as controlled by $f$, and similar for $\bar{Z}^{\prime}_{k}$, for each $k\in\{1,\ldots,K\}$ (recall Definition 4.2). Because the variables of $\vec{y}_{M_{j}}$ do not appear in any $Z_{k}$ (by the assumption mentioned after the definition of $\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})ri}$), we have $v[Z_{k}]=v^{\prime}[Z_{k}]$ for all $k\in\{1,\ldots,K\}$, and similar for $\bar{Z}_{k}$.

So, suppose $\forall$ chooses $\vec{a}_{M_{j}}\in A$ and plays the move $(\tau_{j},\vec{a}_{M_{j}})$. We define $v^{\prime}$ to be $v$ except that $v^{\prime}(y_{m})=a_{m}$ for all $m\in\{1,\ldots,M_{j}\}$. As discussed above, there is $f$ such that $A,v^{\prime}\models\psi^{j}_{\Delta_{K}(\vec{Z}_{K},f)}\wedge\mathsf{D}_{\Delta_{\bar{K}}(\vec{Z}_{K},\vec{\bar{Z}}_{K},f)}$. So, appealing to Lemma 4.1 applied to $\psi^{j}_{\Delta_{K}(\vec{Z}_{K},f)}$, there is a way, described by $f$, to assign each $a_{m}$ to either $v[Z_{k}]$ or $v[\bar{Z}_{k}]$ for each $k\in\{1,\ldots,K\}$ such that $A\models_{\mathscr{L}^{+}}\psi^{j}$ if we interpret each $C_{k}$ as the modified $v[Z_{k}]$. Moreover, from the definition of $\mathsf{D}$, we see that each modified $v[Z_{k}]$ is disjoint from the modified $v[\bar{Z}_{k}]$, and so $\exists$ can survive the first round of the reduced $(A,\sigma)$-game with starting position $(v[Z_{1}],\ldots,v[Z_{K}],v[\bar{Z}_{1}],\ldots,v[\bar{Z}_{K}])$, so long as $\forall$ starts with a move involving $\tau_{j}$ for some $j\leq i$. This proves that (1)$\implies$(2) for $r=1$.

For the converse, suppose (2) holds and that $A,v^{\prime}\models\gamma^{j}(\vec{y}_{M_{j}})$ for some $j\leq i$ with $v^{\prime}$ agreeing with $v$ about everything except, possibly, $\vec{y}_{M_{j}}$. Then $\exists$’s strategy tells us how to find $f\in F^{K}_{\vec{y}_{M_{j}}}$ appropriately. I.e. if $\exists$’s strategy assigns $v^{\prime}(y_{m})$ to $C_{k}$, then $f$ should assign $y_{m}$ to $Z_{k}$ (formally, $f(y_{m},k)=1$), and if not it should assign $y_{m}$ to $\bar{Z}_{k}$ (formally, $f(y_{m},k)=0$). With this $f$, if $Z^{\prime}_{k}$ and $\bar{Z}^{\prime}_{k}$ are, respectively, the modified $Z_{k}$ and $\bar{Z}_{k}$ for all $k\in\{1,\ldots,K\}$, we have $v^{\prime}[Z^{\prime}_{k}]\cap v^{\prime}[\bar{Z}^{\prime}_{k}]=\emptyset$, and $A,v^{\prime}\models_{\mathscr{L}^{+}}\psi^{j}(\vec{y}_{M_{j}})$ if we interpret $C_{k}$ as $v^{\prime}[Z^{\prime}_{k}]$ for all $k\in\{1,\ldots,K\}$. From Lemma 4.1 it follows that $A,v^{\prime}\models\psi^{j}_{\Delta_{K}(\vec{Z}_{K},f)}\wedge\mathsf{D}_{\Delta_{\bar{K}}(\vec{Z}_{K},\vec{\bar{Z}}_{K},f)}$. So (2)$\implies$(1).

For the inductive step, let $1<R<\omega$ and suppose the claim is true for all $1\leq r<R$. Then, by the inductive hypothesis, and appealing to similar reasoning as used for the base case, $A,v\models\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})Ri}$ if and only if, whatever move involving $\tau_{j}$ for $j\leq i$ $\forall$ plays, $\exists$ can respond in such a way that she has an $(R-1)$-strategy in the game whose starting position corresponds to her response. But this is the same as saying that $\exists$ has an $R$-strategy as claimed. ∎

The formulas $\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})ri}$ we have just defined let us deal with reduced $(A,\sigma)$-games, but we need more to handle the full games. With that in mind we now define formulas where round zero is included. These will include the $\alpha$ formulas as subformulas.

1. $\bullet$

Let $\sigma\in\Sigma^{>0}$, and for all $i\in\omega$, for all finite $(\vec{Z}_{K},\vec{\bar{Z}}_{K})$, and for all $0\leq r<\omega$, define

[TABLE]

Here $\eta_{\Delta_{K}(\vec{Z}_{K},f)}$ is constructed from $\eta$ as in Lemma 4.1. We assume that the variables in $\vec{x}_{N}$ do not appear in any subformula not involving $\mu$. The formula $\beta^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})ri}$ is intended to say that, whatever move $\forall$ makes in round zero of the $(A,\sigma)$-game with starting position $(\vec{Z}_{K},\vec{\bar{Z}}_{K})$, $\exists$ can respond in such a way that she survives this opening round, and can survive in the resulting reduced game for at least $r$ rounds, so long as $\forall$ only plays moves involving $\tau_{j}$ for $j\leq i$. Lemma 4.4 makes this precise.

Lemma 4.4**.**

Let $1\leq K<\omega$, let $A\in\mathcal{A}$, let $\mathcal{B}$ be a separation subclass of $\mathcal{A}$ defined by the essentially r.e. separation scheme $\Sigma$, and let $\sigma\in\Sigma$ be a separation rule of order $K$. Then for all $(\vec{Z}_{K},\vec{\bar{Z}}_{K})$, for all assignments $v$, for all $i\in I$, and for all $r\in\omega$, the following are equivalent:

[TABLE]

[TABLE]

Proof.

(1) is the statement that whenever $v^{\prime}$ is an assignment agreeing with $v$ about everything except, possibly, $\vec{x}_{N}$, if $A,v^{\prime}\models\mu(\vec{x})$ then there is a way $\exists$ can assign the variables of $\vec{x}_{N}$ to $\vec{Z}_{K},\vec{\bar{Z}}_{K}$ so that $A,v^{\prime}\models\eta_{\vec{Z}^{\prime}_{K}}$ and $A,v^{\prime}\models\alpha^{\sigma}_{(\vec{Z}^{\prime}_{K},\vec{\bar{Z}}^{\prime}_{K})ri}$ for the resulting values $Z^{\prime}_{1},\ldots,Z^{\prime}_{K},\bar{Z}^{\prime}_{1},\ldots,\bar{Z}^{\prime}_{K}$.

So, suppose $\forall$ plays $\vec{a}_{N}$ as an opening move. Define $v^{\prime}$ to be like $v$ except that $v^{\prime}(x_{n})=a_{n}$ for all $n\in\{1,...,N\}$. By the assumption that $\vec{x}_{N}$ involves only variables not appearing in subformulas not involving $\mu$, we have $v[Z_{k}]=v^{\prime}[Z_{k}]$ for all $k$. Then $A,v^{\prime}\models\mu(\vec{x}_{N})$, and by the preceding paragraph, there is a way $\exists$ can assign variables from $\vec{x}_{N}$ so that $A,v^{\prime}\models\eta_{\vec{Z}^{\prime}_{K}}$ and $A,v^{\prime}\models\alpha^{\sigma}_{(\vec{Z}^{\prime}_{K},\vec{\bar{Z}}^{\prime}_{K})ri}$. So, for her response, $\exists$ adds $a_{n}$ to $v[Z_{k}]$ if $x_{n}$ is added to $Z_{k}$, and otherwise adds it to $v[\bar{Z}_{k}]$. Since $A,v^{\prime}\models\eta_{\vec{Z}^{\prime}_{K}}$, it follows from Lemma 4.1 that $\exists$ can survive the opening round, and since $A,v^{\prime}\models\alpha^{\sigma}_{(\vec{Z}^{\prime}_{K},\vec{\bar{Z}}^{\prime}_{K})ri}$, it follows from Lemma 4.3 that she has an $r$-strategy in the resulting reduced game. Thus (1)$\implies$(2).

Conversely, if $\exists$ has an $r$-strategy in the game, if $v^{\prime}$ is an assignment agreeing with $v$ about everything except possibly $\vec{x}_{N}$ and $A,v^{\prime}\models\mu(\vec{x}_{N})$, then this strategy implies the existence of a suitable $f$. Explicitly, $f(x_{n},k)=1$ if $v^{\prime}(x_{n})$ is added to $v[Z_{k}]$, and $f(x_{n},k)=0$ otherwise. Thus (2)$\implies$(1) as required. ∎

The formulas $\beta^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})ri}$ defined above say that $\exists$ has an $r$ strategy in a constrained $(A,\sigma)$-game with a specified starting position. What we want for our main result are formulas stating that this is true for the ‘simple’ starting position. I.e. where the sets all start off empty. We also want to cover separation rules of order zero. With is in mind, we proceed as follows.

1. $\bullet$

For all $\sigma\in\Sigma$, for all $i\in\omega$ and for all $r\in\omega$, define

[TABLE]

Here $\vec{\emptyset}_{K}$ stands for $\vec{Z}_{K}$ where $Z_{k}=\emptyset$ for all $k$. So, given any $\sigma\in\Sigma^{>0}$, and given any $r,i\in\omega$, the first-order sentence $\hat{\beta}^{\sigma}_{ri}$ states that $\exists$ has an $r$-strategy in the simple $(A,\sigma)$-game in which $\forall$ can only play moves involving $\tau_{j}$ for $j\leq i$. Moreover, if $\Sigma$ is essentially r.e., the set $\{\hat{\beta}^{\sigma}_{ri}:\sigma\in\Sigma,i,r\in\omega\}$ can be made recursively enumerable.

This brings us to the following theorem, which is the main result of this section, and is a considerable generalisation of [24, Theorem 4.5] and [15, Theorem 5.6]. Nevertheless, the key ingredients of the proofs are essentially the same.

Theorem 4.5**.**

Let $\mathcal{A}$ be an elementary class of $\mathscr{L}$-structures, let $A\in\mathcal{A}$, and let $\mathcal{B}$ be a separation subclass of $\mathcal{A}$ defined by the essentially r.e. separation scheme $\Sigma$. Then

[TABLE]

Proof.

If $A\in\mathcal{B}$ then, for all \sigma=\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x})\wedge\tau)\Big{)}\in\Sigma^{>0}, we can use the predicates $C_{k}$ for $k\in\{1,\ldots,K\}$ to guide the strategy of $\exists$ in the appropriate games. By Proposition 3.1, $\exists$ has an $\omega$-strategy in every simple $(A,\sigma)$-game for $\sigma\in\Sigma^{>0}$, and thus $A\models\beta^{\sigma}_{(\vec{\emptyset}_{K},\vec{\emptyset}_{K})ri}$ for all $\sigma\in\Sigma^{>0}$ and for all $r,i\in\omega$, by Lemma 4.4. If $\sigma\in\Sigma\setminus\Sigma^{>0}$ then $\sigma=\hat{\beta}^{\sigma}_{ri}$, and so it follows immediately that $A\models\hat{\beta}^{\sigma}_{ri}$ for all $\sigma,r,i$.

Conversely, suppose first that $A$ is countable and that $A\notin\mathcal{B}$. Then, either $A\not\models\sigma$ for some $\sigma\in\Sigma\setminus\Sigma^{>0}$, or, by Proposition 3.1, there is $\sigma\in\Sigma^{>0}$ such that $\exists$ does not have an $\omega$-strategy in the simple $(A,\sigma)$-game. In the former case we immediately have $A\not\models\hat{\beta}^{\sigma}_{ri}$, just by definition of $\hat{\beta}^{\sigma}_{ri}$, so we consider the latter. It follows from König’s Tree Lemma [30] that some game tree for the simple $(A,\sigma)$-game is finite (otherwise $\exists$ would have a strategy defined using an infinite branch). There are only a finite number of $\forall$ moves in this game tree, and so, if $i\in\omega$ is the largest index of a $\tau_{i}$ used in a move by $\forall$ in this tree, we have $A\not\models\hat{\beta}^{\sigma}_{ri}$ for some $r\in\omega$, by Lemma 4.4.

Now, suppose $A$ is uncountable, and suppose also that $A\models\hat{\beta}^{\sigma}_{ri}$ for all $\sigma\in\Sigma$ and for all $r,i\in\omega$. Then, by the downward Löwenheim-Skolem Theorem, $A$ has a countable elementary substructure, $A^{\prime}$, and, as $A^{\prime}\models\hat{\beta}^{\sigma}_{ri}$ for all $\sigma,i,r$, it follows from our proof of the countable case that $A^{\prime}\in\mathcal{B}$. Moreover, by Theorem 2.14, $\mathcal{B}$ is elementary, so $A^{\prime}$ is a model of the elementary theory defining $\mathcal{B}$. But $A$ and $A^{\prime}$ are elementarily equivalent, so $A$ is also a model of this theory, and thus $A\in\mathcal{B}$ as claimed. ∎

Corollary 4.6**.**

Let $\mathcal{A}$ be an elementary class of $\mathscr{L}$-structures, let $A\in\mathcal{A}$, and let $\mathcal{B}$ be an essentially r.e. separation subclass of $\mathcal{A}$ defined by the separation scheme $\Sigma$. Then $\mathcal{B}$ has a recursive axiomatisation relative to $\mathcal{A}$.

Moreover, if for every $\sigma=\forall\vec{x}_{N}(\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x}_{N})\wedge\bigwedge_{I}\tau_{i}))\in\Sigma^{>0}$, the prenex normal form of $\mu$ contains no universal quantifiers, and, in addition, for every conjunct $\tau_{i}=\forall\vec{y}_{M_{i}}(\gamma_{i}(\vec{y}_{M_{i}})\rightarrow\psi_{i}(\vec{y}_{M_{i}}))$ of $\tau$, the prenex normal form of $\gamma_{i}$ contains no universal quantifiers, then, so long as the prenex normal form of every $\sigma\in\Sigma\setminus\Sigma^{>0}$ is universal, there is a recursive universal axiomatisation of $\mathcal{B}$ relative to $\mathcal{A}$.

Proof.

Since $\Sigma$ is essentially r.e. the set $\mathcal{T}=\{\hat{\beta}^{\sigma}_{ri}:\sigma\in\Sigma,r,i\in\omega\}$ can be assumed to be recursively enumerable. By Theorem 4.5, we know $\mathcal{T}$ axiomatises $\mathcal{B}$ relative to $\mathcal{A}$, and by Craig’s trick, any class with an r.e. axiomatisation relative to a superclass also has a recursive axiomatisation relative to that superclass (see, for example, [25, Exercise 6.3.1]).

Now, let \sigma=\forall\vec{x}_{N}\Big{(}\mu(\vec{x}_{N})\rightarrow\exists\vec{C}_{K}(\eta(\vec{x}_{N})\wedge\bigwedge_{I}\tau_{i})\Big{)}\in\Sigma^{>0}, let $\hat{\beta}^{\sigma}_{ri}\in\mathcal{T}$ be one of the generated $\mathscr{L}$-sentences axiomatising $\mathcal{B}$ relative to $\mathcal{A}$. I.e.

[TABLE]

Suppose $\hat{\beta}^{\sigma}_{ri}$ is not logically equivalent to a universal $\mathscr{L}$-sentence. Then, in particular the prenex normal form of $\hat{\beta}^{\sigma}_{ri}$ contains an existential quantifier. Note that $\mu$ is the antecedent of an implication, so if the prenex normal form of $\mu$ contains no universal quantifiers, then, as $\eta$ is quantifier-free, this implies there must be $f\in F^{K}_{\vec{x}_{N}}$ such that the prenex normal form of $\alpha^{\sigma}_{\Delta_{\bar{K}}(\vec{\emptyset}_{K},\vec{\emptyset}_{K},f)ri}$ contains an existential quantifier. This requires that $r\geq 1$, as when $r=0$ this formula is just $\mathsf{D}_{\Delta_{\bar{K}}(\vec{\emptyset}_{K},\vec{\emptyset}_{K},f)}$.

Now, by definition, for all $\vec{Z}_{k}$ and $\vec{\bar{Z}}_{K}$ we have

[TABLE]

If for each $i$ the prenex normal form of $\gamma_{i}$ contains no universal quantifiers, then, as $\psi^{i}$ is quantifier-free for all $i$, for the prenex normal form of $\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})ri}$ to contain an existential quantifier it is necessary that the prenex normal form of $\alpha^{\sigma}_{\Delta_{\bar{K}}(\vec{Z}_{K},\vec{\bar{Z}}_{K},f)(r-1)i}$ contains an existential quantifier for some $f\in F^{K}_{\vec{y}_{M_{j}}}$. But then the same argument applies to $\alpha^{\sigma}_{(\vec{Z}_{K},\vec{\bar{Z}}_{K})(r-1)i}$, and thus we conclude by induction that $\alpha^{\sigma}_{(\vec{Z}^{\prime}_{K},\vec{\bar{Z}}^{\prime}_{K})0i}$ contains an existential quantifier for some $\vec{Z}^{\prime}_{K}$ and $\vec{\bar{Z}}^{\prime}_{K}$, but this is impossible, as it is quantifier-free by definition.

This proves the claim, because it follows that provided the conditions are met, we can obtain a universal axiomatisation by putting every formula $\hat{\beta}^{\sigma}_{ri}$ into prenex normal form. ∎

The following lemma articulates an essentially trivial but useful observation.

Lemma 4.7**.**

Let $\mathcal{B}$ be a separation subclass of $\mathcal{A}$ defined using the essentially finite separation scheme $\Sigma$. Suppose there are natural numbers $r^{\prime}$ and $i^{\prime}$ such that, for all $\sigma\in\Sigma^{>0}$ and for all $A\in\mathcal{A}$, the following statement holds:

1. $\bullet$

If $\exists$ has an $r^{\prime}$-strategy in the $(A,\sigma)$-game where $\forall$ uses moves with index at most $i^{\prime}$, then she has an $\omega$-strategy in the usual $(A,\sigma)$-game.**

Then the axiomatisations produced in the proof of Corollary 4.6 are equivalent to a finite subset of themselves.

Proof.

By Lemma 4.4, given $\sigma\in\Sigma^{>0}$, $\exists$ having an $r$-strategy in the $(A,\sigma)$-game bounded by $i$ for $A\in\mathcal{A}$ is equivalent to saying that $A\models\hat{\beta}^{\sigma}_{ri}$. So if $r^{\prime}$ and $i^{\prime}$ exist as claimed we have $\hat{\beta}^{\sigma}_{r^{\prime}i^{\prime}}\models\hat{\beta}^{\sigma}_{ri}$ for all $r,i$. Thus by Theorem 4.5 we have $A\in\mathcal{B}\iff A\models\hat{\beta}^{\sigma}_{r^{\prime}i^{\prime}}$ for all $\sigma\in\Sigma$. The result follows as $\Sigma$ is finite. ∎

Example 4.8**.**

Returning to Example 2.6, by Corollary 4.6 we see that the class of representable posets has a recursive axiomatisation (as was proved in [15]). However, the universal quantifiers in the $\mathsf{j}$ and $\mathsf{m}$ formulas mean that the axiomatisation produced is not universal. Indeed, the class of representable posets has no universal axiomatisation, as it is not closed under substructures (see [15, Corollary 2.9]).

We also note the following alternative approach to constructing a recursive axiomatisation for $\mathcal{B}$ relative to $\mathcal{A}$ when $\mathcal{B}$ is an essentially r.e. separation subclass of $\mathcal{A}$ and $\mathcal{A}$ is elementary. [23, Chapter 9] provides a method for generating a recursive first-order axiomatisation for the elementary closure of any pseudoelementary class whose defining theory in the extended language is recursive. Since in the situation we are describing $\mathcal{B}$ is elementary (by Theorem 2.14), the elementary closure is just the class itself, and, since we have an axiomatisation of $\mathcal{B}$ as an essentially recursive pseudoelementary class by Lemma 2.9, this method can be applied to find a recursive axiomatisation for $\mathcal{B}$. This method also produces a universal axiomatisation when $\mathcal{B}$ is pseudouniversal, in the sense of [23, Definition 9.1].

Also of interest is the result presented as [23, Theorem 9.14], where it is attributed to Mal’cev and Tarski. According to this theorem, every pseudoelementary class that is closed under ultraroots is elementary, and, moreover, if it is also closed under substructures it is universal. If the pseudoelementary theory is r.e. then so too will be the elementary, or universal, axiomatisations. Appropriate sets of axioms are defined, but not made explicit. The reader is directed to the discussion following [23, Corollary 9.15] for some comments on this.

A notable advantage of the recursive axiomatisation generated in the proof of Theorem 4.5 is that, as it has an explicit connection to $\exists$’s ability to survive in certain combinatorial games, it can give us some insight into the question of whether an essentially r.e. separation subclass $\mathcal{B}$ of an elementary class $\mathcal{A}$ is finitely axiomatisable relative to $\mathcal{A}$. To understand how this works, let $T=\{\psi_{0},\psi_{1},\psi_{2},\ldots\}$ be the recursive axiomatisation obtained from Theorem 4.5. Then, if $\mathcal{B}$ is finitely axiomatisable relative to $\mathcal{A}$, there must be some $K\in\omega$ with $A\models\bigwedge_{k=0}^{K}\psi_{k}\implies A\models\psi_{j}$ for all $j\in\omega$, for all $A\in\mathcal{A}$. So, to prove that no such finite axiomatisation exists, it suffices to construct, for each $K\in\omega$, a structure $A_{K}\in\mathcal{A}$ such that $A_{K}\models\bigwedge_{k=0}^{K}\psi_{k}$, but $A_{K}\not\models\psi_{K+1}$.

Translating this back into the setting of games, for an essentially finite separation subclass the idea is to construct objects $A_{r}\in\mathcal{A}$ such that $\exists$ has $r$-strategies for all simple $(A,\sigma)$-games, but not an $(r+1)$-strategy for at least one such game. The non-finite case is similar, but we must consider the maximum indices of allowed $\forall$ moves, and we also have to take the possibly infinite number of separation rules of order zero into account. Of course, the substance of any such proof is to be found in the constructions themselves, but this can be a useful approach, where it applies. For example, this method is essentially the engine of the proofs of the titular result of [14], and the results of [24, section 5], though the work in these examples is phrased in terms of ultraproducts. Note that the argument as described here has an advantage over the originals as reasoning about properties of the ultraproduct is not required. We present a simple application of this technique in Section 6.2.

5. Expressive power and decision problems

To begin this section we organise our results on the expressive power of the formalism of separation subclasses vis-à-vis first-order logic.

Lemma 5.1**.**

There is a basic elementary class $\mathcal{A}$, and an essentially finite separation subclass $\mathcal{B}$ of $\mathcal{A}$, such that $\mathcal{B}$ is not finitely axiomatisable.

Proof.

We have shown that the class of $(\alpha,\beta)$-representable posets is an essentially finite separation subclass of the class of posets whenever $2\leq\alpha,\beta<\omega$ (see Example 2.6), and this class is also known to not be finitely axiomatisable for $\alpha,\beta\geq 3$ [14]. ∎

Proposition 5.2**.**

Let $\mathcal{A}$ be an elementary class and make the following definitions:

• $\mathbf{S}_{\mathcal{A}}$* is the class of separation subclasses of $\mathcal{A}$.*
• $\mathbf{RS}_{\mathcal{A}}$* is the class of essentially r.e. separation subclasses of $\mathcal{A}$.*
• $\mathbf{FS}_{\mathcal{A}}$* is the class of essentially finite separation subclasses of $\mathcal{A}$.*
• $\mathbf{E}_{\mathcal{A}}$* is the class of elementary subclasses of $\mathcal{A}$.*
• $\mathbf{RE}_{\mathcal{A}}$* is the class of subclasses of $\mathcal{A}$ with recursive axiomatisations relative to $\mathcal{A}$.*
• $\mathbf{FE}_{\mathcal{A}}$* is the class of subclasses of $\mathcal{A}$ that are finitely axiomatisable relative to $\mathcal{A}$.*

Then Figure 1 represents the class inclusions that always hold (with arrows from subclass to superclass). In cases where there is no arrow there are choices of $\mathcal{A}$ for which the inclusion does not hold.

Proof.

The horizontal arrows come straight from the definitions, and the lack of backward arrows is also straightforward. The downward arrows come from Corollary 4.6 and Theorem 2.14, and the upward arrows come from Proposition 2.7. The lack of an arrow from $\mathbf{FS}_{\mathcal{A}}$ to $\mathbf{FE}_{\mathcal{A}}$ comes from Lemma 5.1. ∎

Now we present some easy results on the decision problem for separation subclasses.

Definition 5.3** (Subclass decision problem).**

Given classes $\mathcal{A}$ and $\mathcal{B}$ with $\mathcal{B}\subseteq\mathcal{A}$, the decision problem for $\mathcal{B}$ relative to $\mathcal{A}$ is the question:

[TABLE]

Proposition 5.4**.**

Let $\mathcal{A}$ be a class of $\mathscr{L}$-structures, and let $\mathcal{B}$ be an essentially r.e. separation subclass of $\mathcal{A}$. Then the complement to the decision problem for $\mathcal{B}$ relative to $\mathcal{A}$ is semidecidable.

Proof.

If $\mathcal{A}$ is elementary then $\mathcal{B}$ has a recursive axiomatisation relative to $\mathcal{A}$, by Corollary 4.6, and the result follows immediately.

Suppose now that $\mathcal{A}$ is not elementary, and that $\mathcal{B}$ is defined by the essentially r.e. separation scheme $\Sigma$. Our algorithm is as follows. Given finite $A\in\mathcal{A}$, using dovetailing we work through the separation rules of $\Sigma$. If $\sigma$ is finite then it can be checked directly if $A\models\sigma$. If on the other hand

[TABLE]

is infinite then it cannot be checked directly if $A\models\sigma$, but, as $\Sigma$ is essentially r.e., we can assume without loss of generality that $I=\omega$, and for each $n\in\omega$ we can define

[TABLE]

Now with dovetailing we can check if $A\models\sigma_{n}$ for each $n\in\omega$ and each infinite $\sigma\in\Sigma$. If $A\not\models\sigma$ then there is $n$ with $A\not\models\sigma_{n}$, so if such a $\sigma$ exists our algorithm will eventually find it. As soon as $\sigma$ with $A\not\models\sigma$ is found the algorithm terminates, as this shows $A\notin\mathcal{B}$. ∎

Lemma 5.5**.**

If $\mathcal{A}$ is a class of $\mathscr{L}$-structures and $\mathcal{B}$ is an essentially finite separation subclass of $\mathcal{A}$, then the decision problem for $\mathcal{B}$ relative to $\mathcal{A}$ is in $\mathbf{NP}$.

Proof.

By Lemma 2.9, an essentially finite separation subclass is essentially finite pseudoelementary relative to the superclass, and being essentially finite pseudoelementary is equivalent to being finitely axiomatisable in existential second-order logic. Finally, by Fagin’s Theorem [18], the problem of checking whether a finite structure satisfies an existential second-order sentence is in $\mathbf{NP}$. ∎

Proposition 5.6**.**

Let $\mathcal{A}$ be an elementary class and make the following definitions in addition to those of Proposition 5.2:

• $\mathbf{P}_{\mathcal{A}}$* is the class of subclasses of $\mathcal{A}$ whose decision problem relative to $\mathcal{A}$ is in $\mathbf{P}$.*
• $\mathbf{NP}_{\mathcal{A}}$* is the class of subclasses of $\mathcal{A}$ whose decision problem relative to $\mathcal{A}$ is in $\mathbf{NP}$.*

Then Figure 2 represents the class inclusions that always hold, using the same system as in Figure 1, but with the addition that the existence of a full arrow in either of the places indicated by dotted arrows is equivalent to $\mathbf{P}=\mathbf{NP}$.

Proof.

The arrow from $\mathbf{FS}_{\mathcal{A}}$ to $\mathbf{NP}_{\mathcal{A}}$ comes from Lemma 5.5. To see that there is no arrow from $\mathbf{P}_{\mathcal{A}}$ to $\mathbf{FS}_{\mathcal{A}}$ let $\mathcal{A}$ be, for example, the class of all sets, and let $\mathcal{B}$ be the class of all finite sets. Then the decision problem for $\mathcal{B}$ relative to $\mathcal{A}$ is trivially in $\mathbf{P}$ (as every instance is a yes instance), but finiteness has no first-order characterisation, and thus cannot be formalised as a separation subclass (by Theorem 2.14). That there is no arrow from $\mathbf{NP}_{\mathcal{A}}$ to $\mathbf{FS}_{\mathcal{A}}$ follows immediately.

If there is an arrow from $\mathbf{FS}_{\mathcal{A}}$ to $\mathbf{P}_{\mathcal{A}}$ then, for example, deciding whether a finite poset is $(4,4)$-representable is in $\mathbf{P}$, as the $(4,4)$-representable posets are an essentially finite separation subclass of the class of posets (see Example 2.6), and thus $\mathbf{P}=\mathbf{NP}$, as this problem is $\mathbf{NP}$-complete [39]. Conversely, if $\mathbf{P}=\mathbf{NP}$ then there is an arrow from $\mathbf{NP}_{\mathcal{A}}$ to $\mathbf{P}_{\mathcal{A}}$, and thus an arrow from $\mathbf{FS}_{\mathcal{A}}$ to $\mathbf{P}_{\mathcal{A}}$. ∎

We have established that every essentially finite separation subclass of an elementary class is recursively axiomatisable relative to the superclass, and also that the converse does not hold in general (see Proposition 5.2). The following result says that the converse still doesn’t hold when we restrict to varieties and recursively axiomatisable subvarieties.

Proposition 5.7**.**

There is a finitely axiomatised variety $\mathcal{A}$, and a recursively axiomatised subvariety $\mathcal{B}$ of $\mathcal{A}$ such that $\mathcal{B}$ is not an essentially finite separation subclass of $\mathcal{A}$.

Proof.

The class $\mathbf{RRA}$ of representable relation algebras is a variety (by [37], or see [23, Theorem 3.37]), and can be recursively axiomatised by equations (see [23, Theorem 8.4]), but the decision problem for $\mathbf{RRA}$ relative to the class of relation algebras, $\mathbf{RA}$, is not decidable (by [22], or see [23, Theorem 18.13]), and thus cannot be an essentially finite separation subclass (appealing to Lemma 5.5). ∎

Finally, as in the argument used in the proof of Lemma 5.5, an essentially finite separation subclass $\mathcal{B}$ of a basic elementary class $\mathcal{A}$ can be finitely axiomatised in existential second-order logic. Of course, it follows immediately from Fagin’s Theorem and Proposition 5.6 that there are subclasses that are finitely axiomatisable in existential second-order logic relative to their superclasses that cannot be expressed as essentially finite separation subclasses.

6. Applications

In this section we use the general theory of separation subclasses to get some axiomatisation results in graph theory and theoretical computer science.

6.1. Disjoint union partial algebras

Here we deal with a class of structures introduced in [24].

Definition 6.1**.**

A partial algebra is a set equipped with a number of partial operations of fixed arities, and also possibly some constants. In order to accommodate this in first-order logic we think of partial algebras as relational structures, where each $n$-ary partial operation corresponds to an $(n+1)$-ary relation, and for each such relation $R$ we have a sentence

[TABLE]

expressing that the associated partial function is well defined.

Definition 6.2**.**

A disjoint union partial algebra (DUPA) is a partial algebra with a single ternary relation $\mathsf{d}$ (disjoint union). We will usually write $\mathsf{d}(x,y,z)$ as $x\dot{\cup}y=z$.

For more on DUPAs and their uses in computer science see [24].

Definition 6.3** (Representable DUPA).**

A DUPA is representable if it is isomorphic (as a relational structure) to a DUPA whose universe is a set of sets, and whose relation $\mathsf{d}$ is defined by

[TABLE]

The following is a minor adaptation of [24, Definition 4.1]

Definition 6.4** (Basic sets).**

If $A$ is a disjoint union partial algebra, and if $\Gamma\subseteq A$, then we say $\Gamma$ is basic if:

1. (1)

$a\dot{\cup}b\in\Gamma\implies$ either $a\in\Gamma$ or $b\in\Gamma$. 2. (2)

If either $a\in\Gamma$ or $b\in\Gamma$, and if $a\dot{\cup}b$ is defined, then $a\dot{\cup}b\in\Gamma$. 3. (3)

If both $a\in\Gamma$ and $b\in\Gamma$ then $a\dot{\cup}b$ is not defined.

The word ‘basic’ here refers to being part of the ‘base’ of a representation as an algebra of sets.

Lemma 6.5**.**

If $A$ is a DUPA, then $A$ is representable if and only if:

1. (1)

For all $a\neq b\in A$, there is a basic $\Gamma\subseteq A$ with either $a\in\Gamma$ and $b\not\in\Gamma$, or $b\in\Gamma$ and $a\not\in\Gamma$. 2. (2)

For all $a,b\in A$, if $a\dot{\cup}b$ is undefined then there is a basic $\Gamma\subseteq A$ with $\{a,b\}\subseteq\Gamma$.

Proof.

This is [24, Lemma 4.2]. ∎

Proposition 6.6**.**

The class of representable DUPAs is an essentially finite separation subclass of the class of all DUPAs.

Proof.

Let $\mathscr{L}=\{\mathsf{d}\}$ be the signature of disjoint union partial algebras, and let $\mathscr{L}^{+}=\mathscr{L}\cup\{C\}$, where $C$ is a unary predicate symbol. Define the following $\mathscr{L}^{+}$-sentences:

[TABLE]

Then $\tau=\tau_{0}\wedge\tau_{1}\wedge\tau_{2}$ states that the set defined by $C$ is basic, and, moreover, $\tau$ is a closure rule as defined in Definition 2.1. Now define

[TABLE]

and

[TABLE]

Then $\sigma_{1}$ and $\sigma_{2}$ are separation rules, as defined in Definition 2.2. Moreover, by Lemma 6.5, $\{\sigma_{1},\sigma_{2}\}$ axiomatises the class of representable DUPAs relative to the class of all DUPAs, which is what we are required to prove. ∎

Having established that the class of representable DUPAs is an essentially finite separation subclass of the class of all DUPAs (which is basic elementary), we can use general results for separation subclasses to easily prove some results that were obtained with more effort in [24]. For example:

Corollary 6.7**.**

The class of representable DUPAs is basic pseudoelementary.

Proof.

This follows from Proposition 6.6 and Lemma 2.9. ∎

Corollary 6.8**.**

The class of representable DUPAs has a recursive axiomatisation in first-order logic.

Proof.

This follows from Proposition 6.6 and Theorem 4.5. ∎

Note that the appearance of $\neg\exists$ in $\sigma_{2}$ means the recursive axiomatisation generated is not universal. Indeed, by [24, Corollary 3.3] we know that no such universal axiomatisation can exist.

Corollary 6.9**.**

The decision problem for the class of representable DUPAs is in $\mathbf{NP}$.

Proof.

This follows from Lemma 5.5. ∎

6.2. $N$-colourable graphs

Here and elsewhere we assume all graphs are undirected and simple. Given $\leq N<\omega$, a graph $G=(V,E)$ is $N$-colourable if it is possible to assign to each vertex $v\in V$ one of $N$ colours in such a way that no adjacent vertices have the same colour. Equivalently, $G$ is $N$-colourable if there is a homomorphism $h:G\to K_{N}$ where $K_{N}$ is the complete graph with $N$ vertices. Let $\mathcal{G}$ be the (elementary) class of all graphs, and, given $1\leq N<\omega$, define $\mathcal{G}_{N}$ to be the class of $N$-colourable graphs. Note that if $G$ is $N$-colourable via $h:G\to K_{N}$, and if $H$ is any other graph, then the composition of $h$ with the projection function, $h\circ\pi_{G}:G\times H\to K_{N}$, is a homomorphism. So, in particular, $\mathcal{G}_{N}$ is closed under taking direct products for all $1\leq N<\omega$.

Let $\mathscr{L}=\{E\}$ be the standard signature for graphs (so $E$ stands for the binary edge relation). Let $\mathscr{L}^{+}=\mathscr{L}\cup\{C_{1},\ldots,C_{N}\}$ (here $C_{n}$ is a monadic predicate intended to pick out the vertices coloured by the $n$th colour), and define

[TABLE]

[TABLE]

[TABLE]

and

[TABLE]

Then $\sigma$ is a separation rule, and if $\mathcal{C}_{N}$ is the separation subclass of $\mathcal{G}$ defined by $\{\sigma\}$, then $\mathcal{C}_{N}$ is exactly the class of all $N$-colourable graphs. Thus we see that $\mathcal{C}_{N}$ has the various pleasant properties associated with essentially finite separation subclasses of elementary classes. In particular, from Corollary 4.6 we obtain a recursive universal axiomatisation for $\mathcal{C}_{N}$ as a class of $\mathscr{L}$-structures. This is not a new result. Indeed, [41, Theorem 1.4] proves that $\mathcal{C}_{N}$ has a recursive axiomatisation using universal Horn formulas, and that paper attributes to W. Taylor a proof of the same result using the De Bruijn-Erdős theorem for graphs (i.e. that a graph is $N$-colourable when all its finite subgraphs are) [10].

Now, being universal, $\mathcal{C}_{N}$ is closed under isomorphisms, substructures and ultraproducts, and, as the class is also closed under taking direct products, it follows that $\mathcal{C}_{N}$ is a universal Horn class (see e.g. [5, Theorem V.2.23]). The universal Horn theory of $\mathcal{C}_{N}$ must be precisely the universal Horn consequences of our recursive axiomatisation, and so is also a recursively enumerable set, and consequently defines a recursive axiomatisation using Craig’s trick. Thus the prima facie stronger result of [41] follows easily from our version, which we got more or less for free from the general theory. Note that such a universal Horn axiomatisation is the best that can be hoped for, as for $N\geq 2$ there can be no finite axiomatisation of $\mathcal{C}_{N}$ [41, Theorem 1.5]. Of course, $\mathcal{C}_{1}$ is just the class of totally disconnected (edgeless) graphs.

Making good on the claims in the comments at the end of Section 4, we can also use our game-generated axioms to find a simple proof that $\mathcal{C}_{N}$ is not finitely axiomatisable when $N\geq 2$. First, for each $n\geq 1$ consider the cycle graph $C_{2n+1}$, and consider also the class $\mathcal{C}_{2}$ as a separation subclass of $\mathcal{G}$. Then the number of rounds $\exists$ can guarantee to survive in the simple $(C_{2n+1},\sigma)$ game scales linearly with $\log_{2}n$. Here $\exists$’s strategy is to always colour vertices consistently with their closest neighbour, and $\forall$’s best strategy is to make the maximum size of a chain of uncoloured vertices as small as possible each round - see Figure 3 for an illustration. Note that $\exists$ can use her strategy against any strategy used by $\forall$. The one described is optimal for him in the sense that it wins fastest.

Now, if $\mathcal{C}_{2}$ were finitely axiomatisable then a graph would be $2$-colourable if and only if $\exists$ could guarantee survival for a fixed finite number of rounds. By choosing $n$ large enough, $\exists$ can find a graph $C_{2n+1}$ where she does have such a strategy, but which is nevertheless not $2$-colourable, and this would result in contradiction. Thus the axiomatisation of $\mathcal{C}_{2}$ generated by Corollary 4.6 cannot be logically equivalent to a finite subset of itself, and it follows that $\mathcal{C}_{2}$ is not finitely axiomatisable. Note that as $C_{2n+1}\in\mathcal{C}_{3}$ for all $n$, this argument also shows that $\mathcal{C}_{2}$ is not finitely axiomatisable relative to $\mathcal{C}_{3}$.

Generalising, let $N>2$, and for each $n\geq 1$ define $G_{n}$ to be the graph obtained by taking the disjoint union of the cycle graph $C_{2n+1}$ and the complete graph $K_{N-2}$, and adding edges between every vertex of $C_{2n+1}$ and every vertex of $K_{N-2}$. Then, in the game where $\exists$ attempts to colour $G_{n}$ using $N$ colours, the choice of colours for $K_{N-2}$ forces her to attempt to colour $C_{2n+1}$ with two colours. We know this is impossible, but the number of rounds she can survive again scales with $\log_{2}n$. Here $\exists$’s strategy is to choose $N-2$ colours for $K_{N-2}$, and to use her strategy from the $N=2$ case for $C_{2n+1}$ with the two remaining colours. Thus $\mathcal{C}_{N}$ is not finitely axiomatisable for all $N\geq 2$. This provides a proof of [41, Theorem 1.5] that does not use the fact that the class of graphs with chromatic number $N$ is not elementary for all $N\geq 3$ [38, Theorem 6.3]. Note that, combined with the result for $N=2$, this argument also shows that $\mathcal{C}_{N}$ is not finitely axiomatisable relative to $\mathcal{C}_{N+1}$ for all $N\geq 2$.

Moreover, let $N\geq 3$ and define $\chi_{N}$ to be the class of graphs with chromatic number $N$. We can use our results on the lack of a finite axiomatisation for $\mathcal{C}_{N-1}$ relative to $\mathcal{C}_{N}$ to prove that $\chi_{N}$ is not elementary. To see this, first note that $\chi_{N}=\mathcal{C}_{N}\setminus\mathcal{C}_{N-1}$, and so $\mathcal{C}_{N}=\mathcal{C}_{N-1}\cup\chi_{N}$, which is a disjoint union. Now, as $\mathcal{C}_{N}$ and $\mathcal{C}_{N-1}$ are elementary, if $\chi_{N}$ is also elementary then $\mathcal{C}_{N-1}$ will be finitely axiomatisable relative to $\mathcal{C}_{N}$, by a variation of the compactness argument that says that if a class and its complement are elementary, then both will be basic elementary. As $\mathcal{C}_{N-1}$ is not finitely axiomatisable relative to $\mathcal{C}_{N}$, it follows that $\chi_{N}$ is not elementary. Thus we also obtain an alternative proof of [38, Theorem 6.3] (the original uses Erdős’ famous result that for all $m,k\in\omega$ there is a finite graph with chromatic number $\geq m$ and no circuits of length $\leq k$ [17]).

As a final observation, every first-order structure can be embedded into an ultraproduct of its finitely generated substructures (see e.g. [5, Theorem V.2.14]). Moreover, if a graph $G$ has the property that every finite subgraph is $N$-colourable, then, as $\mathcal{C}_{N}$ is elementary, an ultraproduct of these subgraphs must also be $N$-colourable, by Łoś’ theorem. Furthermore, as $\mathcal{C}_{N}$ is universal, its substructures must also be in $\mathcal{C}_{N}$, and so it follows that $G\in\mathcal{C}_{N}$. Thus, from the axiomatisation of $\mathcal{C}_{N}$ we also obtain a rather indirect proof of the De Bruijn-Erdős theorem. We must note that much simpler proofs are well known, so this last result is essentially a curiosity.

6.3. Clique covers

Let $N\in\omega$. We say a graph $G=(V,E)$ has an $N$-clique cover if its vertices can be partitioned into $N$ subsets, each of which is a clique. In other words, if there is a partition $V_{1},\ldots,V_{N}$ of $V$ such that the restriction of $E$ to $V_{n}$ produces a complete graph for all $n\in\{1,\ldots,N\}$. Note that a graph $G$ has an $N$-clique covering if and only if the complement graph $\bar{G}=(V,\bar{E})$ is $N$-colourable. As we can define $\bar{E}$ as $\neg E$, the results of Section 6.2 apply here, with the following exception. The class of undirected simple graphs with an $N$-clique cover is not closed under taking direct products for any $N$. To see this, consider the product of the totally disconnected graph with $N$ vertices with itself. So this class does not have a universal Horn axiomatisation (by [5, Theorem V.2.23] again), though it does have a recursive universal axiomatisation.

6.4. Harmonious colourings

The concept of a harmonious colouring for a graph was introduced in [19] and defined in its current form in [26]. Given $N\in\omega$, we say a graph has a harmonious $N$-colouring if it has an $N$-colouring in which each pair of colours can be used to colour a pair of adjacent vertices at most once. I.e. if we use $c(v)$ to denote the colour of a vertex, and if $v_{1},v_{2},v_{3},v_{4}$ are vertices with $c(v_{1})=c(v_{3})$ and $c(v_{2})=c(v_{4})$, then either $v_{1}=v_{3}$ and $v_{2}=v_{4}$, or there cannot be edges between both $\{v_{1},v_{2}\}$ and $\{v_{3},v_{4}\}$. Define $\mathscr{L}^{+}$, $\tau_{0}$, $\tau_{1}$ and $\tau_{2}$ as in Section 6.2. In addition, we define a sentence $\tau_{3}$ expressing that the vertices of two distinct edges cannot be coloured by the same pattern of colours. This sentence says that if $E(v_{1},v_{2})$ and $E(v_{3},v_{4})$ (i.e. the edges exist), and if $v_{1}\neq v_{3}$ or $v_{2}\neq v_{4}$ (i.e. the edges are distinct), then either $v_{1}$ is not the same colour as $v_{3}$, or $v_{2}$ is not the same colour as $v_{4}$.

[TABLE]

Now define

[TABLE]

Then $\sigma$ defines the class of graphs with harmonious $N$-colourings as an essentially finite separation subclass of $\mathcal{G}$. It again follows from Corollary 4.6 that this class has a universal recursive axiomatisation. Note that when $N\geq 2$ the class is not closed under taking direct products. To see this, note that a graph with a harmonious $N$-colouring can have at most ${N\choose 2}$ edges, as this is the maximum number of distinct colour pairs, and consider the product of the complete graphs $K_{N}$ and $K_{2}$. Each component has a harmonious $N$-colouring, but the product does not, simply because it has too many edges. So the class does not have a universal Horn axiomatisation. When $N=1$ the graphs must be totally disconnected just to have an $N$-colouring, which will be trivially harmonious.

From the fact that a graph with a harmonious $N$-colouring can have at most ${N\choose 2}$ edges, we can deduce that the axiomatisation produced here is equivalent to a finite one. Assuming $\forall$ plays in an efficient way, in other words, that he forces $\exists$ to define a new coloured pair each round if possible, he will either definitely be able to force a win in round $({N\choose 2}+1)$ at the latest, or he will have run out of useful moves in an earlier round. So, if $\exists$ has an $({N\choose 2}+1)$-strategy, then she has an $\omega$-strategy. Appealing to Lemma 4.7 proves the claim.

Note that it is proved in [26] that the problem of deciding, when given a graph $G$ and a positive integer $N$, whether $G$ has a harmonious colouring with $N$-colours is $\mathbf{NP}$-complete. As it is known that checking whether a first-order sentence is valid in a finite structure can be done in polynomial time (see [40, Proposition 3.1]), we may wonder whether we have accidentally proved $\mathbf{P}=\mathbf{NP}$. The answer, sadly, is no, because given $(G,N)$ we have to construct the appropriate sentence, which depends on $N$, before we can check it, and we have no reason to believe we can do this in polynomial time. There is an alternative version of the problem where $N$ is regarded as fixed, and so an instance is just a graph $G$. In this case our argument does indeed show the decision problem to be in $\mathbf{P}$, but this version of the problem is not $\mathbf{NP}$-complete.

Acknowledgment

The author would like to thank Robin Hirsch for, among other things, a suggestion that significantly simplified the key definitions, and the observation described in the preceding paragraph. The author would also like to thank the Department of Computer Science at UCL for hosting him while part of this paper was written. In addition, the author thanks the anonymous referee for their useful comments.