I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.
As I understand, they might be not ideally phrased, but I don't know what should be changed, or I don't see a good possibility to rewrite them. If you miss some background information, I will try to provide it.
If it would cost too much time, maybe you like to leave hints for (better/more detailed) solutions or general, short descriptions how the solution 'looks like'.
In future I'll try to write in a way that can more easily be answered. Of course nobody should feel forced to answer, in the past it seemed people sometimes feel that way, to my surprise.
Here's a copy:
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
