Decidable formulas of intuitionistic primitive recursive arithmetic

• Autorzy: Salehi S.
• Języki publikacji: EN

Abstrakty

EN

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 i\Sigma_1^+ (intuitionistic \Sigma_1-induction in the language of PRA) coincides with the set of its provably \Delta_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 Delta 1-formulas.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2002
• Tom: No. 36
• Strony: 55--61
• Opis fizyczny: Bibliogr. 6 poz.

Twórcy

autor

Salehi S.

• Institute of Mathematics Polsh Academy of Sciences ul. Śniadeckich 8 P.O. Box 137 00-950 Warsaw, Poland,

Bibliografia

• [1] W. Burr, Fragments of Heyting Arithmetic, Journal of Symbolic Logic 65, N. 3, 2000, pp. 1223-1240.
• [2] S. Buss, The Witness Function Method and Provably Recursive Functions of Peano Arithmetic, ”Logic, Methodology and Philosophy of Science IX”, Parwitz, D., et al. (ed); Studies in Logic and the Foundations of Mathematics, Vol. 134, North-Holland, Amsterdam 1994; pp. 29-68.
• [3] Z. Damnjanovic, Minimal Relaizability of Intuitionistic Arithmetic and Elementary Analysis, Journal of Symbolic Logic 60, N. 4, 1995, pp. 1208-1241.
• [4] Z. Marković, On the structure of Kripke models of Heyting Arithmetic. Mathematical Logic Quarterly 39 (1993), 531–538.
• [5] A.S. Troelstra and D. van Dalen Constructivism in Mathematics. An Introduction, Vol. 1. Studies in Logic and the Foundations of Mathematics, Vol. 121, NorthHolland, Amsterdam 1988.
• [6] K. F. Wehmeier, Fragments of HA based on Σ1 induction. Archive for Math. Logic 37 (1997), 37-49.