[FOM] Reflection Principles and Proof Speed-up
Richard Heck
rgheck at brown.edu
Thu May 31 19:09:05 EDT 2007
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
More information about the FOM
mailing list