Decidable Formulas Of Intuitionistic Primitive Recursive Arithmetic
Reports on Mathematical Logic 36 (1):55-61 (2002)
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 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.
Keywords
No keywords specified (fix it)
Categories
(categorize this paper)
PhilPapers/Archive ID
SALDFO
Upload history
Archival date: 2021-02-22
View other versions
View other versions
Added to PP index
2015-02-12
Total views
7 ( #58,122 of 56,903 )
Recent downloads (6 months)
7 ( #52,722 of 56,903 )
2015-02-12
Total views
7 ( #58,122 of 56,903 )
Recent downloads (6 months)
7 ( #52,722 of 56,903 )
How can I increase my downloads?
Downloads since first upload
Sorry, there are not enough data points to plot this chart.
Sorry, there are not enough data points to plot this chart.