Does P equal NP? This is not an answer.

A preprint by Sten-Åke Tärnlund, purporting to prove that P≠NP, is making its rounds on the internets. I noticed it through a blog post by Bruce Schneier; he quite sensibly notes that "these sorts of papers make the rounds regularly, and [Schneier's] advice is to not pay attention to any of them."

Still, someone has to try to pick such papers apart, if only to make sure that they are as worthless as statistics suggest. I'll volunteer for this one. (This mini-review was originally intended to be a comment to Schneier's posting, but grew a bit too large for that. Also, I want to use markup that plain-text comments cannot contain).

It is not easy to figure out what the author is getting at, because the paper is pithy to the point of sloppiness. Take, for example:

Definition 8 p(a) for c·|a|^q some c q ∈ N any a ∈ L.

By comparison with other similarly terse definitions, this apparently means

Definition 8. Let p(a) abbreviate c·|a|^q for some c and q in N, and any list a.

But what are the scope of the quantifiers on c and q? Are they constant throughout the paper or can they depend on something? What can they depend on? It makes no sense in context to let them depend on a ... Complexity theory has no lenity for those who fail to be rigorous about order and scope of quantifiers.

Formally, the paper begins to go wrong no later than Definition 13, where T(s,a,u) is defined to mean something that involve the "truth" symbol ⊨ (or |= if your font, like mine, has no native Unicode glyph for this symbol), which is not in the language of B – but in the remainder of the paper T(s,a,u) is treated as if it was a formula of B, and bogosity ensues.

Of course, a formal error does not mean that the idea behind the paper is flawed. But it does not bode well – one would think that an author who is smart enough to solve an open problem as famous and long-standing as this would be more careful. Indeed, a true flaw shows up:

As far as I understand it, the main argument in the paper goes somewhat like this: Assume that you give me a Turing machine that purports to solve SAT (i.e., decide whether a propositional formula is a tautology) in polynomial time. Then I'll try to run a sufficiently large "pigeonhole formula" PF_m through your machine. I already know that this formula is a tautology, but if your machine tells me that in polynomial time, I can extract a short proof of the formula from what the machine does. This contradicts a theorem by Haken which says that proofs (in a certain restricted form) of the pigeonhole formula are always long. Therefore, your machine either does not solve SAT or does not do it in polynomial time.

What first meets the eye here is that the paper appears to redefine SAT. The SAT we all know and love is about propositional formulas (i.e., expressions built from Boolean variables and the Boolean operators not, and, or and so forth). However, PF_m which the paper tries to use the SAT solver on is not propositional. It is defined only informally here, but for it to have any relation to Haken's theorem, it needs to contain non-Boolean variables and equality operators. Those belong to predicate calculus, not propositional logic. However, this is not in itself damning, because satisfiability in the pure first-order theory of equality is easily seen to be in NP. A valid proof that this is outside P would also solve the P=NP question.

Correction (2008-11-09): It turns out that there are indeed purely propositional formalizations of the pigeonhole principle, and the paper must be referring to one of those. I had in mind a formula such as "(a=1 or a=2) and (b=1 or b=2) and (c=1 or c=2) implies a=b or a=c or b=c". What I did not notice (and, in my defence, the paper never writes out an example of its PF_m) was that we can just expand, say, "a=b" to "(a=1 and b=1) or (a=2 and b=2)", in which case we can take things like b=2 as propositional variables.

The true fallacy here, however, is the tacit assumption (partly concealed as Definitions 13 and 14) that if we have a Turing machine that recognizes tautologies, then a short proof that this machine answers yes for a given formula corresponds to a short proof that the formula is indeed a tautology. But this is not necessarily true; it is at least conceivable that there is a fast Turing machine that recognizes tautologies but that we cannot prove that this is what it does. In that case, a trace of the Turing machine's action does not correspond to any proof that the formula is a tautology, much less a short one. And even if the machine provably recognizes tautologies, we cannot necessarily extract a short proof in a particular formalism from a short run of the machine.

There is various additional smoke and mirrors, including the central proposition which is stated thus:

Theorem 1 SAT ∉ P is true in a simply consistent extension B' of theory B.

Does this mean simply that there is some consistent extension of B in which SAT is not in P, or that SAT∉P is true in every consistent extension of B? I cannot tell. In the former case, the proposition says nothing about the standard model for B (i.e. Turing machines modeled with the standard integers, which are not necessarily a model for the extension). In the latter case, why bother speaking about extensions in the first place?

In conclusion, Schneier is right, and this can safely be ignored.