[FOM] Reflection Principles and Proof Speed-up
Aatu Koskensilta
aatu.koskensilta at xortec.fi
Wed May 30 19:14:14 EDT 2007
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
More information about the FOM
mailing list