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

[Alasdair Urquhart]

Tim Chow:

> I think more to the point is that we don't have any reason to believe that
> P != NP is independent of PA.

Well, our collective failure as logicians and CS theorists to make much
of a dent on the main problems of separating complexity classes
has indeed led quite a number of people to surmise independence
as a possibility.

> 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.

That's exactly right, and that is why the result of Ben-David and
Halevi has some traction.  It says that if you succeeded in proving
P != NP unprovable by a standard technique, then something that
nobody believes would follow.  Hence, it seems that making an
attempt along these lines is not likely to be fruitful.

I should add that there has been quite a lot of useful and partially
successful work in proving independence in weak fragments of arithmetic,
some of interest to complexity theorists.  My pessimistic
remarks only have relevance to strong systems like PA.

Alasdair Urquhart