I am trying to understand FOL + PA, better.


With FOL + PA I mean, first order logic, with addition and multiplication predicate and induction axiom scheme.


The book I am reading explains how to construct transitive reflexive closure with these predicates. By encoding the sequence using a prime number, that is larger than any of the numbers in the sequence.


However, it is not directly clear to me, that the invariant of this closure can be derived from the induction axiom scheme (it is also not explained in the book). If there is a predicate R(x,y), one wants to be able to prove that for any $\phi$:


$(\forall x,y:(\phi(x) \land R(x,y)) \to \phi(y)) \to (\forall x,y:(\phi(x) \land R^\*(x,y)) \to \phi(y))$


It is not obvious to me that this is possible. For using induction, you need to number the values in the sequence. However, I doubt if there is already enough prove power to do so.


Does any have resources where this is detailed out? If such invariant is not possible, then FOL + PA constructed this way is crippled. 


Lucas


Edit, here the definition as in the book of John Harrison:


$R^\*(x,y) ::= \exists m, p, Q: primepow(p,Q) \land x < p \land y < p \land$
$(\exists s: m = x + ps) \land$


$(\exists r: r < Q \land m = r + Qy) \land$


$\forall q: q < Q \to primepow(p,q) \to \exists r, a, b, s: m = r + q(a + p(b + ps)) \land r < q \land a < p \land b < p \land R(a,b)$



Can invariant of transitive reflexive closure in FOL+PA always been proven?
The answer can be found here:


<http://www.staff.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf>


Most important part, theorem 1.9 ii.


With this theorem you can have some kind of sequence for which you can prove that the sequence can be extended. This proof is given in PA. With the sequences the remaining part is trivial.


The suggested book Shoenfield's "Mathematical Logic", doesn't provide the answer. It only gives the proof in informal mathematics, but not in PA. Which is required here. The informal mathematics assumes sequences you haven't available yet.


