"this means we have derived a contradiction from the assumption that P≠NP, and thus can conclude that P=NP by the law of the excluded middle". Sadly, P=NP is a statement about physical systems (at least as I see it), and the law of the excluded middle is a property of classical logic, as opposed to constructivist mathematics. The only thing we could conclude is that we compare Apples and Oranges and get jam and that maybe something is wrong in the logical system or the axioms of the mathematics that allows us to conclude an undesired statement, namely P=NP. Anyway, +1

@DavidTonhifer No, P and NP are defined in terms of Turing Machines, which are purely mathematical. They are just sets of strings, and exist independent from any physical model.

Turing Machines are as purely mathematical as a blueprint of your fridge. They ground mathematics in physics. Or at least tell you your mathematics is unconnected to reality when it offers you a way to "hypercomputation".

Also, let's hear it from Scott Aaronson: NP-complete Problems and Physical Reality (PDF)

@DavidTonhofer P and NP are sets, and P=NP means all elements of P are elements of NP, and vice versa. If we disprove P!=NP, it means we prove that the difference between the two sets is empty. Not sure why you think law of excluded middle would not apply. P=NP has nothing to do with physical systems. Yes the mathematics is unconnected to reality (for example, the turing machine model assumes infinite memory). It is still useful.

@kutschkem That's not what I'm saying. P=NP has nothing to do with physical systems, really? I'm waiting for someone to compute the answer to an NP-complete problem in polynomial time. I don't expect this wait to end soon. Further, The "law of the excluded middle" is a property of classical logic, you can throw it overboard with no regret and great gain.

@kutschkem Also, for "Yes the mathematics is unconnected to reality". Not at all. On the contrary, anything positing P=NP is unconnected to reality. As for TM models assuming infinite memory (or even error-free functioning and infinite energy to function), it rarely matters. It's time that is important. PSPACE for example doesn't tell you as much as P, or EXPTIME.

@DavidTonhofer I am not really waiting for that, since I expect P is not equal to NP.

@DavidTonhofer I can compute answers to a finite number of NP-hard problems in polynomial time no problem. P=NP/P!=NP as formulated is a statement about infinite sets and behaviour of things at infinity. As such it never has much to do with physical systems. We think about it in terms of physical systems, sure. But the problem of there being efficient 3-SAT solvers we care about doesn't need to have much to do with P=NP. It's consistent that P!=NP yet all 3-SAT problems smaller than G_64 can be solved by something you think of as a poly time algorithm.

@David Tonhofer "PSPACE for example doesn't tell you as much as P, or EXPTIME." This is simply wrong: PSPACE is a subset of EXPTIME. Knowing that something is PSPACE tells you it's EXPTIME. As for physical reality, the set of $x$ which are solutions to SAT and whose length is greater than $10^{10^{50}}$ is NP-complete, yet we can solve all of its "practical" instances. Aaronson's paper is about solving NP-complete problems with physics, but this does not mean that P=NP is a physical question: you can use integrals to solve physical problems, but integrals exist without physical considerations.

@DavidTonhofer I'm not saying that the definition of a Turing Machine is completely disconnected from reality. Surely P and NP are useful to model physical properties. But a Turing Machine is a computer as much as a blueprint is a fridge, to use your metaphor. You can prove something about the blueprint, and it may or may not translate exactly to the fridge. The point is, P and NP are defined in terms of logic, and P = NP is a logical proposition, so you can phrase it classically or intuitionistically.

@DavidTonhofer To get back to your original point, I acknowledge that Turing Machines are related to physical computers. But that does not imply that logical rules like excluded middle aren't relevant when discussing P vs. NP. For example, we might find that P=NP is equivalent to excluded middle, i.e. that it can only be proved in a non-constructive way.

@Arno there's a difference between "we have" and "there exists". There could exist an algorithm whose description has more symbols than the number of atoms in the universe, but it would be a stretch to say we "have" that algorithm.

@PyRulez - I have added an answer which elucidates that we even know that a specific algorithm with a simple description exists, but that that to complete its description, we'd have to substitute a parameter whose minimum viable value does not easily follow from P=NP, so it does escape our "having it" even if its description is presumably conceptually quite simple. Of course, that simple algorithm may not be optimal for the problem, neither theoretically nor practically.

“each time we have to compose a reduction, the degree of our polynomial is going to get higher and higher” – not necessarily in each step, but probably in most, yes. However. once we have a polynomial algorithm at all, it seems likely enough that people would have a starting point to optimise its exponent, like they have done with other P-problems which at first only had impractically high polynomial degree. Even if the constructive solution is given by lots of small reduction steps, probably most of these wouldn't really be needed but just introduce unnecessary work.

@leftaroundabout - That sounds quite optimistic. Some algorithms need low exponents, others are proven to need a very high exponent. It might not be a coincidence that it's easier to guess a moderately fast algorithm for a problem for which very fast algorithms exist than to devise any polynomial time algorithm for a problem for which an astronomically high exponent is required.

Is there a third possibility, that $P=NP$ is true, but undecidable by the common proof systems?

P=NP nonconstructive is equivalent to P=NP constructive. The upconversion algorithm is well-known.

@Joshua If it's well known, can you link it? And does it run in polynomial time for both positive and negative inputs?

@jmite: en.wikipedia.org/wiki/…

@Joshua, no, they're not equivalent. I think you've misunderstood the consequences of Levin's search. The reasons why Levin's algorithm does not imply what you say are already explained by sdcvvc.