I wouldn't be so sure that P=NP not provable <=> de facto P!=NP.

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

And that would simply "not be a proof". That doesn't disprove my point at all. You have to try harder than that to get one of the funky edge cases.

You're really moving the goalposts here: if it's already proven that P==NP is undecidable (your supposition) then of course you couldn't prove that the algorithm, say, solved arbitrary instances of SAT in time polynomial in their size; such a proof would prove P==NP => contradiction of undecidability of P==NP.

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.

My apologies. I misunderstood your argument. I believe that is a correct example of the "finer slicing" I was referring to.

or - another fun possibility - you could have a provably polynomial-time algorithm that seems to solve SAT, but you can't prove or refute its correctness.

Actually: I think you meant what I'm saying in the earlier version of this comment. But yes: if "P==NP is undecidable" holds then for any provably-polynomial sat-"solver" the following possibilities hold:

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

This comment shows you don't know the definition of the problem. The P?=NP problem is defined in such a way that it is either true or not. P- the set of languages that can be recognized by Deterministic Turing Machine in O(n^k) for some fixed k, n-length of input. NP - the set of languages that can be recognized by NON-Deterministic Turing Machine in O(n^k) for some fixed k, n-length of input.

Your comment shows you don't know much about logic.

No it doesn't! Justify your claim. I just stated the definition of the P?=NP problem. You can find it in any good book on complexity theory. For example:

http://www.amazon.com/Introduction-Theory-Computation-Michae...

I was not refering to your definition of P and NP (which I've just reread and I think it's not good; you want "accept", not "recognize"). I was refering to the fact that you do not make the difference between "true" and "provable", which can be found in any standard introductory book on logic; or, if you prefer a novel, Hofstadter's Goedel, Escher, Bach: an Eternal Golden Braid.

First of all- the definition is not mine. It is what is in the books. The terms "recognize" and "recognizable" is defined in the context of complexity theory. So are the terms "decide" and "decidable". "Accept" is not. So when you say you don't think some definition is good please read the exact definition first. There are many serious and great mathematicians and computer scientist involved in that theory and it is irrespectable to them to comment it without being familiar with it.

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.

Dude, you have no idea what you're talking about. So please stop with the bullshit about great mathematicians and computer scientists when this has nothing to do with them -- only with you -- you cannot accept being wrong. Do your homework first.

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.