标题： 经典逻辑和直觉主义逻辑：自然演绎中的等价形式，哥德尔-柯尔莫戈罗夫-格利文科翻译 显示英文标题

标题： Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation

摘要： 本报告首先展示了直觉逻辑中几种经典逻辑公式的等价性（排中律，归谬法，皮尔士定律）。 然后建立了哥德尔-柯尔莫戈罗夫翻译的正确性，其命题情况的限制由格利文科提出。 该翻译将一阶逻辑中的公式$F$映射为一个公式$F^{\lnot\lnot}$，使得$F$在经典逻辑中可证明当且仅当$F^{\lnot\lnot}$在直觉逻辑中可证明。 所有形式证明都以自然演绎的形式呈现。 这些问题是众所周知的证明理论事实，但在教科书中常常被忽略或留给读者自行思考。 由于某些所需形式证明的组合难度，我们希望本报告可能有用，尤其是对学生们和其他领域的同事。 显示英文摘要

摘要： This report first shows the equivalence bewteen several formulations of classical logic in intuitionistic logic (tertium non datur, reductio ad absurdum, Pierce's law). Then it establishes the correctness of the G\"odel-Kolmogorov translation, whose restriction to the propositional case is due to Glivenko. This translation maps a formula $F$ of first order logic to a formula $F^{\lnot\lnot}$ in such a way that $F$ is provable in classical logic if and only if $F^{\lnot\lnot}$ is provable in intuitionistic logic. All formal proofs are presented in natural deduction. These questions are well-known proof theoretical facts, but in textbooks, they are often ignored or left to the reader. Because of the combinatorial difficulty of some of the needed formal proofs, we hope that this report may be useful, in particular to students and colleagues from other areas.