Total computable function

A total computable function is a computable function whose domain contains every allowed input.

For a theory of arithmetic $T$ and a program index $e$, the function ${\phi }_e$ is provably total in $T$ when $T$ proves its canonical totality sentenceIf $T$ is recursively axiomatized, the indices of its provably total functions form a computably enumerable set.