Fragments of Heyting Arithmetic
Burr, Wolfgang
J. Symbolic Logic, Tome 65 (2000) no. 1, p. 1223-1240 / Harvested from Project Euclid
We define classes $\Phi_n$ of formulae of first-order arithmetic with the following properties: (i) Every $\varphi \in \Phi_n$ is classically equivalent to a $\Pi_n$-formula (n $\neq$ 1, $\Phi_1 :=\Sigma_1)$. (ii) $\bigcup_{n\in \omega} \Phi_n = \mathscr L_A$. (iii) $I\Pi_n$ and $i\Phi_n$ (i.e., Heyting arithmetic with induction schema restricted to $\Phi_n$- formulae) prove the same $\Pi_2$-formulae. We further generalize a result by Visser and Wehmeier, namely that prenex induction within intuitionistic arithmetic is rather weak: After closing $\Phi_n$ both under existential and universal quantification (we call these classes $\Theta_n$) the corresponding theories i$\Theta_n$ still prove the same $\Pi_2$-formulae. In a second part we consider i$\Delta_0$ plus collection-principles. We show that both the provably recursive functions and the provably total functions of $i\Delta_0 + \{\forall x \leq a \exists y \varphi(x,y) \rightarrow \exists z \forall x \leq a \exists y \leq z \varphi(x,y) \mid \varphi \in \mathscr L_A\}$ are polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence $i\Delta_0 + \{B\varphi, C\varphi \mid \varphi \in \mathscr L_A\} \vdash PA$.
Publié le : 2000-09-14
Classification: 
@article{1183746179,
     author = {Burr, Wolfgang},
     title = {Fragments of Heyting Arithmetic},
     journal = {J. Symbolic Logic},
     volume = {65},
     number = {1},
     year = {2000},
     pages = { 1223-1240},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183746179}
}
Burr, Wolfgang. Fragments of Heyting Arithmetic. J. Symbolic Logic, Tome 65 (2000) no. 1, pp.  1223-1240. http://gdmltest.u-ga.fr/item/1183746179/