Representable functions on System T 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:


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).
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)?
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.