Provably recursive functions of constructive and relatively constructive theories (Q964451)

The property that an intuitionistic theory \(T^i\) has the same provably recursive functions as its classical closure \(T^c\) is studied for two groups of theories. The first group includes subsystems of Heyting Arithmetic HA based on induction on formulas in the classes \(E_n\) and \(U_n\) corresponding to the classes \(\Sigma_n\) and \(\Pi_n\) of the classical arithmetical hierarchy. The classes \(E_n\) and \(U_n\) are defined inductively: 1) \(E_0=U_0\) is the set of quantifier-free formulas; 2a) \(U_n\subseteq E_{n+1}\); 2b) if \(A\in E_{n+1}\), then \(\exists x\,A\in E_{n+1}\); 2c) if \(A\) and \(B\) are in \(E_{n+1}\), then \(A\land B\) and \(A\lor B\) are in \(E_{n+1}\); 2d) if \(A\in E_{n+1}\) and \(B\in U_{n+1}\), then \(B\to A\in E_{n+1}\); 3) the definition of the class \(U_{n+1}\) is obtained by interchanging in 2a)--2d) ``\(U\)'' and ``\(E\)'' and replacing \(\exists\) by \(\forall\). The theories \(IU_n^i\) and \(IE_n^i\) are fragments of HA with the induction scheme restricted to \(U_n\) and \(E_n\) formulas, respectively; \(IU_n^c\) and \(IE_n^c\) are their classical versions. In fact, \(IU_n^c\) is \(I\Pi_n\) and \(IE_n^c\) is \(I\Sigma_n\). It is proved that for each \(n\geq 0\) the theories \(I\Sigma_n\) and \(IE_n^i\) have the same \(\Pi_2\)-consequences; therefore these theories have the same provably recursive functions. A method described by \textit{D. Leivant} [``Syntactic translations and provably recursive functions'', J. Symb. Log. 50, 682--688 (1985; Zbl 0593.03038)] and based on the negative translation combined with a variant of Friedman's translation is used. The same method can be applied to show that \(IU_n^i\) and \(IU_n^c\) have the same \(\Pi_2\)-consequences. A similar result is obtained for the relatively constructive theories \(IE_n^{i+\text{PEM}_k}\), where \(\text{PEM}_k\) is the principle of excluded middle for all formulas with at most \(k\) nested quantifiers. The second group of theories consists of the intuitionistic theories of bounded arithmetic \(IS_2^n\) introduced by \textit{V. Harnik} [``Provably total functions of intuitionistic bounded arithmetic'', J. Symb. Log. 57, 466--477 (1992; Zbl 0778.03019)]. In fact, \(IS_2^n\) are intuitionistic versions of Buss's theories \(S_2^n\). Using a general forcing method for establishing \(\Pi_2\)-conservativity for classical theories over their intuitionistic versions proposed by \textit{J. Avigad} [``Interpreting classical theories in constructive ones'', J. Symb. Log. 65, 1785--1812 (2000; Zbl 0981.03061)], the author proves that if \(A\) is a positive \(\Sigma_n^b\)-formula and \(S_2^n\vdash\forall x\,\exists y\,A\) then \(S_2^n\vdash\forall x\,\exists y\,A\). This result is obtained as a corollary of the similar result for the theories \(CPV_n\) and \(IPV_n\) also considered by Harnik.