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)$
