Abbreviating proofs using metamathematical rules
Petr Hájek, Franco Montagna, Pavel Pudlá · 1993
Abstract There are examples of sentences which are provable in theory T but which have only very long proofs. All the known examples have the property that at the same time there is a simple meta mathematical argument which shows that they are provable; thus, they have short proofs in some stronger theory whose soundness is as acceptable as the soundness of the original one. Such a phenomenon, which one calls speed up by provability, was first studied by Parikh. He proved in [Par71] that, if T is a recursively enumerable extension of Peano Arithmetic PA, then there is a sentence φ such that the formalization of “ φ is provable in T” has a much shorter proof than φ. This result is generalized in [DM89] and in (Mon90].