论各种否定翻译

在过去一个世纪中，文献中提出了多种将经典数学翻译为直觉主义数学的证明翻译。这些翻译通常被称为否定翻译或双重否定翻译。其中，最常被引用的是Kolmogorov、Gödel、Gentzen、Kuroda和Krivine的翻译（按时间顺序）。在本文中，我们提出了一个框架来解释这些不同翻译之间的相互关系。更准确地说，我们从Kolmogorov翻译出发，定义了一种（模块化）简化的概念，这导致了不同否定翻译之间的偏序关系。在这个推导出的序关系中，Kuroda和Krivine是最小元素。我们引入了两种新的最小翻译，而Gödel和Gentzen翻译则位于Kolmogorov翻译与其中一种新翻译之间。