A function $f:\mathbb{N}^k\to\mathbb{N}$ is Provably Total in Arithmetical recursively enumerable first order Theory $T$ if there exists a $\Sigma_1$ formula $\phi({\bf x},y)$ in language of $T$ such that:

1. $T\vdash \forall {\bf x}\exists!y\phi({\bf x},y)$
2. $\mathbb{N}\models \forall{\bf x}\phi({\bf x},f({\bf x}))$.

(Suppose $\mathbb{N}\models T$.)

Def. A set $\mathcal{A}\subseteq \mathbb{N}$ is Provably Decidable in Arithmetical recursively enumerable first order 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.

A function $f:\mathbb{N}^k\to\mathbb{N}$ is Provably Total in Arithmetical recursively enumerable Theory $T$ if there exists a $\Sigma_1$ formula $\phi({\bf x},y)$ in language of $T$ such that:

1. $T\vdash \forall {\bf x}\exists!y\phi({\bf x},y)$
2. $\mathbb{N}\models \forall{\bf x}\phi({\bf x},f({\bf x}))$.

(Suppose $\mathbb{N}\models T$.)

Def. A set $\mathcal{A}\subseteq \mathbb{N}$ is Provably Decidable in Arithmetical recursively enumerable 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.

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:

1. $T\vdash \forall {\bf x}\exists!y\phi({\bf x},y)$
2. $\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.

A function $f:\mathbb{N}^k\to\mathbb{N}$ is Provably Total in Arithmetical recursively enumerable first order Theory $T$ if there exists a $\Sigma_1$ formula $\phi({\bf x},y)$ in language of $T$ such that:

1. $T\vdash \forall {\bf x}\exists!y\phi({\bf x},y)$
2. $\mathbb{N}\models \forall{\bf x}\phi({\bf x},f({\bf x}))$.

(Suppose $\mathbb{N}\models T$.)

Def. A set $\mathcal{A}\subseteq \mathbb{N}$ is Provably Decidable in Arithmetical recursively enumerable first order 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.