Fragments of HA based on Sigma_1 induction

Archive for Mathematical Logic 37 (1):37-49 (1997)
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
 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
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 28,777
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
References found in this work BETA

No references found.

Add more references

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.

View all 7 citations / Add more citations

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.

Monthly downloads

Added to index


Total downloads

3 ( #704,313 of 2,177,973 )

Recent downloads (6 months)

1 ( #317,205 of 2,177,973 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums