塔斯克几何的拓扑改写

基于 Goodman 式全体论和伪拓扑的定性空间模型常为高级几何推理带来问题，因为它们缺乏真正的欧几里得几何和完全发展的拓扑空间。我们通过扩展现有基于依赖类型理论的形式化（使用 Coq 证明助手），并结合 Whitehead 式无点解释的塔斯克几何，来解决这一问题。更准确地说，我们在 lambda-MM 库的基础上，通过在全体论框架上探讨拓扑关系的代数形式化，来形式化塔斯克的实体几何。由于塔斯克的工作根植于 Lesniewski 的全体论，且已知 lambda-MM 目前仅提供塔斯克几何的部分实现，本文的前半部分通过证明全体论类对应于正开集，完成了该框架，使其获得可扩展的单个名称拓扑，可与塔斯克的几何原语相结合。与经典定性逻辑理论方法不同，我们采用一种从全体论和几何子空间中派生完整拓扑空间的方案，从而增加了该理论的表达力。在第二部分，我们展示塔斯克的几何是该拓扑子空间中的一个子空间，其中区域对应于受限类。我们还证明了塔斯克的三个原始公理，简化了其公理体系，并扩展了该理论以包含 T2（Hausdorff）性质和额外定义。