Fragments of HA based on \(\Sigma_ 1\)-induction
type: Item
instance of: scholarly article
title: Fragments of HA based on \(\Sigma_ 1\)-induction
zbMATH Open document ID: 0886.03040
published in: Archive for Mathematical Logic
publication date: 1996-09-25T00:00:00Z
review text: 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. 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 arithmetic 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 considered: 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 \(\mathbb{N}\). \(iI \Pi_1\) is unusual also in that it lacks closure under Markov's Rule \(\text{MR}_{PR}\).
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03D20
zbMATH DE Number: 918721
zbMATH Keywords: Kleene's recursive realizability
zbMATH Keywords: primitive recursive choice functions
zbMATH Keywords: quantifier alternation
zbMATH Keywords: prenex formulas
zbMATH Keywords: provably recursive functions
zbMATH Keywords: primitive recursive functions
author: Kai Frederick Wehmeier
MaRDI profile type: Publication
full work available at URL: s001530050081
OpenAlex ID: W2050152670
DOI: 10.1007/S001530050081
description: scientific article; zbMATH DE number 918721