I refer to Proof and Types by Jean-Yves Girard for the definition of System T (pag. 46) and System F (pag. 81).
In this treatise there are two base types, i. e. $\text{Int}$ (natural numbers) and $\text{Bool}$ (booleans), so I suppose that the type $\text{Int} \rightarrow \text{Bool}$ can be seen as **set of natural numbers**. This gives me a curiosity: what is the position of the sets of System T in the arithmetical hierarchy? and about the sets of System F?
I searched in the literature, but I didn't find anything.

Oh, thank you Izaak.

So $\Delta_0^0 \subsetneq T$ and $\Delta_0^0 \subsetneq F$ because in $T$ and in $F$ there are Sudan function, Ackermann function and so on; but $T \subsetneq \Delta_1^0$ and $F \subsetneq \Delta_1^0$ because all the functions in $T$ (or in $F$) are computable and total and by diagonalization it is possible to build a function total, computable, not in $T$ (or in $F$).

Only now I realize how much $\Delta_1^0$ is not constructive.

provablyin $\Delta^0_1$, though, from PA's point of view... $\endgroup$ – cody Jan 3 at 15:29externallydecidable set is $\Delta^0_1$. Seems a little weird though. $\endgroup$ – cody Jan 3 at 22:49