# 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) Reprint years 1998 DOI 10.1007/s001530050081 Options Save to my reading list Follow the author(s) My bibliography Export citation Edit this record Mark as duplicate Request removal from index
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 26,178

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)
References found in this work BETA

No references found.

Citations of this work BETA
Elementary Arithmetic.Geoffrey E. Ostrin & Stanley S. Wainer - 2005 - Annals of Pure and Applied Logic 133 (1):275-292.
Archive for Mathematical Logic.Helmut Pfeiffer - 2001 - Bulletin of Symbolic Logic 7 (4):532.
2003 Annual Meeting of the Association for Symbolic Logic.Andreas Blass - 2004 - Bulletin of Symbolic Logic 10 (1):120-145.
Similar books and articles
On the Induction Schema for Decidable Predicates.Lev D. Beklemishev - 2003 - Journal of Symbolic Logic 68 (1):17-34.
Fragments of Heyting Arithmetic.Wolfgang Burr - 2000 - Journal of Symbolic Logic 65 (3):1223-1240.
Induction and Objectivity.F. John Clendinnen - 1966 - Philosophy of Science 33 (3):215-229.
First Order Common Knowledge Logics.Wolter Frank - 2000 - Studia Logica 65 (2):249-271.
A Note on Finiteness in the Predicative Foundations of Arithmetic.Fernando Ferreira - 1999 - Journal of Philosophical Logic 28 (2):165-174.

2011-08-02

3 ( #687,692 of 2,153,589 )