[FOM] Reflection Principles and Proof Speed-up
rda at lemma-one.com
Wed May 30 11:41:25 EDT 2007
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.
I would like to know whether there is a theoretical basis for thinking that
reflection principles can speed up proofs. Specifically, if Pr is a standard
provability predicate in the language of PA, and writing '' for Quine corners,
given a speed-up factor N, are there propositions in the language of PA such
that PA proves Pr('P') by a proof which is N times shorter than any proof of P.
More information about the FOM