Decidable Formulas of Intuitionistic Primitive Recursive Arithmetic
Abstract
By formalizing some classical facts about provably total
functions of intuitionistic primitive recursive arithmetic
(iPRA), we prove that the set of decidable formulas of iPRA
and of intuitionistic Σ1−induction in the
language of PRA coincides with the set of its provably
Δ1−formulas and coincides with the set of its provably
atomic formulas. By the same methods, we shall give another proof
of a theorem of Markovic and De Jongh: the decidable
formulas of HA are its provably Δ1−formulas.
References
-
Burr, W.; Fragments of Heyting Arithmetic,
Journal of Symbolic Logic 65, N. 3, 2000, 1223-1240.
-
Buss, S.; The Witness Function Method and Provably
Recursive Functions of Peano Arithmetic, "Logic,
Methodology and Philosophy of Science IX", Parwitz, D., etal
(ed); Studies in Logic and the Foundations of Mathematics, Vol. 134,
North-Holland, Amsterdam 1994; 29-68.
-
Damnjanovic; Z.; Minimal Relaizability of Intuitionistic Arithmetic and
Elementary Analysis,
Journal of Symbolic Logic 60, N. 4, 1995, 1208-1241.
- Markovic, Zoran; On the structure of Kripke models of Heyting Arithmetic,
Mathematical Logic Quarterly 39, N. 4, 1993, 531-538.
- Troelstra, Anne S. & van Dalen, D.;
Constructivism in Mathematics. An Introduction, Vol. 1,
Studies in Logic and the Foundations of Mathematics, Vol. 121,
North-Holland, Amsterdam 1988.
- Wehmeier, K.F.; Fragments of HA based on $\Sigma_1$ induction, Archive for
Math. Logic 37, N. 1, 1997, 37-49.