[FOM] Reflection Principles and Proof Speed-up

[Robert M. Solovay]

>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
In-Reply-To: <465D9B25.1070302 at lemma-one.com>
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
X-Reply-Mbox: INBOX
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
>