A Calculus of Apartness over Separoids: Effective Convex Representation, Stratified Conservativity, and the Complexity of Entailment

技术摘要：分离体上的隔离微积分 (A Calculus of Apartness over Separoids)

问题陈述
本文研究了由欧几里得空间中紧凸体的凸包不相交性所诱导的逻辑与组合结构。给定一个有限集合的“位点” $E$，其中每个位点都与一个非空紧凸体相关联，研究重点在于位点不相交子集之间的“隔离” (apartness, $A \mathbin{\#} B$) 二元关系。若 $A$ 与 $B$ 所对应的集合并集的凸包是互不相交的，则该关系成立。核心问题在于：在保留分离模式的逻辑后果的同时，可以在多大程度上忽略几何细节（维度、形状、坐标）？具体而言，本文旨在对这种关系进行公理化，提供一种有效的表示方法，并对对其进行推理的复杂度进行分类。

研究方法
作者采用了一种结合凸几何、组合拓扑和证明论的多层方法：

1. 公理化基础： 本文确定了任何凸体场景所满足的三个基本律：对称性 (Symmetry)、双边包含性 (Bilateral Subsumption，即单调性) 以及空集律 (Vacuity，即空集与任何集合都隔离)。这些律定义了一种称为“隔离分离体” (apartness separoid) 的结构，本文证明该结构与现有文献（Strausz 等人）中的无环分离体 (acyclic separoids) 是密码同构的，即从其互补的“拉登划分” (Radon partition) 侧来观察分离关系。
2. 有效表示： 开发了一种构造性定理，用于利用有理多胞体实现任何有限的隔离分离体。与以往优化最小维度的几何实现不同，该构造是“证明可读的”。它为每个极大分离分配一个坐标，并使用具有有界位高 (bit height) 的显式有理坐标。该构造确保了所有分离都具有统一的欧几里得裕度（至少为 2），从而对扰动具有鲁棒性。
3. 稳定性分析： 利用距离函数和外平行体，本文分析了实现的稳定性。研究表明，隔离关系在半径为 $r < 1$ 的外平行扩张下是不变的，并且可以将这些物体增厚为全维的 $C^{1,1}$ 物体而不改变其关系。
4. 逻辑微积分与复杂度： 定义了一个以分离断言为原子的形式语言 $L_E$。本文引入了正序言演算 ($SC_0$) 和布尔演算 ($ACE$)。本文分析了满足性、有效性和蕴含问题的决策问题，并确定了它们的计算复杂度。
5. 分层： 本文引入了一种分层规范来证明一个保守性定理，证明了布尔层（复合推理）对于原子层（正事实）是惰性的。

主要贡献与结果

• 密码同构公理化： 本文确立了对称性、双边包含性和空集律这三个律完全公理化了凸体的隔离关系。这证实了“遗忘”几何细节在逻辑后果关系方面没有任何代价，只要环境维度足够高。
• 有效有理表示 (定理 4.3)： 每个有限隔离分离体都由有理多胞体实现。该构造是输出敏感的：
  • 坐标由极大分离进行索引。
  • 所有坐标均为有理数，且具有显式的有界分子和分母大小（$O(\log n)$ 位）。
  • 实现保证了每个双边分离至少具有 2 的统一裕度。
  • 该构造允许从各种输入格式（完整表、生成元或成员判定器）中枚举极大分离和最小拉登划分，其输出成本为指数级，但不存在隐藏的算术膨胀。
• 稳定性与鲁棒性 (定理 1.13)： 该实现是稳定的。如果场景中的每个物体都被替换为其半径为 $r < 1$ 的外平行体，隔离关系保持不变。此外，这些物体可以被平滑为具有 $C^{1,1}$ 边界的物体，同时保留其关系。
• 维度层级与阈值 (定理 4.17)： 本文精确地刻画了基于环境维度 $d$ 的后果关系层级。
  • 当 $d < |E| - 1$ 时，后果关系形成一个严格递减链：$|=_{0} \supsetneq |=_{1} \supsetneq \dots \supsetneq |=_{|E|-2}$。
  • 维度层级在 $d = |E| - 1$ 时恰好稳定。对于所有 $d \ge |E| - 1$ 的情况，其后果关系与无维度几何后果关系 ($|=_{geo}$) 相同。
  • 该阈值被证明是尖锐的；在维度低于 $|E|-1$ 时，会严格扩大可驳斥断言的集合。
• 逻辑微积分与复杂度：
  • 正蕴含： 正蕴含退化为简单的包含关系。一个断言由一组前提推导出来，当且仅当它是空值的，或者（在可能经过交换后）被单个前提成分性地支配。对于排序编码，这一检查对于输入规模是线性的。
  • 布尔闭包： 布尔演算是可靠、完备且可判定的。满足性问题是 NP-完全的，有效性问题是 coNP-完全的。
  • 保守性 (定理 7.3)： 一个形式化的分层条件证明了布尔层在原子层上是惰性的。任何经典的推理（否定、析取、分类讨论）都无法推导出一个不是原子数据之包含关系的新的正隔离事实。

意义与主张
本文声称，隔离讨论的“稳定核心”是微小的、精确已知的，并且完全是包含性的。本文认为，一旦环境维度超过 $|E| - 1$ 的阈值，场景的具体几何形状对于逻辑后果而言就变得无关紧要了；该关系完全由这三条公理律所捕捉。

其意义在于为现有的分离体组合理论提供了一个“逻辑与有效的层面”。虽然以往的工作侧重于普遍性和同态，但本文提供了：

1. 一个具有有理裕度的定量表示定理，使得逻辑结构可以通过坐标逐一检查。
2. 一个精确的复杂度分类，区分了正蕴含的平凡性与布尔组合引入的复杂性。
3. 一个保守性结果，形式化地分离了“数据”（原子分离）与“推理”（布尔逻辑），表明后者并未增加新的几何约束。

本文的定位并非是对新几何现象的发现，而是对凸分离逻辑极限的严密形式化，证明了只要处于稳定的、无维度的范畴内，遗忘几何细节的代价在逻辑后果方面是零成本的。