Some weak fragments of HA and certain closure properties
Some weak fragments of HA and certain closure properties
复制标题
HA 的一些弱片段和某些闭合特性
DOI：
10.2178/jsl/1190150031
复制
发表时间：
2002
影响因子：
0.6
通讯作者：
M. Moniri
中科院分区：
文献类型：
--
作者：
Morteza Moniri;M. Moniri
本文证明了直觉开放归纳在DNS（1）规则下是不封闭的。这是通过构建iop +<$Ly（2 y> x）的Kripke模型来建立的，其中Ly（2 y> x）在x上被普遍量化。另一方面，我们证明了iop等价于PA−公理化的直觉理论加上开放公式的弱LNP方案，其中参数的泛量化先于双重否定。我们还证明了对于任何只有y自由的开公式φ（y）. (PA−）i <$Lyφ（y）.我们观察到，理论iop，i 1和i 1在弗里德曼的翻译下被否定公式封闭，因此在VR和IP下也是如此。我们包括一些评论的经典世界中的Kripke模型的IOP。
Abstract We show that Intuitionistic Open Induction iop is not closed under the rule DNS(Ǝ1). This is established by constructing a Kripke model of iop + ¬Ly(2y > x), where Ly(2y > x) is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA− plus the scheme of weak ¬¬ LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula φ(y) having only y free. (PA−)i ⊢ Lyφ(y). We observe that the theories iop, i∀1 and iΠ1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop.