A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
复制标题
经典算术与直觉算术的保守性定理的推广
DOI：
10.1002/malq.200310074
复制
发表时间：
2004
影响因子：
0.3
通讯作者：
S. Berardi
中科院分区：
文献类型：
--
作者：
S. Berardi
直觉主义的一个基本结果是保守性。以经典算术中的某个命题（某个算术命题<$x.<$y.P（x，y），其中P是可判定的）的任何证明p为例。然后我们可以有效地在同一陈述的某些直观证明中翻转p。在文献[1]中，我们推广了这个结果：算术命题P = x，y，P（x，y）的任何经典证明，当P为k次时，可以有效地转化为同一命题的某些证明，只在k次上使用排除中间公式。当k = 0时，作为特例得到了原来的保守性结果。这个结果是语义结构的副产品。卡耐基梅隆大学的J. Avigad，用H.弗里德曼的A翻译他的证明在他的许可下被包括在这里。（© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA，魏因海姆）
A basic result in intuitionism is Π02‐conservativity. Take any proof p in classical arithmetic of some Π02‐statement (some arithmetical statement ∀x.∃y.P(x, y), with P decidable). Then we may effectively turn p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof p of an arithmetical statement ∀x.∃y.P(x, y), with P of degree k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree k formulas. When k = 0, we get the original conservativity result as particular case. This result was a by‐product of a semantical construction. J. Avigad of Carnegie Mellon University, found a short, direct syntactical derivation of the same result, using H. Friedman's A‐translation. His proof is included here with his permission. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)