# Fragments of HA based on Sigma_1 induction

Archive for Mathematical Logic 37 (1):37-49 (1997)
Abstract
In the first part of this paper we investigate the intuitionistic version \$iI\!\Sigma_1\$ of \$I\!\Sigma_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_1\$ , e.g. 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_1\$ together with induction over arbitrary prenex formulas is \$\Pi_2\$ -conservative over \$iI\!\Pi_2\$ . In the second part of the article we study the relation of \$iI\!\Sigma_1\$ to \$iI\!\Pi_1\$ (in the usual arithmetical language). The situation here is markedly different from the classical case in that \$iI\!\Pi_1\$ and \$iI\!\Sigma_1\$ are mutually incomparable, while \$iI\!\Sigma_1\$ is significantly stronger than \$iI\!\Pi_1\$ as far as provably recursive functions are concerned: All primitive recursive functions can be proved total in \$iI\!\Sigma_1\$ whereas the provably recursive functions of \$iI\!\Pi_1\$ are all majorized by polynomials over \${\Bbb N}\$ . 0 \$iI\!\Pi_1\$ is unusual also in that it lacks closure under Markov's Rule \$\mbox{MR}_{PR}\$
Keywords Legacy
Categories (categorize this paper)
DOI 10.1007/s001530050081
Options
 Save to my reading list Follow the author(s) My bibliography Export citation Find it on Scholar Edit this record Mark as duplicate Revision history Request removal from index

 PhilPapers Archive Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 23,280 External links Setup an account with your affiliations in order to access resources via your University's proxy server Configure custom proxy (use this if your affiliation does not provide a proxy) Through your library Sign in / register to customize your OpenURL resolver.Configure custom resolver
References found in this work BETA

No references found.

Citations of this work BETA
Geoffrey E. Ostrin & Stanley S. Wainer (2005). Elementary Arithmetic. Annals of Pure and Applied Logic 133 (1):275-292.
Helmut Pfeiffer (2001). Archive for Mathematical Logic. Bulletin of Symbolic Logic 7 (4):532.
Similar books and articles
Wolfgang Burr (2000). Fragments of Heyting Arithmetic. Journal of Symbolic Logic 65 (3):1223-1240.
F. John Clendinnen (1966). Induction and Objectivity. Philosophy of Science 33 (3):215-229.

2011-08-02

3 ( #675,209 of 1,932,537 )