迈向Tarski几何系统的独立版本

在1926-1927年，Tarski为欧几里得几何设计了一组公理，最终形式出现在Schwabhäuser、Szmielew和Tarski于1983年的手稿中。差异在于Tarski和Gupta所做的简化。Gupta提出了Tarski几何系统的一个独立版本，从而确定他的版本在不修改公理的情况下无法进一步简化。为了获得其一个公理（即Pasch公理）的独立性，他证明了其一个推论（即先前被消除的中间性对称性）的独立性。然而，对于Pasch公理的非退化部分，Szczerba为Tarski几何系统的另一个版本提供了一个独立性模型，在该版本中中间性对称性成立。该独立性证明不能直接用于Gupta的版本，因为平行公理的陈述不同。在本文中，我们介绍了在获得Gupta系统变体的独立版本方面的进展。与Gupta的版本相比，我们将Pasch公理拆分为先前被消除的公理及其非退化部分，并更改了平行公理的陈述。我们通过使用Coq证明助手机械化反例模型来验证独立性性质。