[FOM] Reflection Principles and Proof Speed-up
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?
More information about the FOM