[FOM] Reflection Principles and Proof Speed-up
Ilya Tsindlekht
eilya497 at 013.net
Fri Jun 8 03:09:11 EDT 2007
On Thu, May 31, 2007 at 07:09:05PM -0400, Richard Heck wrote:
> hendrik at topoi.pooq.com wrote:
> > On Wed, May 30, 2007 at 04:41:25PM +0100, Rob Arthan wrote:
> >
> >> Several people in the mechanized theorem-proving world have proposed reflection
> >> principles as a way of increasing the power of a proof tool. Nuprl for example
> >> has such a rule allowing you to infer P from a theorem asserting that P is provable.
> >>
> > Doesn't this just assert that anything proven inside the system is true?
> > If this is done within the system, doesn't it imply that the system
> > can show its own consistency, and hence is inconsistent?
> >
> > How does it get around this?
> >
> Certainly by L"ob's theorem, if any axiomatic system S (of sufficient
> strength, etc) proves all instances of Bew_S('A') --> A, then S is
> inconsistent. But formulating such a system isn't entirely trivial. Take
> PA. If we add the instances of Bew_{PA}('A') --> A, then we don't have
> PA anymore. So what is needed is going to be some kind of
> diagonalization: We want a system PA* that adds to PA precisely the
> instances of: Bew_{PA*}('A') --> A. I'm sure this can be done, but, as I
> said, it doesn't seem trivial.
>
It seems one can use the same technic as in construction of Goedel's
indecidable statement: take sentence which says 'PA + sentence obtained
from sentence with Goedel number N by substituting N for 'N' proves A ->
A' and then substitute its Goedel number for N.
More information about the FOM
mailing list