# 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: 28,777

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
Quick Cut-Elimination for Strictly Positive Cuts.Toshiyasu Arai - 2011 - Annals of Pure and Applied Logic 162 (10):807-815.
Elementary Arithmetic.Geoffrey E. Ostrin & Stanley S. Wainer - 2005 - Annals of Pure and Applied Logic 133 (1):275-292.
Homomorphisms and Chains of Kripke Models.Morteza Moniri & Mostafa Zaare - 2011 - Archive for Mathematical Logic 50 (3-4):431-443.
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 ( #704,313 of 2,177,973 )