[FOM] Reflection Principles and Proof Speed-up

[Aatu Koskensilta]

Rob Arthan wrote:
> 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.

Yes. As an example, PA proves of its each finite subtheory that the 
subtheory is consistent, and this is, quite easily, provable in PA, 
using the Haupsatz, for example. So pick a fast-growing function F(x). 
PA proves, for every n, that the theory with axioms of PA of complexity 
< F(n) is consistent. If we allow reflection, and can prove F total, we 
can immediately conclude that the subtheory of PA with axioms of 
complexity < n is consistent. Without reflection we must calculate the 
value of F(n) and carry out a tedious induction, yielding a much longer 
proof.

-- 
Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus