On the induction schema for decidable predicates

Abstract

We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, IΔ1. We show that IΔ1 is independent from the set of all true arithmetical II2 sentences. Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also establish some conservation and independence results for parameter free and inference rule forms of Δ1-induction. An open problem formulated by J. Paris (see [4.5]) is whether IΔ1 proves the corresponding least element principle for decidable predicates. LΔ1 (or, equivalently, the Σ1-collection principle В Σ1). We reduce the question to a purely computation-theoretic one.