# [FOM] Reflection Principles and Proof Speed-up

Robert M. Solovay solovay at Math.Berkeley.EDU
Wed May 30 21:01:54 EDT 2007

```>From solovay at math.berkeley.edu Wed May 30 17:42:56 2007
Newsgroups:
Date: Wed, 30 May 2007 17:42:56 -0700 (PDT)
From: "Robert M. Solovay" <solovay at math.berkeley.edu>
X-X-Sender: solovay at blue3
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: [FOM] Reflection Principles and Proof Speed-up
Fcc: sent-mail
Message-ID: <Pine.GSO.4.63.0705301736440.25887 at blue3>
References: <465D9B25.1070302 at lemma-one.com>
X-Reply-UID: (2 > )(1 1173177054 53800)/var/mail/solovay
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

The following example is well-known. I don't know who its due to.

Let J be the stack of twos function. So J(0) = 0; J(n+1) = 2^{J(n)}.

By the usual self-reference trick construct a sentence Phi which asserts
"I have no proof in PA of Godel number less than J(1000)." [Of course, to
make this precise one needs to set up a Godel numbering of PA. But this is
routine.]

The following argument is easily formalizable in PA by a proof of Godel
number less than J(10) [for any reasonable Godel numbering]:

If PA has a proof of Phi of Godel number < J(1000) then of course PA
proves Phi. But if not, this is easily recognized in PA [by inspection!].
This will yield a proof slightly larger in Godel number than J(1001),
Certainly there will be such a proof of Godel number < J(1010). Hence PA
proves Phi.

Next observe that if Phi has a proof in PA of Godel number less
than J(1000) than PA can recognize this and conclude "not Phi". With the
given proof of Phi and the proof just constructed of "not Phi", we would
have an inconsistency in PA. So there is no proof of Phi of Godel number <
J(1000). Any proof of PA is much much larger than the constructed proof of
"PA proves Phi".

All I really used about J is that "PA proves J is a total
recursive function". So, for example, J could be replaced in the above
argument by Ackerman's function.

By a slight massaging of the argument one could get the following:
Let f be a function which is provably total recursive in PA. Then there is
a sentence Phi which is a theorem of PA but letting n and m be the Godel
numbers of the smallest proofs (in PA) of Phi and "PA proves Phi" we have
n > f(m).

--Bob Solovay

On Wed, 30 May 2007, Rob Arthan wrote:

> 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.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
```