An Algebra of Properties of Binary Relations

TL;DR

This paper develops an algebraic framework for analyzing properties of binary relations through boolean combinations of their fundamental operations, providing tools for implication analysis and property equivalence.

Contribution

It introduces an algebraic system for unary operations on binary relations, including a complete set of implications and methods for property equivalence analysis.

Findings

A comprehensive table for extensional equality of lifted properties.

A complete axiom set for implications between properties.

Counter-example generator and theorem prover for relation properties.

Abstract

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").