Polynomial time computable arithmetic and conservative extensions
Stephen G. Simpson, Fernando Jorge Inocencio Ferreira · 1988
Samuel Buss' theory S$\sbsp{2}{1}$ is that bounded analog of the theory I$\sum\sbsp{1}{0}$ in which induction for NP-predicates plays the role of induction for recursively enumerable predicates. A new bounded theory, the bounded analog of primitive recursive arithmetic, is defined. In this theory, called PTCA, induction of arithmetic that is used is the language $\{0,1\}$*, as opposed to the natural numbers $\omega$. The provably recursive functions of this theory are characterized and a certain class of thin models is defined, the elements of which do not have end extensions. In a small digression we consider the subtheory of PTCA with induction restricted to strictly rudimentary predicates: it is shown that the complement function is not provably total in this subtheory. By permitting NP-induction on notation we obtain a theory that is $\forall\sum\sbsp{1}{\rm b}$-conservative over PTCA. An intuitionistic version of this new system is studied and, via a realizability argument within a suitable infinitary theory, a question of Buss is partially settled. Finally, second-order theories that are $\forall\sum\sbsp{1}{\rm b}$-conservative over PTCA are introduced. These theories may contain (1) a particular case of the $\Delta\sbsp{1}{0}$-comprehension scheme that implies the existence of NP $\cap$ co-NP sets, (2) weak Konig's lemma for trees in the Meyer-Stockmeyer hierarchy of predicates, and (3) the scheme of bounded collection. It is shown that the Heine-Borel theorem and the uniform continuity theory in the Cantor space 2$\sp{\omega}$ are provable in suitable $\forall\sum\sbsp{1}{\rm b}$-conservative extensions of PTCA. It is argued that the amount of induction necessary to prove the theorem on the existence of a maximum for total continuous functions (with domain and range 2$\sp{\omega}$) is slow induction for NP-predicates.