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

## Key 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.