[FOM] Reflection Principles and Proof Speed-up

[hendrik@topoi.pooq.com]

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