[FOM] Reflection Principles and Proof Speed-up

[Ilya Tsindlekht]

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.