Reports on Mathematical Logic

No. 36


Saeed SALEHI:

Decidable formulas of Intuitionistic Primitive Recursive Arithmetic

A b s t r a c t. 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 Markovi\'{c} and \mbox{ De Jongh}: the decidable formulas of $HA$ are its provably $\Delta_1$-formulas.


Back to Main Menu