[FOM] Reflection Principles and Proof Speed-up

[Rob Arthan]

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.

Regards,

Rob.