[FOM] Can invariant of transitive reflexive closure in FOL+PA always been proven?

[Lucas Kruijswijk]

Dear FOMers,

I am collecting material and theorems about FOL + PA, for the case one
want really to do some proving in such system (also for educational 
purposes,
because more advanced systems are often too much for the newbie).

To do some real reasoning (without adding definitions), one needs to have
a pair operator and a transitive reflexive closure. With that one can build 
a lot
and also reason about programs (instead of the higher order fixed point for 
loops
and recursion, one has to rewrite them to closures).

But, I have one problem for which I don't have an answer yet, and I would 
expect
that it is a just a standard result. If one has a closure (with some tricks 
using
prime numbers), then one also want to makes proofs with an invariant of the
closure. However, this is at least not obvious, because at this moment of 
proving
within the FOL + PA system lots of results are not there yet.

I have asked this 15 months ago on MathOverflow without any good answer yet:

http://mathoverflow.net/questions/44007/can-invariant-of-transitive-reflexive-closure-in-folpa-always-been-proven

I gave it a bounty of 50, so, 100 to gain in total,

of couse I could start thinking about it by myself, but again, this should 
be a standard
result to my opinion.

Regards,

Lucas Kruijswijk