AbstractThe 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 ($$\sqsubseteq $$
⊑
) arises from the partial order given by modeling demonic choice ($$\sqcup $$
⊔
) of programs (see below for the formal relational definitions). We prove that the class $$R(\sqsubseteq , ;)$$
R
(
⊑
,
;
)
of abstract $$(\le , \circ )$$
(
≤
,
∘
)
structures isomorphic to a set of binary relations ordered by demonic refinement with composition cannot be axiomatised by any finite set of first-order $$(\le , \circ )$$
(
≤
,
∘
)
formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines $$R(\sqsubseteq , ;)$$
R
(
⊑
,
;
)
. We prove that a finite representable $$(\le , \circ )$$
(
≤
,
∘
)
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.
Reducts of Relation Algebras: The Aspects of Axiomatisability and Finite Representability
