An Algebra of Properties of Binary Relations

Overview & Synopsis

We consider all 16 unary operations that, given a homogeneous binary relation R, define a new one by a boolean combination of xRy and yRx. Operations can be composed, and connected by pointwise-defined logical junctors. We consider the usual properties of relations, and allow them to be lifted by prepending an operation. We investigate extensional equality between lifted properties (e.g. a relation is connex iff its complement is asymmetric), and give a table to decide this equality. Supported by a counter-example generator and a resolution theorem prover, we investigate all 3-atom implications between lifted properties, and give a sound and complete axiom set for them (containing e.g. "if R's complement is left Euclidean and R is right serial, then R's symmetric kernel is left serial").