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

[Timothy Y. Chow]

Here is a simple observation which is probably not new, but which I have 
not seen explicitly written down anywhere.  Thanks to Andreas Blass for 
sanity-checking the argument.

Recall that P/poly is the non-uniform analogue of P: it is the class of 
Boolean functions computable by polynomial-size Boolean circuits.  It is 
widely believed that

   (*) NP is not contained in P/poly.

Conjecture (*) is a somewhat stronger conjecture than P != NP, but weaker 
than the conjecture that the polynomial hierarchy does not collapse.

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.

To see this, fix some way of encoding SAT instances.  Let n_0(d) be the 
smallest integer n such that no Boolean circuit with n inputs and n^d 
gates correctly solves every instance of SAT (of the appropriate size). If 
there is no such n then n_0(d) is undefined.  Then (*) asserts that n_0 is 
total.

The point is that if (*) is barely true, then n_0 grows very fast.  As 
Andreas puts it, f(n_0(d)) > (n_0(d))^d because the left side is enough 
gates to solve n_0(d)-sized instances of SAT while the right side isn't.  
Then for k = g(d) (and therefore also for k not of this form with just a 
minor change in the estimates) f(k) > k^(n_0^{-1}(k)).  Now if f is just 
barely superpolynomial, then the exponent here, n_0^{-1}(k), must be just 
barely above constant, and so n_0 grows very fast.  If it grows fast 
enough then your favorite formal system won't be able to prove that it is 
total.

Tim