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

[Timothy Y. Chow]

Alasdair Urquhart <urquhart at cs.toronto.edu> wrote:
>Their main result is that if you can prove independence of
>"P = NP" using standard techniques involving rate of growth of
>functions, then there is a "very close to polynomial" deterministic
>algorithm for SAT.  Since at the moment, we don't know of any
>other non-Goedelian techniques for proving independence from PA, this 
>appears to me to show that the independence route is not
>currently a fruitful line to follow.

Wait a minute, is this really true?  Hasn't Harvey Friedman, for example, 
exhibited "non-Goedelian" Pi_1 statements that are unprovable in ZFC, and 
thus a fortiori unprovable in PA?  Simply by virtue of being Pi_1, aren't
such statements automatically "immune" to Ben-David and Halevi's result?

I think more to the point is that we don't have any reason to believe that 
P != NP is independent of PA.  If we suspected that NP were barely 
superpolynomial then we would have some reason to suspect that P != NP is 
unprovable, but nobody I know of suspects that.

Tim