[FOM] Reflection Principles and Proof Speed-up

hendrik@topoi.pooq.com hendrik at topoi.pooq.com
Wed May 30 20:30:40 EDT 2007

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?

-- hendrik

More information about the FOM mailing list