[FOM] Reflection Principles and Proof Speed-up

[Richard Heck]

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.

As for Nuprl, I don't know if it satisfies this condition or not, seeing 
how I'd never heard of it before.

Richard

-- 
==================================================================
Richard G Heck, Jr
Professor of Philosophy
Brown University
http://frege.brown.edu/heck/
==================================================================
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:
http://dudu.dyn.2-h.org/nist/gpg-enigmail-howto