Brett McLean

The first-order logic of disjoint union

Disjoint union is a partial binary operation on sets, defined if and only if the two sets are disjoint, in which case it yields the union. This operation is used in the semantics of separation logic, where it is applied to abstract models of heap states. We will talk about the class of partial algebras representable as algebras of sets equipped with disjoint union. We will describe an infinite first-order axiomatisation of this representation and then show that no finite axiomatisation exists. We will also discuss a possible notion of complete representability.