Complete representation by partial functions for signatures containing antidomain restriction

TL;DR

This paper explores complete representations of algebras with partial functions involving antidomain restriction and other operations, establishing conditions for representability and axiomatizability across various signatures.

Contribution

It characterizes when complete representations exist for different signatures and provides explicit representations and axiomatizations for classes of such algebras.

Findings

Meet-complete representations are strictly stronger than join-complete in some signatures.

Atoms are separating for meet-complete representations when composition is absent.

Classes of completely representable algebras are not axiomatisable by existential-universal-existential first-order theories.

Abstract

We investigate notions of complete representation by partial functions, where the operations in the signature include antidomain restriction and may include composition, intersection, update, preferential union, domain, antidomain, and set difference. When the signature includes both antidomain restriction and intersection, the join-complete and the meet-complete representations coincide. Otherwise, for the signatures we consider, meet-complete is strictly stronger than join-complete. A necessary condition to be meet-completely representable is that the atoms are separating. For the signatures we consider, this condition is sufficient if and only if composition is not in the signature. For each of the signatures we consider, the class of (meet-)completely representable algebras is not axiomatisable by any existential-universal-existential first-order theory. For 14 expressively distinct signatures, we show, by giving an explicit representation, that the (meet-)completely representable algebras form a basic elementary class, axiomatisable by a universal-existential-universal first-order sentence. The signatures we axiomatise are those containing antidomain restriction and any of intersection, update, and preferential union and also those containing antidomain restriction, composition, and intersection and any of update, preferential union, domain, and antidomain.