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.

  • 3
    $\begingroup$ 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$. $\endgroup$ – Izaak Meckler Jan 3 at 1:47
  • $\begingroup$ @IzaakMeckler not provably in $\Delta^0_1$, though, from PA's point of view... $\endgroup$ – cody Jan 3 at 15:29
  • $\begingroup$ @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. $\endgroup$ – Andrej Bauer Jan 3 at 17:04
  • $\begingroup$ 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. $\endgroup$ – none Jan 3 at 19:26
  • $\begingroup$ @AndrejBauer You're correct, I'm over-internalizing. Any externally decidable set is $\Delta^0_1$. Seems a little weird though. $\endgroup$ – cody Jan 3 at 22:49

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.


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.