二元关系性质目录：蕴涵、不相容与独立性结果
A Catalogue of Properties of Binary Relations: Entailments, Incompatibilities, and Independence Results
浏览论文内容
中文总结 AI 辅助
本文研究十五种二元关系性质，给出经Lean证明的霍恩蕴涵基、反模型及关系代数翻译，并证明在非空域上霍恩闭包对正蕴涵完备。
中文摘要 AI 辅助
我们研究了十五种二元关系的性质，这些性质在模态逻辑、序与偏好理论以及关系代数中已有既定应用。组织问题的出发点是实用性的：一旦已知一个关系的某些性质，哪些进一步的性质会随之而来，哪些组合会迫使退化，哪些性质仍然保持独立？我们给出了一个经过证明的基本蕴涵和复合蕴涵的霍恩基，为非蕴涵提供了显式反模型，并给出了所有十五种性质的关系代数翻译。模态讨论包括通常的斯科特-莱蒙对应关系，以及吉拉尔迪和明茨研究的传递稠密框架的逻辑。穷举有限枚举和有针对性的模型搜索用于发现，而目录在Lean中得到了认证。一个经内核检查的覆盖计算遍历所有2^15 = 32,768个前件集合和所有十五个可能的后件。其51条规则的霍恩清单在定义上与Lean证明的语义可靠性证明相耦合，其49个见证行在定义上与Lean认证的有限或无限关系相耦合。因此，在非空域上，霍恩闭包对于十五个选定性质之间的正蕴涵是完备的，并且一致性分类对于它们的正组合是完备的。
英文摘要
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.
发表机构
- Karolinska Institutet（卡罗林斯卡学院）
机构由 AI 辅助整理，请以论文原文为准。
