## 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.