# System T, System F and arithmetical hierarchy

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.

• If $f \colon \mathrm{Int} \to \mathrm{Bool}$, then we can also of course get the complement of $f$ by negating, and since System T and F are strongly normalizing, this implies the set corresponding to $f$ is computable, so in $\Delta^0_1$. – Izaak Meckler Jan 3 at 1:47
• @IzaakMeckler not provably in $\Delta^0_1$, though, from PA's point of view... – cody Jan 3 at 15:29
• @cody: Hmph? For each particular $f$ there is a proof in $PA$ of the fact that $f$ characterizes a $\Delta_1^0$-predicate. I don't think anyone here suggested that we should understand Izaak's comment as saying "$\mathrm{PA} \vdash \lceil \forall f . f^{-1}(0) \in \Delta_1^0 \rceil$". That's an unusual amount of internalization. – Andrej Bauer Jan 3 at 17:04
• I thought that in System T, functions and functionals were required to be primitive recursive, so Int->Bool would just be the relevant countable subset of $2^\omega$, not the whole set. – none Jan 3 at 19:26
• @AndrejBauer You're correct, I'm over-internalizing. Any externally decidable set is $\Delta^0_1$. Seems a little weird though. – cody Jan 3 at 22:49

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.