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

技術要約：セパロイドにおける離隔の計算論

問題提起
本論文は、ユークリッド空間におけるコンパクト凸体の凸包の離散性が誘発する論理的および組合せ論的な構造を調査している。有限個の「サイト（site）」の集合 $E$ が与えられ、各サイトが空でないコンパクト凸体に関連付けられているとき、本研究は、サイトの互いに素な部分集合間の「離隔（apartness）」の関係（$A \mathbin{\#} B$）に焦点を当てる。この関係は、$A$ に対応する体の和集合の凸包と、$B$ に対応する体の和集合の凸包が互いに素である場合に成立する。中心となる問題は、幾何学的な詳細（次元、形状、座標）を、分離パターンによる論理的帰結を保持したまま、どの程度まで「忘却」できるかである。具体的には、この関係を公理化し、効果的な表現を提供し、それに関する推論の複雑さを分類することを目的としている。

手法
著者らは、凸幾何学、組合せトポロジー、および証明論を組み合わせた多層的なアプローチを採用している。

1. 公理的基礎： 本論文は、あらゆる凸体のシーン（scene）が満たす3つの基本的法則、すなわち「対称性（Symmetry）」、「両側包含（Bilateral Subsumption/単調性）」、「空虚性（Vacuity/空集合はすべてから離隔している）」を特定している。これらの法則は「離隔セパロイド（apartness separoid）」と呼ばれる構造を定義する。これは、既存の文献（Strauszら）に見られる非サイクルなセパロイドと、分離関係をその相補的な「ラドンの分割（Radon partition）」側から捉えるという点で、同型（cryptomorphic）であることが示されている。
2. 効果的な表現： 有限の離隔セパロイドを有理多面体を用いて実現するための構成的定理が開発された。最小次元を最適化する従来の幾何学的実現とは異なり、この構成は「証明に読み取り可能（proof-readable）」である。各最大分離に一つの座標を割り当て、境界付きのビット高さを持つ明示的な有理座標を使用する。この構成は、すべての分離に対して一様なユークリッド・マージン（少なくとも2）を保証し、摂動に対する堅牢性を提供する。
3. 安定性解析： 距離関数と外側平行体を用いて、実現の安定性を分析している。実現は、半径 $r < 1$ の外側平行拡大に対して不変であり、また、各物体を（関係を変えることなく）フル次元の $C^{1,1}$ 体へと太らせることが可能であることを示している。
4. 論理計算と複雑性： 分離の言明を表す原子（atom）を持つ形式言語 $L_E$ を定義する。本論文では、正のシーケント計算（$SC_0$）とブール計算（$ACE$）を導入している。充足可能性、妥当性、および含意の決定問題を分析し、それらの計算複雑性を確立している。
5. 層化（Stratification）： 階層化の規律を導入して保存定理を証明し、ブール層（複合的な推論）が原子層（正の事実）に対して無効（inert）であることを示している。

主要な貢献と結果

• 同型的な公理化： 本論文は、3つの法則（対称性、両側包含、空虚性）が凸体の離隔関係を完全に公理化することを確立している。これは、十分な周囲次元が確保されている限り、幾何学的な詳細を「忘却」しても、論理的帰結関係には何の影響も及ぼさないことを裏付けている。
• 効果的な有理表現（定理 4.3）： すべての有限離隔セパロイドは、有理多面体のシーンによって実現される。この構成は出力に敏感（output-sensitive）である：
  • 座標は最大分離によってインデックス付けされる。
  • すべての座標は、明示的に境界付けられた分子および分母のサイズ（$O(\log n)$ ビット）を持つ有理数である。
  • 実現は、すべての両側分離に対して少なくとも2の一様なマージンを保証する。
  • この構成により、さまざまな入力形式（完全な表、生成子、またはメンバーシップ・オラクル）から、最大分離および最小ラドン分割を、隠れた算術的膨張なしに指数的な出力コストで列挙することが可能である。
• 安定性と堅牢性（定理 4.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$ のすべての $d$ について、帰結関係は次元に依存しない幾何学的帰結（$|=_{geo}$）と同一である。
  • この閾値はシャープであることが証明されており、$|E|-1$ 未満の次元では、反駁可能な言明の集合が厳密に拡大する。
• 論理計算と複雑性：
  • 正の含意： 正の含意は単純な包含関係に崩壊する。ある言明が前提集合から導かれるのは、それが空虚であるか、あるいは（入れ替えの可能性を含め）単一の前提によって成分ごとに支配されている場合のみである。ソートされたエンコーディングを用いた場合、このチェックは入力サイズに対して線形である。
  • ブール閉包： ブール計算は健全、完全、かつ決定可能である。充足可能性はNP完全であり、妥当性はcoNP完全である。
  • 保存性（定理 7.3）： 層化条件は、ブール層が原子層に対して無効であることを証明する。古典的な推論（否定、選言、場合分け）をどれほど用いても、原子データによる包含ではない新しい正の離隔の事実を導き出すことはできない。

意義と主張
本論文は、分離に関する議論の「安定した核」は小さく、明確であり、完全に包含的であることを主張している。一度周囲次元が $|E| - 1$ を超えると、シーンの具体的な幾何学は論理的帰結にとって無関係になり、その関係は3つの公理的法則によって完全に捉えられる。

その意義は、既存のセパロイド理論に対して「論理的かつ効果的な層」を提供することにある。従来の作業が普遍性と準同型に焦点を当てていたのに対し、本論文は以下の点を提供している：

1. 有理的なマージンを持つ定量的な表現定理を提供し、論理構造を座標ごとに検査可能にしている。
2. 精緻な複雑性分類を行い、正の含意の自明性と、ブール結合によって導入される困難さを区別している。
3. 「データ」（原子的な分離）と「推論」（ブール論理）を形式的に分離する保存性の結果を提供し、後者が新たな幾何学的制約を加えないことを示している。

本論文は、新しい幾何学的現象の発見を目指すものではなく、凸分離の論理的限界を厳密に定式化するものであり、安定した次元に依存しない領域に留まる限り、幾何学的な詳細を「忘却」することは論理的帰結の観点からはコストフリーであることを示している。