Finite representability of semigroups with demonic refinement

The motivation for using demonic calculus for binary relations stems from the behaviour of demonic turing machines, when modelled relationally. Relational composition (; ) models sequential runs of two programs and demonic refinement (⊑) arises from the partial order given by modeling demonic choice (⊔) of programs (see below for the formal relational definitions). We prove that the class R(⊑,;) of abstract (≤,∘) structures isomorphic to a set of binary relations ordered by demonic refinement with composition cannot be axiomatised by any finite set of first-order (≤,∘) formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines R(⊑,;). We prove that a finite representable (≤,∘) structure has a representation over a finite base. This appears to be the first example of a signature for binary relations with composition where the representation class is non-finitely axiomatisable, but where the finite representation property holds for finite structures