I think the OP makes great points in his article, but the title of the blog post is wrong. He really speaks of how the scope of P=NP is misconceived by most people.
This being math, one can imagine ever more finely sliced arguments being made, but a "simple" proof that P=NP is forever unsolvable is itself a proof ("the probability that we will find such an algorith is 1 in 10^100"), for all practical and most theoretical (though not all) purposes.
http://www.amazon.com/Introduction-Theory-Computation-Michae...
Second - What I meant to say in my first comment is that the way P?=NP problem is defined it is provable. The fact that it is provable can be proved easily and I will leave this as exercise to you.
Recognizable is not the same thing as acceptable. For example, some undecidable languages are recognizable by Turing machines.
You can leave it as an exercise for anyone you wish, but your assertion (existance of a simple metaproof that there is [a proof of either P=NP or P!=NP]) is false. I base my assertion about your assertion on the fact that about 40 years of research has not produced such a metaproof.
It's at least not obviously inconceivable that one might stumble upon an algorithm for SAT or traveling salesman whose running time on all known inputs appears to be polynomial but for which a proof of its asymptotic running time might prove extremely elusive (in much the same way that so far as we know the riemann hypothesis appears to hold but proof remains elusive).
I was specifically critiquing this assertion:
- since it (P=?NP shown unprovable) proves that you won't ever come up with an algorithm
...which isn't exactly right (you're drawing too strong a conclusion from your supposition): in a "P==NP is undecidable" universe there's nothing (apparently) stopping there being polynomial-time algorithms for NP-complete problems, just a barrier preventing proof that a given algorithm's asymptotic performance puts it in P.
- you'd be able to find a proof it was an invalid "solver" (eg: the algorithm that assigns 'YES' to each of the N variables is provably polynomial and provably incorrect)
- you wouldn't be able to find a proof it was incorrect (in a strong sense: this isn't 'because you aren't clever enough' but b/c you've stumbled upon one of the 'true' polynomial-time algorithms, ergo there can't be a valid proof it's an invalid solver)
I'd guess you couldn't prove that a given polynomial-time algorithm couldn't be shown to be "provably known to be incapable of invalidation"; such a proof => doesn't exist a counterexample (in this case a SAT instance it doesn't get the right answer for), b/c such a counterexample is a refutation => proof the algorithm is correct => contradiction of "P==NP undecidable", but I won't remove the 'I'd guess' from that unless I had a better understanding of the field, as this kind of reasoning is the kind of thing where the technicalities are the important things, and I'm not up to speed on them.
Thus in the "P==NP undecidable" universe if you found a creepy algorithm -- in your example provably-polynomial but not known to be correct or incorrect, but "empirically" correct over a very extended period of time -- you'd know not to waste time trying to prove it correct (b/c such a proof would be obviously impossible) but you'd see every attempt at proving it invalid also fail, like you said.
Edited for clarity. Edited again for correction.
But I agree, the blog isn't about this issue at all.
Statement of the continuum hypothesis: There is no set whose cardinality is strictly between that of the integers and that of the real numbers.
You can provide your argument against the continuum hypothesis. No middle ground? There might not be a polynomial-time algorithm for SAT... but how would we know? You might not be able to prove that one does not exist. The absence of evidence is not the evidence of absence. And we could be eternally locked in this state.
Middle ground exists, for constructivists, those who don't admit the law of the excluded middle (that any statement must be either true or false). And I think most theoretical computer scientists are of this persuasion.
CH is a statement about the existence of an abstract infinite set, so it is not that surprising that its truth depends on your very definition of a set, an elusive object with multiple possible meanings.
On the other hand, P=NP is a statement about boolean formulas, Turing machines and polynomials. None of these are elusive, they are very cleanly defined, trivial concepts. So it's a very well-posed question.
Of course, we could still not be able to prove the (non)existence of a polynomial algorithm for SAT in ZF set theory. In that case, too bad for ZF, but whether P=NP is still a meaningful question.