从塔斯基立体几何中的区域拓扑到点类拓扑
From Regional Topology to Point-Class Topology in Tarski's Geometry of Solids
浏览论文内容
中文总结 AI 辅助
研究塔斯基立体几何中从区域拓扑到点类拓扑的转换，在名义分体论框架内形式化重构，通过定义点开复数及邻域闭包算子，证明其满足库拉托夫斯基闭包公理，区分多种性质并避免点的具体化。
中文摘要 AI 辅助
塔斯基的立体几何从同心球区域族重构点状对象，而非将点作为原始实体。我们在受莱斯涅夫斯基启发的名义分体论框架内，于Coq中形式化此重构。主要问题是无点的区域几何如何在由此类重构点得到的对象上支持库拉托夫斯基闭包算子。我们区分了塔斯基 - 莱斯涅夫斯基立体的区域拓扑与基于球代表构建的点类拓扑。点状对象被视为同心点类，即球代表在同心族相等下的等价类。区域对象提供基本邻域源，但闭包作用于点类复数而非立体本身。我们定义点开复数并在其上引入基于邻域的闭包算子。核心Coq定理证明该算子满足四个库拉托夫斯基闭包公理。我们进一步将点闭复数定义为此闭包的不动点并导出拓扑边界余项。形式化区分了区域开放性、代表等价性和拓扑附着性，同时避免将重构点作为分体论个体具体化。
英文摘要
Tarski's geometry of solids reconstructs point-like entities from concentric families of spherical regions rather than taking points as primitive. We formalize this reconstruction in Coq within a nominal mereological framework inspired by Leśniewski, and study how the regional geometry of solids induces a topology on reconstructed point-classes without adding new point individuals. Three of Tarski's postulates concerning solids and interior points, P2--P4, are derived as theorems. We refine Tarski's interior-point notion and define a regional interior operator satisfying the four Kuratowski interior axioms, together with a boundary operation and an encoding of RCC8 relations. We then pass to the setoid of ball representatives modulo same_center. Each ball generates a stable basic point-plural GBasicPointSet(Q), and these plurals form a basis for a metatheoretic topology on reconstructed point-classes. This topology is Hausdorff under Tarski's separation axiom Three_points and non-discrete under the local richness hypothesis BallCenterBundle. Finally, geometric neighbourhoods yield a closure operator GClosurePoint satisfying the four Kuratowski closure axioms and respecting extensional point-set equality. The formalization thus verifies the passage from a regional topology of solids to a Hausdorff topology and neighbourhood closure on reconstructed point-classes.
