Hacker News Reader

Comment by presidentender | Hacker News Reader

The year is 2230. The Nuclear Winter has passed, and the water wars have come.

One mathematician - the last of his kind - dares to spend precious time puzzling through theorems, seeking out ancient tomes of knowledge written in arcane symbols. He is searching for a proof which meant something to his ancestors hundreds of years ago.

One day, in a dusty library in what used to be called New England, he finds it. Not only through reading the works of others, no, he has proven many new theorems, and his results would have held application to the software efforts of centuries ago. God weeps that there is no software now.

But he has at last found it, the final proof: that it cannot be proven that it cannot be proven ... that it cannot be proven conclusively whether P = NP.

View on HN

Suppose we could resolve (conclusively prove one way or the other) whether P=NP. Then we could also prove that we could resolve whether P=NP. Thus, if we can prove that you cannot prove that you can resolve P=NP, then we have also proven that we cannot resolve P=NP, a contradiction. Thus proving that we cannot prove that we cannot prove that we cannot resolve whether P=NP. This proves that we cannot prove that we cannot prove that we cannot prove that we cannot resolve whether P=NP. etc.

Let A be the statement: "P=NP or P!=NP" (in other words, suppose P vs. NP is decidable in some chosen axiomatic system, like Zermelo-Fraenkel set theory with or without axiom of choice).

You first said:

Suppose we proved A. Then we could also prove that we proved A. This is practically a tautology, since if we proved A, of course we can prove we proved A. I'll just hand you the proof.

Next, you said:

Suppose we can prove ~A (in other words, suppose we can prove that P vs. NP is undecidable in the given axiomatic system). Contradiction!

To sum it up, you said: "Suppose A and ~A. Contradiction!"

Or am I missing something here?

Ya, it looks like I bungled the logic. Let 'Pr X' means 'X is provable'. Let A be your A. Really what I wanted to say is that:

Pr A -> (~Pr ~Pr A)

and thus, Pr a -> Pr ~Pr ~Pr A.

Hence, ~Pr ~Pr ~Pr A -> ~Pr A

Taking A to be ~Pr A, we get:

~Pr ~Pr ~Pr ~Pr A -> ~Pr ~Pr A

So you can peel off pairs of ~Pr until you get down to one or two. Not very surprising, I guess, since Pr A == A in constructive logic, and you can do similar negation collapsing there.

The story reads great :D

But first and foremost, I like how ``it cannot be proven that...'' is a special kind of negation, much different than the ordinary negation in boolean logic. Is there any formalized logic system with a negation with properties like ``it cannot be proven that...''?

I'd go see that movie.

Reply on news.ycombinator.com