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

Lucas Kruijswijk L.B.Kruijswijk at inter.nl.net
Sat Jan 14 15:22:53 EST 2012

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 
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 
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 
that it is a just a standard result. If one has a closure (with some tricks 
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 
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:


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.


Lucas Kruijswijk

More information about the FOM mailing list