Representable functions on System T

Question

In Proof and Types by Girard et alii. Section 7.4.2, I think that the authors want to show that:

(1) The set of functions definable in System T coincides with the set of recursive functions whose termination is provable in Peano arithmetic

I don't understand the arguments given to support this thesis.

In particular, if t is a closed term of type $Int \to Int$ of T, it induces a function $|t|:\mathbb{N} \to \mathbb{N}$ defined by:

$|t|(n) = m$ iff $t \overline{n} \leadsto \overline{m}$ $[\ldots]$

The functions $|t|$ are clearly calculable: the normalization algorithm gives $|t|(n)$ as a function of $n$. So those functions representable in T are recursive. Can we characterize the class of such functions?

This is how I read this parragraph:

1. Regarding calculability of $|t|$: using the iff one computes $|t|(n)$ by computing $t \overline{n} \leadsto \overline{m}$. Then $\overline{m}$ syntax can be more complex that an integer and in order to obtain $m$ one has to rewrite it into a normal form (which should be an integer by the term's type).

2. Regarding recursivity: I believe that they stress that the normalization begins with term $t \overline{n}$ and thus $|t|$ is indirectly "recursive" in its argument.

The next parragraph seems to confirm this view:

$[\ldots]$ Seen as a partial algorithm, $|t|$ amounts to looking for the normal form, and, in the case where this succeeds, writing it. The normalization theorem is thus a proof of program guaranteeing termination of all algorithms obtained from $T$.

From here I get the idea that every function written in $T$ is terminating. The next parragraph comes as a surprise though:

Now, what are the mathematical principles necessary to prove the reducibility of a fixed term t?

• to be able to express the reducibility of t and of its subterms: one must be able to write a finite number of reducibilities, which can be done in Peano arithmetic (PA)

• to be able to reason by mathematical induction on this finite number of reduciblity predicates; that can again be done in PA, modulo some awful coding without significant interest (Godel numbering).

Summing up, the termination is provable in arithmetic: we say that $|t|$ is provably total in PA.

If every function was terminating in System T why would one want to prove in PA specifically?

My question is if you can solve the doubts I presented or if you have your own way of showing statement (1)?

Answer 1

If every term in system T terminates, then $t\overline{n}\leadsto\overline{m}$ for every numeral $n$, and it is easy to show that a normal form $\overline{m}$ in the empty context is a numeral as well (and cannot be more complex!). In addition, it is easy to show, if the term $t\overline{n}$ is normalizing, that computing the normal form $\overline{m}$ can be done by a Turing machine, which is to say that the function $|t|$ is recursive (the terminology is slightly confusing here). This is what is meant by the first paragraph you have quoted.

Furthermore, every fact stated above can be easily proven in $\mathrm{PA}$, except the normalization of an arbitrary term of system T. They go on to show that each individual term $t$ can be shown to be normalizing in $\mathrm{PA}$ wich they suggest implies that every term $t$ defines a function in $\mathrm{PA}$: for every term $t:\mathrm{Int}\rightarrow\mathrm{Int}$, there is a proposition $\phi_t(x,y)$ such that $$\mathrm{PA}\vdash \forall x\exists! y\phi_t(x,y)$$

and

$$\mathrm{PA}\vdash\phi_t(\overline{n},\overline{m})$$ iff $$|t|(n)=m$$

As the following pages explain, the other direction is provable as well, that is to every $\phi$ with the first property, there is some term $t$ in system T that corresponds to it.