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.