Fragments of $HA$ based on $\Sigma_1$-induction
Fragments of
$HA$ based on
$\Sigma_1$-induction
复制标题
基于 $Sigma_1$ 归纳的 $HA$ 片段
DOI：
10.1007/s001530050081
复制
发表时间：
1997
影响因子：
0.3
通讯作者：
K. Wehmeier
中科院分区：
文献类型：
--
作者：
K. Wehmeier
抽象。本文的第一部分利用Kleene的递归可实现性技术研究了I SIGMA [sub 1]的直觉版本iI SIGMA [sub 1]（PRA语言）。我们的处理与HA的通常处理非常相似，并为iI SIGMA [sub 1]建立了一些很好的性质，例如原始递归选择函数的存在性（这在[D94]中也通过不同的方法建立）。然后，我们锐化Visser的一个未发表的定理，其效果是，量词交替单独是不太强大的直觉比经典的：iI SIGMA [sub 1]连同归纳在任意前束公式是PI [sub 2]-保守的iI PI [sub 2]。在文章的第二部分中，我们研究了iI SIGMA [sub 1]与iI PI [sub 1]的关系（在通常的算术语言中）。这里的情况与经典的情况明显不同，因为iI PI [sub 1]和iI SIGMA [sub 1]相互不可比，而就可证明递归函数而言，iI SIGMA [sub 1]明显强于iI PI [sub 1]：所有的原始递归函数都可以证明在iI SIGMA [sub 1]中是全的，而iI PI [sub 1]的可证递归函数都可以被N上的多项式优化。PI [sub 1]也是不寻常的，因为它在马尔可夫规则MR [sub PR]下缺乏封闭性。
Abstract. In the first part of this paper we investigate the intuitionistic version iI SIGMA [sub 1] of I SIGMA [sub 1](in the language of PRA), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for HA and establishes a number of nice properties for iI SIGMA [sub 1], eg existence of primitive recursive choice functions (this is established by different means also in [D94]). We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is much less powerful intuitionistically than classically: iI SIGMA [sub 1] together with induction over arbitrary prenex formulas is PI [sub 2]-conservative over iI PI [sub 2]. In the second part of the article we study the relation of iI SIGMA [sub 1] to iI PI [sub 1](in the usual arithmetical language). The situation here is markedly different from the classical case in that iI PI [sub 1] and iI SIGMA [sub 1] are mutually incomparable, while iI SIGMA [sub 1] is significantly stronger than iI PI [sub 1] as far as provably recursive functions are concerned: All primitive recursive functions can be proved total in iI SIGMA [sub 1] whereas the provably recursive functions of iI PI [sub 1] are all majorized by polynomials over N. iI PI [sub 1] is unusual also in that it lacks closure under Markov's Rule MR [sub PR].