[FOM] Can invariant of transitive reflexive closure in FOL+PA always been proven?
L.B.Kruijswijk at inter.nl.net
Sat Jan 14 15:22:53 EST 2012
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
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.
More information about the FOM