A Catalogue of Properties of Binary Relations: Entailments, Incompatibilities, and Independence Results
Magnus Boman
cs.LO
Sep 10, 2026 · v1
math.LO
TL;DR
A catalogue of entailments, incompatibilities, and independence results for fifteen binary-relation properties is certified with kernel-checked Lean proofs.
Abstract
We study fifteen properties of binary relations that have established uses in modal logic, order and preference theory, and relation algebra. The organising question is pragmatic: once some properties of a relation are known, which further properties follow, which combinations force degeneracy, and which properties remain independent? We give a proved Horn basis of elementary and compound entailments, explicit countermodels for non-entailments, and a relation-algebraic translation of all fifteen properties. The modal discussion includes the usual Scott–Lemmon correspondences and the logic of transitive dense frames studied by Ghilardi and Mints. Exhaustive finite enumeration and targeted model search are used for discovery, while the catalogue is certified in Lean. A kernel-checked coverage calculation ranges over all 2^15 = 32,768 antecedent sets and all fifteen possible consequents. Its 51-rule Horn manifest is coupled definitionally to Lean proofs of semantic soundness, and its 49 witness rows are coupled definitionally to Lean-certified finite or infinite relations. Consequently, over non-empty domains, the Horn closure is complete for positive entailment among the fifteen selected properties, and the consistency classification is complete for their positive combinations.
Problem
Given a selection of fifteen properties of binary relations from modal logic, order/preference theory, and relation algebra, the question is which further properties are entailed, which combinations force degeneracy, and which remain independent.
Approach
Fifteen first-order properties are defined and given relation-algebraic translations. Exhaustive finite enumeration and targeted model search discover entailments, unsatisfiable combinations, and countermodels. The resulting catalogue is certified in Lean: a 51-rule Horn manifest is definitionally coupled to Lean proofs of semantic soundness, and 49 witness rows are coupled to Lean-certified finite or infinite relations. A kernel-checked coverage calculation ranges over all 2^15 antecedent sets and fifteen consequents.
Results
Over non-empty domains the Horn closure is complete for positive entailment among the fifteen properties, and the consistency classification is complete for their positive combinations. Named classes (preorders, partial/total orders, equivalence relations) are recovered.
| Property | Relation-algebraic form |
|---|
| P1 Refl | 1'⊆R |
| P4 Sym | R=R˘ |
| P7 Trans | R;R⊆R |
| P10 Dense | R⊆R;R |
| P13 Eucl | R˘;R⊆R |
Relation-algebraic translation of the fifteen properties (excerpt)
