<p>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, <strong>if the term $t\overline{n}$ is normalizing</strong>, that computing the normal form $\overline{m}$ can be done by a Turing machine, which is to say that the function $|t|$ is <a href="https://en.wikipedia.org/wiki/%CE%9C-recursive_function" rel="noreferrer">recursive</a> (the terminology is slightly confusing here). This is what is meant by the first paragraph you have quoted.</p>

<p>Furthermore, every fact stated above can be easily proven in $\mathrm{PA}$, <strong>except the normalization of an arbitrary term of system T</strong>. They go on to show that each <em>individual</em> 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)$$</p>

<p>and</p>

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

<p>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.</p>

CC BY-SA 4.0
2018-07-29T22:25:44.677Z
2018-07-29T22:25:44.677Z
cody
<p>In Proof and Types by Girard et alii. Section 7.4.2, I think that the authors want to show that:</p>

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

<p>I don't understand the arguments given to support this thesis.</p>

<blockquote>
  <p>In particular, if t is a closed term of type $Int \to Int$ of <strong>T</strong>, it
  induces a function $|t|:\mathbb{N} \to \mathbb{N}$ defined by:</p>
  
  <p>$|t|(n) = m$ iff $t \overline{n} \leadsto \overline{m}$ $[\ldots]$ </p>
  
  <p>The functions $|t|$ are clearly calculable: the
  normalization algorithm gives $|t|(n)$ as a function of $n$. So those
  functions representable in <strong>T</strong> are recursive. Can we characterize the
  class of such functions?</p>
</blockquote>

<p>This is how I read this parragraph:</p>

<ol>
<li><p>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).</p></li>
<li><p>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.</p></li>
</ol>

<p>The next parragraph seems to confirm this view:</p>

<blockquote>
  <p>$[\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$.</p>
</blockquote>

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

<blockquote>
  <p>Now, what are the mathematical principles necessary to prove the
  reducibility of a fixed term t?</p>
  
  <ul>
  <li><p>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)</p></li>
  <li><p>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).</p></li>
  </ul>
  
  <p>Summing up, the termination is provable in arithmetic: we say that
  $|t|$ is provably total in PA.</p>
</blockquote>

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

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

CC BY-SA 4.0
2018-07-30T04:26:58.730Z
The syntax of $\overline{m}$ is *not* "more complicated". The notation $\overline{m}$ means "numeral $m$", so the statement is that in fact when we normalize $t \overline{n}$ we get a numeral. And this is not a research-level question, it belongs on cs.stackexchange.com.
Andrej Bauer
<lo.logic><type-theory><formal-systems>
Representable functions on System T
user1868607
# Representable functions on System T

(Asked by: username_0 on 2018-07-29)

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

**Tags:** lo.logic, type-theory, formal-systems

> **Comments:**
> **username_1**: The syntax of $\overline{m}$ is *not* "more complicated". The notation $\overline{m}$ means "numeral $m$", so the statement is that in fact when we normalize $t \overline{n}$ we get a numeral. And this is not a research-level question, it belongs on cs.stackexchange.com.  

---

## 1 answers

### Answer by username_2 on 2018-07-29. Score: 7 | Accepted answer

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](https://en.wikipedia.org/wiki/%CE%9C-recursive_function) (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.


---

