论文标题
在某些建设性的谓词微积分上
On certain constructive predicate calculus
论文作者
论文摘要
建设性算术或马尔可夫算术ma是通过添加以下两个原则从直觉算术算法获得的：将建构主义与直觉主义区分开的马尔可夫原理m和所谓的扩展教会论文，从而将建设性语义与经典语言区分开来。第一个原理由谓词公式表示，但在算术语言中将ECT作为方案提出。作者的一些较早结果使得通过纯谓词公式替换方案ECT。这给出了一个谓词计算MQC，可以作为建设性算术的逻辑基础。也就是说，基于MQC和Peano Axioms的算术理论证明了所有公式在MA中可推论。请注意，MQC不是直觉和经典逻辑之间的中间积分：它证明了某些在经典谓词计算中不可推断的公式。 参考书目：12个项目。
Constructive arithmetic, or the Markov arithmetic MA, is obtained from intuitionistic arithmetic HA by adding the following two principles: the Markov principle M which distinguishes constructivism from intuitionism, and the so-called extended Church thesis ECT, which distinguishes constructive semantics from classical semantics. The first principle is expressed by a predicate formula, but ECT is formulated as a scheme in the arithmetical language. Some earlier results of the authors make possible to replace the scheme ECT by a pure predicate formula. This gives a predicate calculus MQC which can serve as a logical basis for constructive arithmetic. Namely, arithmetical theory based on MQC and Peano axioms proves all formulas deducible in MA. Note that MQC is not an intermediate calculus between intuitionistic and classical logics: it proves some formulas that are not deducible in the classical predicate calculus. Bibliography: 12 items.
