The Thins Ordering on Relations
Ed Voermans, Jules Desharnais, Roland Backhouse
TL;DR
The paper introduces the thins ordering $\textsf{thins}$ on relations, showing that the axiom of choice (AC) is equivalent to minimal elements of $\textsf{thins}$ on pers being the indices of pers, and extending these ideas to core relations and maximal pers. It develops a point-free relation-algebra framework with a typed monoid, lattice, and converse, and establishes that $\textsf{thins}$ is a partial order on pers, with indexes characterized via thinning accuracy. A key result is that, under AC, minimal elements of the extended thins ordering on arbitrary relations are precisely the core relations, while maximal pers on pers align with equivalence relations, generalized beyond concrete relations by avoiding the cone rule. The work provides deeper insights into strengthening point-free reasoning about relations and broadens the modeling landscape beyond concrete relations, with careful constructions (e.g., transitive closures) that remain valid without case-splitting on emptiness. Overall, AC emerges as a powerful tool for controlling the structure of relation hierarchies in a purely point-free setting, yielding robust minimality and maximality characterizations applicable to varied models.
Abstract
Earlier papers \cite{VB2022,VB2023a,VB2023b} introduced the notions of a core and an index of a relation (an index being a special case of a core). A limited form of the axiom of choice was postulated -- specifically that all partial equivalence relations (pers) have an index -- and the consequences of adding the axiom to axiom systems for point-free reasoning were explored. In this paper, we define a partial ordering on relations, which we call the \textsf{thins} ordering. We show that our axiom of choice is equivalent to the property that core relations are the minimal elements of the \textsf{thins} ordering. We also characterise the relations that are maximal with respect to the \textsf{thins} ordering. Apart from our axiom of choice, the axiom system we employ is paired to a bare minimum and admits many models other than concrete relations -- we do not assume, for example, the existence of complements; in the case of concrete relations, the theorem is that the maximal elements of the \textsf{thins} ordering are the empty relation and the equivalence relations. This and other properties of \textsf{thins} provide further evidence that our axiom of choice is a desirable means of strengthening point-free reasoning on relations.