布劳威尔与欧几里得

我们探讨布劳威尔直觉主义数学与欧几里得几何之间的关系。布劳威尔在1949年发表了一篇题为《初等几何的矛盾性》的论文。在该文中，他证明了平行公设的某个经典推论蕴含马尔可夫原理，而他认为该原理在直觉主义上是不可接受的。然而，欧几里得几何作为清晰正确推理的灯塔长达两千年，并非如此轻易就能被抛弃。布劳威尔的出发点是一个不在欧几里得著作中的“定理”，且其证明需要马尔可夫原理。这意味着布劳威尔的论文并未解决欧几里得《几何原本》是否真的需要马尔可夫原理这一问题。在本文中，我们证明存在一个自洽的“非马尔可夫欧几里得几何”理论。我们相当详细地展示了我们的理论是（至少）欧几里得第一卷的恰当形式化表述，并且足以定义几何算术，从而改进了作者先前的研究（那些研究将马尔可夫原理作为一条公理）。从哲学上讲，如果人们认为布劳威尔出发点的几何“相交定理”在几何上是显然的，那么布劳威尔关于其平行公设版本蕴含马尔可夫原理的证明，同样可以被解读为支持马尔可夫原理为真的几何证据。