[FOM] If "NP is not in P/poly" is barely true, then it is unprovable

[Timothy Y. Chow]

I wrote:

>   (*) NP is not contained in P/poly.
>
>Suppose that (*) is indeed true, but only "barely true," i.e., there 
>exists some function f(n) that is just barely superpolynomial, such that 
>there exist Boolean circuits of size f(n) that correctly solve an 
>NP-complete problem.  Then the promised "simple observation" is that
>(*) is then unprovable.

Scott Aaronson pointed out to me that this observation is made in a 1991
technical report by Ben-David and Halevi, "On the independence of P versus 
NP."  I had heard of this paper before but had never read it.  See

   http://www.cs.technion.ac.il/~shai/ph.ps.gz

or look it up on CiteSeer.  For some strange and annoying reason the pages 
in the electronic version of this paper appear in reverse order.  Anyway, 
if we let PA_1 denote PA augmented with all true Pi^0_1 statements, then 
their Theorem 4 states:

  PA_1 |- "P != NP" if and only if there exists F_alpha for
  alpha < epsilon_0 in the Wainer hierarchy that dominates the
  approximation rate of SAT to P.

Because this is an "if and only if," it provides a partial converse to the 
observation I made.  Roughly speaking, if you have a method for proving 
independence from PA that automatically proves independence from PA_1 as 
well, then your method will succeed on "P != NP" only if "P != NP" is 
barely true.  Or turning it around, if you think that "P != NP" is more 
than barely true and you suspect it is independent of PA, then you'll have 
to come up with an independence proof that doesn't generalize to PA_1.

Tim