Abstract Using a variation of the rainbow construction and various pebble and colouring games, we prove that RRA, the class of all representable relation algebras, cannot be axiomatised by any first-order relation algebra theory of bounded quantifier depth. We also prove that the class At(RRA) of atom structures of representable, atomic relation algebras cannot be defined by any set of sentences in the language of RA atom structures that uses only a finite number of variables.

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.

Abstract We define an order polarity to be a polarity $(X,Y,{\operatorname{R}})$ where $X$ and $Y$ are partially ordered, and we define an extension polarity to be a triple $(e_X,e_Y,{\operatorname{R}})$ such that $e_X:P\to X$ and $e_Y:P\to Y$ are poset extensions and $(X,Y,{\operatorname{R}})$ is an order polarity. We define a hierarchy of increasingly strong coherence conditions for extension polarities, each equivalent to the existence of a preorder structure on $X\cup Y$ such that the natural embeddings, $\iota _X$ and $\iota _Y$, of $X$ and $Y$, respectively, into $X\cup Y$ preserve the order structures of $X$ and $Y$ in increasingly strict ways. We define a Galois polarity to be an extension polarity satisfying the strongest of these coherence conditions and where $e_X$ and $e_Y$ are meet- and join-extensions, respectively. We show that for such polarities the corresponding preorder on $X\cup Y$ is unique. We define morphisms for polarities, providing the class of Galois polarities with the structure of a category, and we define an adjunction between this category and the category of $\varDelta _1$-completions and appropriate homomorphisms.