Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)

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. If afraid in this case only somebody with the book can help me, since I would have to quote to much of the book here.

This is about the proof of theorem 1.4.7 (i).

It states: $$PRA \vdash Thm_{EA}[\langle \overline{9}, \langle \overline{5}, Num(x), Num (y) \rangle, Num(x+y) \rangle]$$

I think I basically understood the overall frame of the argument, still I have many concerns though and I am quite confused about details.

1) In the statement of the theorem, does he mean to prove it for any natural numbers x and y as metavariables, or are x and y intended to be formal variables available in the system? I would assume the latter, but then, what is $$\overline{x}$$, $$\overline{x+y}$$ etc. supposed to mean? (It occurs everywhere in the proof.) The overline is a $${meta}$$symbol to have an easier writing of numerals of the system, it is not available as a symbol $${in}$$ the system. He seems to mean something like "the numeral of the value that the term that could be placed here instead of the x represents", but what function would that be, and is it expressible $${in}$$ the theory? The overline occurs everywhere, the proof is full of it, it shouldn't be a simple typo..

Accordingly, I don't understand the paragraph on page 70 in between the two formal parts or the paragraph at the end of the proof, page 72, especially the occuring equalities.
For example: "...PRA proves that $$\ulcorner S \overline{y} \urcorner = \ulcorner \overline{Sy} \urcorner$$...i.e. $$Num(Sy)=\langle \ulcorner S \urcorner , Num(y) \rangle$$...

2) When beginning with the (sketch of the) formal proof of the induction step on page 71 he notes the hypothesis $$lh(f(x,y))=l+\overline{1}$$.
Is this a formal hypothesis in PRA (he does not seem to use it formally), or just a meta-assumption?
If the former, then why is there no overline, (and is l a fixed value or a variable of the system)? If the latter, then why is there an overline on 1? If the function lh is prim. rec. shouldn't we be able to acutually compute the value of it, or anyway exactly represent it? When he uses the projection function $$(.)_i$$ to list every derived formula, he writes the argument i as the sum of l and a numeral. Since this is a meta-usage - the formulas aren't really part of the system, they only denote a real formula - why is it written as numeral? He never wrote this argument as numeral before. If for some reason a numeral makes sense, why is there no overall bar, but just on the number, not on the l? To prove his induction step, he doesn't seem to use his induction hypothesis $$Pr_{EA}(\ulcorner \vdash \overline{x}+\overline{y}=\overline{x+y} \urcorner)$$.

He writes "the proof is not complete, we must prove the endless atomic formulas". What does he mean? Aren't the formulas correctly derived?

Thanks for any help,

Regards,

Ettore

PS: I also put it on mathoverflow: https://mathoverflow.net/questions/319409/questions-in-proof-theory-pra-provability-of-ea-theorems-girards-book-from-87

• Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $\overline 0$ is the term naming the number zero. Thus, when we write $\overline 1$ we really mean $S \overline 0$, and so on. – Mauro ALLEGRANZA Nov 29 '18 at 12:30
• Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $\overline n$ is not the number $n$. See page 48 : $\text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $\text {Num}(0)=1$ because the G-number of $\overline 0$ is $1$ (see page 46). – Mauro ALLEGRANZA Nov 29 '18 at 12:47
• on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think. – Ettore Dec 1 '18 at 10:30
• on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles... – Ettore Dec 1 '18 at 10:33
• Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $\ulcorner \overline 0 \urcorner = \ulcorner \overline {\overline 0} \urcorner$ (i.e. $\text {Num} (\overline 0 ) = \ulcorner \overline 0 \urcorner$)." The author defines [page 48] : $\text {Num} (\overline n ) = \ulcorner \overline n \urcorner$. Thus, $\text {Num} (\overline 0 )=1$ and $\text {Num} (\overline 1 ) = \text {Num} (S \overline 0) = < 3, \text {Num} (\overline 0) > = 2^3 \cdot 3^1=8 \cdot 3=24$. But what does it mean $\ulcorner \overline {\overline 0} \urcorner$ ? – Mauro ALLEGRANZA Dec 1 '18 at 11:27