Decidable Formulas Of Intuitionistic Primitive Recursive Arithmetic

Reports on Mathematical Logic 36 (1):55-61 (2002)
  Copy   BIBTEX


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Σ1+ (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 Marković and De Jongh: the decidable formulas of HA are its provably ∆1-formulas.

Author's Profile

Saeed Salehi
University of Tabriz


Added to PP

151 (#79,832)

6 months
55 (#78,705)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?