A function $f:\mathbb{N}^k\to\mathbb{N}$ is Provably Total in Arithmetical Theory $T$ if there exists a $\Sigma_1$ formula $\phi({\bf x},y)$ in language of $T$ such that:
- $T\vdash \forall {\bf x}\exists!y\phi({\bf x},y)$
- $\mathbb{N}\models \forall{\bf x}\phi({\bf x},f({\bf x}))$.
Def. A set $\mathcal{A}\subseteq \mathbb{N}$ is Provably Decidable in Arithmetical Theory $T$ if $\chi_{\mathcal{A}}$ is provably total in $T$.
Is there any standard name or reference for Provably Decidable sets of Theory $T$?
Thanks.