A Topological Rewriting of Tarski's Mereogeometry¶
会议: AAAI 2026
arXiv: 2511.12727
代码: https://www.univ-smb.fr/listic/technologies/logiciels/modeles-decidables-pour-la-specification-d-ontologies/extending-tarskis-mereo-geometry-with-topological-definitions/ (Coq库)
领域: 形式化推理 / 空间推理 / 数理逻辑
关键词: Tarski几何, 拓扑学, Mereology(部分整体论), Coq定理证明, 定性空间推理(QSR)
一句话总结¶
本文在Coq定理证明器中，基于λ-MM库（Leśniewski部分整体论的类型论实现），将Tarski的实体几何（geometry of solids）重新用拓扑学语言改写：先证明部分整体论的类（m-class）对应正则开集从而构成拓扑空间，再证明Tarski几何形成该拓扑的子空间并满足Hausdorff（T₂）分离性质，从而为定性空间推理提供了一个统一的、机器验证的部分整体论-几何-拓扑理论。
背景与动机¶
定性空间推理（QSR）是AI中表达和推理空间关系的重要分支，常见理论如RCC8、contact algebra等。这些理论的共同基础是将部分整体论（mereology）与拓扑学结合。然而现有方法存在几个关键痛点： 1. 边界的本体论地位不清：拓扑边界到底是空间实体还是抽象实体，很多理论没说清楚 2. 可判定性未解：许多扩展理论的可判定片段尚未确定 3. 推理机制不健全：缺乏严格的形式化验证，空间表示的实用性受限 4. 部分整体论的表达力不足：直接用一阶逻辑映射part-of关系，太浅，表达力差
Tarski早在1929年就提出了"实体几何"——用球（ball）作唯一原语来构建无点几何，但这个优美的理论长期缺乏与现代拓扑学的严格桥接。λ-MM库虽然在Coq中形式化了Leśniewski部分整体论和Tarski几何的一部分，但尚未建立拓扑结构。
核心问题¶
如何在严格的形式化框架中，将Tarski基于部分整体论的无点几何与真正的拓扑空间统一起来？具体来说：(1) 部分整体论中的"类"(m-class)能否自然地对应拓扑学中的正则开集？(2) Tarski的几何公设能否用拓扑学原语重新表述和证明？(3) 这个统一理论能否形式化验证（在Coq中证明），并且具有足够的表达力（如Hausdorff性质）？
这个问题重要，因为它关系到AI空间推理的逻辑基础是否健全——如果基础理论不严谨，建立在上面的推理系统就不可靠。
方法详解¶
整体框架¶
论文的思路分三步走： - 输入：λ-MM库（已有Leśniewski本体论+部分整体论+部分Tarski几何的Coq实现） - 第一步（Section 3）：在部分整体论上添加拓扑定义，证明部分整体空间就是一个拓扑空间 ⟨N, 𝕋_MM⟩ - 第二步（Section 4）：以Tarski的球作为子基，在该拓扑中构造几何子空间 ⟨balls, 𝕋_MG⟩，证明Tarski的公设2、3、4 - 输出：一个统一的、经Coq机器验证的 部分整体论-拓扑-几何 理论，具备Hausdorff性质
关键设计¶
-
Leśniewski本体论的类型论编码（λ-MM基础）：系统的基石是Leśniewski的"名称逻辑"(LO)，用归纳类型N表示名称，核心算子η充当名称间的分类关系（类似类型论中的":"但在单一语法层内运作）。部分整体论的part-of(pt)、klass等都是η的复合关系。这种编码的精妙之处在于：名称的存在性由归纳构造保证，身份由语法决定而非语义，从而避免了经典逻辑对外部模型的依赖。
-
部分整体论即拓扑（核心桥接）：作者定义了meet/join算子（分别对应名称的合取/析取），然后定义内部算子：interior(Q) = Q当且仅当Q是individual。关键洞察是：m-class（部分整体类）恰好对应正则开集——它们是"内部的闭包的内部等于自身"的集合。作者用Coq type class定义了Kuratowski公理（空间保持、内包性、幂等性、交集保持），并证明部分整体论的结构满足所有四条公理（Theorem 1）。有趣的是，他们还证明了这个拓扑是clopen的（Theorem 2：边界为空），说明纯部分整体论的拓扑表达力确实不够。
-
Tarski几何的拓扑重写：引入ball作为原语和Gspace = klass(balls)作为几何空间。点(Point)定义为同心球的等价类（二阶对象），区域(Region)定义为球的m-class。核心创新是定义了"饱和内部点"(SatInteriorPoint)——要求内部点的生成球完全包含在区域内（原始Tarski定义的球可能超出区域边界），这使得可以构造满足Kuratowski公理的拓扑内部算子InteriorG。用这个算子实例化同一个type class，得到几何拓扑 𝕋_MG（Theorem 6）。
-
边界与Hausdorff性质：边界定义为"既不在区域内也不在其补集内的点"（与Jaśkowski 1948一致）。证明了内部点与边界点不相交（Lemma 9）、边界不是区域（Lemma 10）、区域的边界等于其补的边界（Lemma 11）。利用betweenness公理（任意两点间存在第三点），证明了Gspace满足T₂(Hausdorff)分离性——不同心的点有不相交的邻域（Theorem 8）。
损失函数 / 训练策略¶
不适用（本文是纯数学/形式化工作，无训练过程）。Coq中的证明使用CoqHammer（主要调用Vampire和Eprover自动定理证明器）半自动完成。
实验关键数据¶
本文是定理证明工作，没有传统意义上的实验数据表。核心"实验结果"是定理的证明：
| 定理 | 内容 | 意义 |
|---|---|---|
| Theorem 1 | 部分整体论满足Kuratowski公理 | m-class构成拓扑空间 |
| Theorem 2 | 纯部分整体拓扑是clopen的 | 说明需要几何扩展 |
| Theorem 3 (Tarski P2) | 区域的内部点类是非空正则开集 | 重新证明Tarski公设2 |
| Theorem 4 (Tarski P3) | 内部点的正则开集类是区域 | 重新证明Tarski公设3 |
| Theorem 5 (Tarski P4) | 内部点包含关系蕴含part-of | 重新证明Tarski公设4 |
| Theorem 6 | 几何空间满足Kuratowski公理 | 区域构成拓扑空间 |
| Theorem 7 | 闭包=内部∪边界 | 标准拓扑性质 |
| Theorem 8 | Gspace是Hausdorff的 | T₂分离性 |
消融实验要点¶
- 纯部分整体论 vs 加入几何：Theorem 2证明纯部分整体论只能产生clopen拓扑（边界为空），表达力不足。加入Tarski的球原语后才能得到有意义的边界和Hausdorff性质——这说明几何扩展是必要的。
- 原始InteriorPoint vs SatInteriorPoint：原始Tarski定义的内部点的球可以超出区域，不足以构造拓扑基。引入"饱和"约束后才满足Kuratowski公理——这是方法论上的关键修改。
亮点¶
- 用一个Coq type class统一两层拓扑：Definition 6定义的Kuratowski type class被实例化两次——一次用于部分整体论拓扑（Theorem 1），一次用于几何拓扑（Theorem 6），展示了极其优雅的抽象设计
- "部分整体论是clopen拓扑"这个否定结果非常有洞察力：它精确地量化了"部分整体论不够用"这个直觉，为何需要引入几何原语有了严格的数学论证
- 饱和内部点(SatInteriorPoint)的创新定义是使Tarski几何能被拓扑化的关键技术修改，简洁而必要
- 将形式验证引入空间推理基础理论：在Coq中机器验证所有定理，确保理论的绝对可靠性
局限性 / 可改进方向¶
- 抽象程度极高：论文几乎完全停留在数学基础层面，没有给出任何具体的空间推理应用实例
- 计算复杂性未讨论：构建了理论但没有分析其可判定性或计算复杂度
- 与RCC8等主流QSR理论的具体对接缺失：虽然声称比RCC8更具表达力，但缺少系统的对比分析
- Coq证明的自动化程度：依赖CoqHammer和外部ATP（Vampire/Eprover），证明的透明性和可理解性可能受限
- 3D假设：猜想Gspace与ℝ³同胚但未证明，限制了对高维空间的推广
- 未来可探索：与神经符号AI的结合（论文结论中提到用λ-MM库为LLM提供符号监督，但未展开）
与相关工作的对比¶
- vs RCC8：RCC8基于contact relation的一阶逻辑公理化，表达力受限于拓扑连接关系。本文基于Tarski几何+部分整体论，在Coq中机器验证，能表达边界、Hausdorff性质和凸性等更丰富的空间概念
- vs Gruszczyński & Pietruszczak (2008)：也对Tarski几何做了完整发展，但是在纯一阶逻辑中，未建立拓扑结构。本文在依赖类型论中实现并加入了拓扑层
- vs Borgo & Masolo (2010)：提出full mereogeometry，采用点作为球的滤结构的思路被本文沿用，但他们未使用机器验证
启发与关联¶
这篇论文属于纯数理逻辑/形式化方法领域，与当前CV/ML研究方向关联较远。但有两个潜在启发： 1. 空间推理的形式化基础：如果要为VLM（视觉语言模型）构建更可靠的空间推理能力，Tarski式的无点几何提供了一种不依赖坐标系的空间表示思路 2. 神经符号整合：论文结论中提到λ-MM库可为LLM提供符号监督训练数据，这是一个值得探索的方向——用形式化验证的空间推理知识来增强LLM的空间理解能力
评分¶
- 新颖性: ⭐⭐⭐⭐ 将部分整体论证明为拓扑空间并重写Tarski公设是有意义的贡献，但主要是已有理论的形式化连接
- 实验充分度: ⭐⭐⭐ 定理证明充分但无应用实验，作为AAAI论文缺少实践验证
- 写作质量: ⭐⭐⭐ 数学符号密集，对非专业读者极不友好；但逻辑结构清晰
- 价值: ⭐⭐⭐ 对空间推理形式化基础有贡献，但短期内对主流AI应用的影响有限