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.