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.
On page 67 there are exercises 1.4.4.
Part one is to show that some axioms of EA (presented on page 53) are provable in PRA. I can't do it with axiom (xv), the others were no problem. Still I think it's probably not difficult.
I also don't know even how to start with part two.
Thanks for your help.
Regards, Ettore
PS: I can't find online a similar axiomatization of PRA like in the book, also I would have to describe the predicate calculus in the style of the book and maybe quote a number of theorems. Thats why I can't provide more details here and refer only to scholars using the book. Sorry about that.
PPS: However...axiom (xv) is $x<y \lor x=y \lor y<x$. You can see what PRA is about for example here: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic Many logic textbooks may have some axiomatization of it as well.
Part two of the exercise is to show that for each quantifier-free formula $A$ (with free variables among $x_1, .., x_n$) in the language of PRA there is an n-ary predicate letter $p$ in the language of PRA such that
$PRA \vdash p (x_1, ..., x_n) \leftrightarrow A[x_1, ... x_n] $ .
It might work somehow with induction on the construction of the formulas.
PPPS: In fact, induction on the construction of the formulas seems to work. I figured a sketch to myself yesterday evening, some details are still unclear to me.
The key is that essentially all formulas are predicates with (propositional) connectives between them.
Hence, for the base case, A being a predicate, you already have the predicate, namely the predicate that is A.
Then, for example, for the conjunction of two formulas one can take the sum of the characteristic functions of the two predicates of the two formulas. For this sum, being a function, one has by definition a predicate, and this predicate suffices for the formula that is the conjunction of the former two formulas.
And so on for other connectives...
The part that is not really doubious, but still in detail not clear to me is the formal system can not only express the sum of two functions but also prove that it is 0 if and only if the other two functions are zero. Similarly it's not fully clear to me how to prove basic properties of the other necessary constructed functions that express some connection of formulas.