Questions in proof theory (Definition of an interpretation of one theory in another, Girards Book from '87)

Question

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, clarify things when I can't work out the sense/meaning or help with the understanding of the proofs.

This is about definition 1.4.5.

I think I basically got this, still I wonder whether there is some 'nicer' reformulation. I find this to be a bit jolty, bulging or clumsy.

Also a few simple examples/applications of this definition (in the language/style of the book) would help me getting the essence of it.

Thanks for your help,

Regards, Ettore

Answer 1

Long comment

There is the $\text {L}_0$ language of arithmetic with function symbols : $s,+,\cdot$ and (binary) relation symbols : $=,<$.

There is the $\text {EA}$ theory of elementary arithmetic based on the previous language with suitable axioms.

Then there is the $\text {PRA}$ theory of primitive recursive arithmetic with a different language : $\text {L}_{pr}$.

$\text {L}_{pr}$ ahs many function symbols: one for each primitive recursive function, like e.g. the remainder of division.

The gist of Def.1.4.5 is to find a way to "mimick" in a theory $\text T$ based on the language $\text {L}_0$ the functions of $\text {PRA}$.

Due to the fact that $\text {L}_0$ has only the "basic" arithmetical functions : $s,+,\cdot$, to express a $\text {PRA}$ function $f$ means to find a suitable formula $A$ such that :

$\text T \vdash A(x,y,z) \text { iff } f(x,y)=z$ holds in $\text {PRA}$.

---

A very simple example, is the way to define $<$ in Peano first-order arithmetic :

$n < m \text { iff } \exists k \ (m=n+s(k))$.