基于 Coq 的塔尔斯基的纯粹几何公理化

过去十年间，净数空间推理领域对纯粹几何（mereogeometry）的研究重新获得了关注。纯粹几何 theory 由塔尔斯基（Tarski）提出，基于雷斯尼斯基（Lesniewski）的本体论（mereology）——即关于部分与整体的理论——并拓展引入几何原语和相应定义。然而，大多数方法（i）偏离原始的雷斯尼斯基本体论，其不以常规集合为基础，（ii）将本体论的逻辑能力限制在纯粹的部分-整体关系理论上，（iii）要求引入连接关系。此外，塔尔斯基的经典论文阐述的基础不够清晰，我们认为塔尔斯基所提出的纯粹几何更适合作为延伸雷斯尼斯基整个本体论理论的基础。为此，我们探索一种更贴近雷斯尼斯基原思想、采用 Coq 语言表达的类型论空间表示方法。我们表明：（i）其基础可以更加清晰，（ii）仅需三个公理即可取代四个，（iii）可作为雷斯尼斯基系统完全合规的空间推理基础。