Implications of unprovability of $P\neq NP$ I was reading &quot;Is P Versus NP Formally Independent?&quot; but I got puzzled.
It is widely believed in complexity theory that $\mathsf{P} \neq \mathsf{NP}$. My question is about what if this is not provable (say in $ZFC$). (Let's assume that we only find out that $\mathsf{P} \neq \mathsf{NP}$ is independent from $ZFC$ but no further information about how this is proven.)
What will be the implications of this statement? More specifically,
hardness
Assuming that $\mathsf{P}$ capture the efficient algorithms (Cobham–Edmonds thesis) and $\mathsf{P} \neq \mathsf{NP}$, we prove $\mathsf{NP\text{-}hardness }$ results to imply that they are beyond the present reach of our efficient algorithms. If we prove the separation, $\mathsf{NP\text{-}hardness}$ means that there is no polynomial time algorithm. But what does an $\mathsf{NP\text{-}hardness }$ result mean if the separation is not provable? What will happen to these results?
efficient algorithms
Does unprovability of the separation mean that we need to change our definition of efficient algorithms?
Your question might better be phrased, "How would complexity theory be affected by the discovery of a proof that P = NP is formally independent of some strong axiomatic system?"

It's a little hard to answer this question in the abstract, i.e., in the absence of seeing the details of the proof.  As Aaronson mentions in his paper, proving the independence of P = NP would require radically new ideas, not just about complexity theory, but about how to prove independence statements.  How can we predict the consequences of a radical breakthrough whose shape we currently can't even guess at?

Still, there are a couple of observations we can make.  In the wake of the proof of the independence of the continuum hypothesis from ZFC (and later from ZFC + large cardinals), a sizable number of people have come around to the point of view that the continuum hypothesis is neither true nor false.  We could ask whether people will similarly come to the conclusion that P = NP is "neither true nor false" in the wake of an independence proof (for the sake of argument, let's suppose that P = NP is proved independent of ZFC + any large cardinal axiom).  My guess is not.  Aaronson basically says that he wouldn't.  Goedel's 2nd incompleteness theorem hasn't led anyone that I know of to argue that "ZFC is consistent" is neither true nor false.  P = NP is essentially an arithmetical statement, and most people have strong intuitions that arithmetical statements&mdash;or at least arithmetical statements as simple as "P = NP" is&mdash;must be either true or false.  An independence proof would just be interpreted as saying that we have no way of determining which of P = NP and P $\ne$ NP is the case.

One can also ask whether people would interpret this state of affairs as telling us that there is something "wrong" with our definitions of P and NP.  Perhaps we should then redo the foundations of complexity theory with new definitions that are more tractable to work with?  At this point I think we are in the realm of wild and unfruitful speculation, where we're trying to cross bridges that we haven't gotten to and trying to fix things that ain't broke yet.  Furthermore, it's not even clear that anything would be "broken" in this scenario.  Set theorists are perfectly happy assuming any large cardinal axioms that they find convenient.  Similarly, complexity theorists might also, in this hypothetical future world, be perfectly happy assuming any separation axioms that they believe are true, even though they're provably unprovable.

In short, nothing much follows logically from an independence proof of P = NP.  The face of complexity theory might change radically in the light of such a fantastic breakthrough, but we'll just have to wait and see what the breakthrough looks like.