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:

By comparison with other similarly terse definitions, this apparently meansDefinition 8p(a) for c·|a|^{q}some c q ∈ N any a ∈ L.

But what are the scope of the quantifiers onDefinition 8.Letp(a)abbreviatec·|a|for some^{q}candqinN, and any lista.

*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:

Does this mean simply that there is some consistent extension ofTheorem 1SAT ∉ P is true in a simply consistent extensionB'of theoryB.

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

If your comments on the preprint by Sten-Åke Tärnlund is a joke then, please, ignore our remark.

ReplyDeleteBut if you just got lost, we shall try to help you to start over.

First, take a good look at the formulas of theory B, then it should be clear why

theorem 1 mentions the simply consistent extension B', introduced in definition 15.

Yes, that's right SAT ∉ P is in B', but not in B. For the Turing machines in the set U

B' is simply consistent by corollary 2. Thus there is, if you don't mind, an intended model for B'.

Unfortunately, this contradicts your comment that this model is: not necessarily a model for the extension.

Second, you are right there is a true fallacy here. Your statement: there is a fast Turing machine that recognizes tautologies

but that we cannot prove that this is what it does. Of course, there is no such machine in theory B. Just take a good look at

axiom 1, and definition 5, 13 and 14.

So much for what you call the main argument of the paper.

Third, unfortunately, you are plying a bit dirty for our taste.

You claim that

(i) : the paper appears to redefine SAT.

This is of course wrong, see definition 11 that defines SAT as usual.

(ii) : However, PFm 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.

Sorry, you are wrong. PFm is not defined informally. It is not defined at all in the paper. It refers to the same pigeonhole formula of Haken as you

say is propositional for Haken, but not propositional for Tarnlund. Obviously, your argument collapses.

Fourth, there is more to correct, but we leave it for now and save our energy to scrutinise

Tarnlund's proof. After all the problem P vs NP is interesting enough to push on to the more sophisticated parts of the proof. You are welcome to join our reading club when you have catched up.

RCLP

Readings in complexity, logic and programming

You are right that PF_m can indeed be taken as propositional. My bad. Correction entered in posting.

ReplyDelete"First, take a good look at the formulas of theory B, then it should be clear why theorem 1 mentions the simply consistent extension B', introduced in definition 15."

Definition 15 does not introduce or even mention any B'. A few lines above Definition 15 theres an (incomplete) sentence that mentions B' but does not say anything to pinpoint B' among the infinity of consistent extensions of B, or even say how B' differs from B.

"Your statement: there is a fast Turing machine that recognizes tautologies but that we cannot prove that this is what it does. Of course, there is no such machine in theory B. Just take a good look at axiom 1, and definition 5, 13 and 14."

I believe you are misunderstanding my statement. For a given input, B can of course prove that the Turing machine computes whatever it computes. But I was talking about the meta-level statement that for ALL inputs "whatever the Turing machine computes" happens to be the correct answer to the SAT problem for that input.

"So much for what you call the main argument of the paper."

The main argument in the paper appears to be the step from equations (49) and (50) to (51) where you assume that a fast run of an *arbitrary* SAT-solving Turing machine corresponds to a short resolution proof of its input. Your response does not address that at all.

However, here is a counterexample to (49),(50)=>(51): Consider a SAT-solving machine which works by first checking if its argument is textually identical to not-PF_m (easily done in polynomial time) -- if so it answers 'unsatisfiable' immediately; otherwise it does a slow exhaustive search for a satisfying truth assignment. It is true that there is a (polynomially) short proof in B that the Turing machine answers 'unsatisfiable' on not-PF_m, but that is not the same as a short resolution proof of PF_m itself. (As it had better not be, because that would contradict Haken).

I'm aware that my machine does not satisfy (47), but it does satisfy (48)-(50), so it works as a counterexample for the purported inference from (49),(50) to (51).

Furthermore, the paper does not even attempt to justify the inference that leads to (51). Why, the very definition of the notation used in (51) is the last thing that happens before Theorem 1, and nowhere is there any sentence or argument that connects the length of Turing machine computations to the length of resolution proofs.

Let me try to clarify what RCLP tried to say. I can understand that they do not bother to reply on your last response, so let me do it on their behalf.

ReplyDeleteI am not claiming that Tärnlund's paper is correct, since I haven't gone through the details yet. However, it hurts my sense of justice when a paper gets debunked for the wrong reasons. Note that your blog is already being quoted on the internet as a negative indication of the papers correctness.

First of all, Tärnlund argues that there cannot exist a polynomial length deduction of some tautologies of the pigeon hole principle in Theory B (relating it

to a Hilbert system of propositional logic).

Second, you state that:

"I believe you are misunderstanding my statement. For a given input, B can of course prove that the Turing machine computes whatever it computes. But I was talking about the meta-level statement that for ALL inputs "whatever the Turing machine computes" happens to be the correct answer to the SAT problem for that input."

You don't need to be able to prove that your Turing Machine solves SAT for all possible inputs. It is sufficient to assume that you are in the possession of a Turing Machine that solves SAT. Tärnlund takes such a turing machine and adds a trail of deductions in Theory B starting from the axiom B.

Given such a Turing Machine, run the negation of a sufficiently large tautology of the pigeon hole principle (named F).

For this particular input there cannot exist a polynomial deduction of the fact that F is a tautology. But since we run -F and finds (in polynomial time) that

the clause is not satisfied, we can deduce that F is a tautology, and furthermore, the trail left by our turing machine constitutes a proof in theory B of this fact.

But in Theory B there cannot exist a polynomial proof

that F is a tautology. Thus, we get a contradiction.

What I want to say is that you do not need to prove that your Turing machine solves SAT for all possible inputs. The assumption is that it does.

"However, here is a counterexample to (49),(50)=>(51): Consider a SAT-solving machine which works by first checking if its argument is textually identical to not-PF_m (easily done in polynomial time) -- if so it answers 'unsatisfiable' immediately; otherwise it does a slow exhaustive search for a satisfying truth assignment. It is true that there is a (polynomially) short proof in B that the Turing machine answers 'unsatisfiable' on not-PF_m, but that is not the same as a short resolution proof of PF_m itself. (As it had better not be, because that would contradict Haken)."

I am not sure what you are saying here. What does "textually identical to not-PF_m" mean, and how is that easily done in polynomial time?

Note again that if we feed our SAT solving TM with -F and it returns in polynomial steps with an unsatisfying

result, we have (in theory B, starting from axiom B) proved that F is a tautology (because if -F is not satisfiable, there cannot be a non-truth assignment of F).

Consider the "short proof" definition of NP. It states that if there is a satisfying assignment then there should be a short proof of its correctness. But it does not say anything about unsatisfiability. This is what Tärnlund aims at. Use Theory B to get a proof even for unsatisfying assignments. This is sweet.

To debunk the paper I would focus on Theory B and its relation to the Hilbert systems of propositional logic (since personally, I'm not there yet).

Mikael Hammar

PhD Computer Science

Apptus Technologies AB

What has happened to this proof?

ReplyDeleteI attended a lecture by Sten-Ake Tarnlund yesterday, and despite his age he appears to still be working on this. I didn't understand everything, being a master student, but all in all it appeared that he has gotten more structure, clarifications and more support for his proof. I can't make any guarantees but I believe something might be published in a not so distant future.

DeleteThis comment has been removed by the author.

ReplyDeleteThis comment has been removed by the author.

ReplyDeleteHi Mikael,

ReplyDeleteYou showed that this proof is false but have you noticed a significant value of this paper that was implied by fallacy you discovered? You said: "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."

This improves work of Yannakakis who proved that you cannot solve NP problem in polynomial time by a symmetric linear program. You actually proved that you cannot solve in NP problem in P by using any constructible algorithm. You showed that if P=NP is true, the proof would not provide any constructible algorithm.

Is there something wrong with my reasoning?

It can serve as basis for writing thematic essays. Now, there are many services that will help write an essay, but I would like to single out one of them. The last few years, my daughter use this resource and is very satisfied with the quality of their work http://essays.io/. I recently evaluated their quality, they prepared me quality information for my request. I was pleasantly surprised with the result.

ReplyDeleteThank you for useful resources! I also want to advise a wonderful one https://paidpaper.net/resume/ where you can select a writer of essays with relevant skills. I often use the services of writers for articles in my blog.

ReplyDeleteI am very grateful to you for having decided to share your experience in this matter and have written an article about this. I also like to write an essay, but often my skills do not allow me to write complex essays, so I often use https://academic-consultants.com/term-paper-writing/ for that. Good luck!

ReplyDeleteHi! Thanks for the great information you have provided! Send gifts to Pakistan from usa

ReplyDeleteGreat Article i like it,This is a really like it Send online gift in Pakistan.

ReplyDeleteYou have a good point here!I totally agree with what you have said!!Thanks for sharing your views...hope more people will read this article!!!

ReplyDeleteprofessional tree trimmers

Great article and a nice way to promote online. I’m satisfied with the information that you provided home security hialeah

ReplyDeleteThanks for the wonderful share. Your article has proved your hard work and experience you have got in this field. Brilliant .i love it reading. home surveillance kendall

ReplyDeleteThis is a great article thanks for sharing this informative information. I will visit your blog regularly for some latest post.home automation miami

ReplyDeleteThis post is good enough to make somebody understand this amazing thing, and I’m sure everyone will appreciate this interesting things.school cleaning fort lauderdale

ReplyDeleteI have read your article, it is very informative and helpful for me.I admire the valuable information you offer in your articles. Thanks for posting it..commercial painting st lucie county

ReplyDeleteThanks for the wonderful share. Your article has proved your hard work and experience you have got in this field. Brilliant .i love it reading. popcorn removal treasure coast

ReplyDeleteThis is a great article thanks for sharing this informative information. I will visit your blog regularly for some latest post.tile installation fort pierce

ReplyDeleteI have read your article, it is very informative and helpful for me.I admire the valuable information you offer in your articles. Thanks for posting it..bathroom remodeling port st lucie

ReplyDeleteThis is a great article thanks for sharing this informative information. I will visit your blog regularly for some latest post.kitchen remodeling fort pierce

ReplyDeleteI have read your article, it is very informative and helpful for me.I admire the valuable information you offer in your articles. Thanks for posting it..remodeling contractor st lucie county

ReplyDeleteExcellent Post! For more information Visit Here.gym cleaning west palm beach

ReplyDeleteI have read your article, it is very informative and helpful for me.I admire the valuable information you offer in your articles. Thanks for posting it..land clearing royal palm beach

ReplyDeleteBut Hedgehog's usually wide awake at this time of the night Fire lane striping chicago il

ReplyDeleteIncredible article! Thanks for sharing your information with us. | https://scottkeeverseo.com/

ReplyDeleteAl Qur'an Keutamaan Doa Abu Darda RA Syekh Abdul Qodir Jailani Rahmat Allah SWT Malaikat Mazhab Hanafi Shalat Tahajud Shalawat Nabi Muhammad Shallallahu 'Alaihi Wa SallamCara Wudhu Nabi Muhammad Saw

ReplyDeleteI really enjoyed reading this post, I always appreciate topics like this being discussed to us. commercial cleaning service west palm beach Thanks for sharing.

ReplyDeleteThis could be one specific with the most beneficial blogs roof contractor west palm beach We have ever arrive across on this subject. Really Wonderful. I’m also an expert in this topic so I can understand your hard work.

ReplyDeleteGreat Post, checkout this amazing stuff:- Algebra 2 Tutoring In Los Angeles

ReplyDeleteroblox asset downloader

ReplyDeleteThanks for such a great post and the review, I am totally impressed! Keep stuff like this coming..natural ways to get rid of lice

ReplyDeleteThanks for such a great post and the review, I am totally impressed! Keep stuff like this coming..homecashoffer

ReplyDeleteSTL Pro Tree Services specializes in residential tree removal in St. Peters and surrounding areas. Contact us for a FREE Quote.

ReplyDeleteTree Service In Fairview Heights. Visit https://stlprotrees.com/fairview-heights.html

ReplyDeleteI understand this is extremely boring as well as likewise you are missing to being successful comment, nevertheless I simply called for to throw you a huge many thanks you tidied up some things for me! Your post is so exceptional and also useful. The web site style is perfect. Inter Mountain Bikes

ReplyDeleteI recognize this is incredibly uninteresting and additionally you are missing to being effective remark, however I simply called for to toss you a substantial many thanks you tidied up some things for me! Your post is so exceptional as well as likewise interesting. The site style is excellent. Find Camping Gear

ReplyDeleteI understand this is incredibly dull and additionally you are missing out on to being effective remark, nonetheless I just required to throw you a massive many thanks you cleaned up some things for me! Your article is so amazing and also interesting. The site style is excellent. Indoor Cardio Pro

ReplyDeleteI recognize this is extremely uninteresting and additionally you are missing to being successful statement, nevertheless I simply called for to toss you a massive many thanks you cleaned up some things for me! Your article is so exceptional and also insightful. The web site design is excellent. Little Pet Corner

ReplyDeleteI know this is exceptionally uninteresting and additionally you are missing to being effective statement, nonetheless I just needed to toss you a significant thanks you tidied up some things for me! Your blog post is so exceptional and additionally informative. The site design is excellent. ComfyKitchen Thank you so much for providing such an awesome content, Keep up the nice work.

ReplyDeleteFull Tree Removal Service Arborist in St. Peters. Learn more about us stpeterstreeservice.com

ReplyDeleteI am interested in this area if you are a great site but know some community forums. I think it should be a good opportunity to get feedback from others who are experienced. Feel free to visit my website; 먹튀검증가이드

ReplyDeleteI was surfing net and fortunately came across this site and found very interesting stuff here. Its really fun to read. I enjoyed a lot. Thanks for sharing this wonderful information. Feel free to visit my website; 카지노사이트링크

ReplyDeleteI was very pleased to find this site.I wanted to thank you for this great read!! I definitely enjoy every little bit of it and I have you bookmarked to check out new stuff you post. Feel free to visit my website; 온라인카지노사이트넷

ReplyDeleteThanks for sharing. I found a lot of interesting information here. A really good post, very thankful and hopeful that you will write many more posts like this one. Feel free to visit my website; 토토사이트

ReplyDeleteWow, awesome blog layout! How long have you been blogging for? you make blogging look easy. The overall look of your web site is great, as well as the content!Feel free to visit my website; 카지노사이트위키

ReplyDeleteI am pleased that I observed this site, exactly the right information that I was searching for! 카지노사이트

ReplyDelete