A Catalogue of Properties of Binary Relations: Entailments, Incompatibilities, and Independence Results
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.
Related
- Independence properties for tree beta models
- Ramsey properties of trees and C-relations via the partite construction
- Tree-independence number VIII. 3PC-free graphs have logarithmic tree-independence number
- Uniform generalization of Goodstein's theorem and Cichon's independence proof
- Equi-dependence implying independence
BibTeX
@misc{boman2026catalogue,
title = {{A Catalogue of Properties of Binary Relations: Entailments, Incompatibilities, and Independence Results}},
author = {Magnus Boman},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.13317},
eprint = {2609.13317},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.13317},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A Catalogue of Properties of Binary Relations: Entailments, Incompatibilities, and Independence Results
AU - Magnus Boman
PY - 2026
DA - 2026/09/10
PB - arXiv
DO - 10.48550/arxiv.2609.13317
UR - https://arxiv.org/abs/2609.13317
AB - 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.
ER -