## Can invariant of transitive reflexive closure in FOL+PA always been proven?

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) ∧ R(x,y)) \to \phi(y)) \to (\forall x,y:(\phi(x) ∧ 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) ∧ x < p ∧ y < p ∧$ $(\exists s: m = x + ps) ∧$

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

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

-
 To clarify, is the displayed formula missing some quantifiers? Also, by FOL+PA do you just mean the usual Peano Arithmetic? – Bjørn Kjos-Hanssen Oct 28 2010 at 20:16 I'm sorry, I do not understand. What is $R^*$? Also, what is the invariant (or invariance?) you mention? I also have Bjørn's question about whether this is PA or something else. Do you have definitional axioms for addition and multiplication, or only the symbols? Do you have a symbol for 0? A symbol for successor? Do you have axioms for them? Can you please explain better what is the encoding you refer to in paragraph 3? – Andres Caicedo Oct 28 2010 at 20:26 Well, I don't know what answer you expect, but yes, it seems quite clear that you can do it. As a good heuristic you can imagine that you're allowed to manipulate finite objects (finite lists of numbers, finite sets of finite lists of numbers, etc.) Then you can show the desired conclusion by induction on the length of the sequence that witnesses $R^{*}(x,y)$. – Andrej Bauer Oct 28 2010 at 20:27 Is $R^*$ the transitive closure of $R$? (If yes, and you really mean Peano Arithmetic, the answer is yes, as mentioned by Andrej.) – Andres Caicedo Oct 28 2010 at 20:31 I added the quantifiers. For FOL + PA, you have a 0, a successor operator, an addition function and multiplication function. And the normal axioms for them. For the $R^*$ I use the definition given in a book from John Harrison (the creator of HOL-Light). Page 536 of his book automated reasoning. – Lucas K. Oct 28 2010 at 20:31

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.

-