Is P Versus NP Formally Independent?

[gusl]

Scott Aaronson's Is P Versus NP Formally Independent? is interesting.

My feeling is that it couldn't go the way of the Continuum Hypothesis, because if P=NP, then there is an algorithm that we can find. The CH, OTOH, does not entail the existence of anything concrete, whether it's assumed to be true or false.

P=NP
<=>
exists P-time-algorithm a ( a solves SAT )

in other words:
P=NP
<=>
exists algorithm a, polynomial function f ( forall inputs i ( a halts after no more than f(size(i)) steps, outputting the answer to whether i is satisfiable) )

This is a Sigma_2 statement about Turing Machines. This means that it has an objective meaning, and must therefore be true or false. I suspect this also means that ZFC can decide it (if it can't, then ZFC is not "meaningful-statement complete", which is a bad thing).

The CH is a Sigma_n statement (maybe it can also be considered Pi_n, if there is no standard way to push negations), but it's not about Turing Machines. This means that the meaning of CH, to the extent that it has one, is dependent on "non-computable" axioms.

Can anyone help me formalize this argument?

Reading Section 6 ("Conclusion"), I see that Aaronson discusses this argument I just made, agreeing with it (but not formalizing it):

But in one crucial respect, P = NP is not at all like CH. It’s a Pi_2-sentence. It refers, not to a transfinite realm beyond human experience, but to machines, Boolean circuits, 1’s and 0’s.
Here’s a simple argument for why, if you accept the physical process criterion, then you should accept
that any Pi_alpha-sentence has a definite truth-value.
...

---

Aaronson's paper seems to suggest that formalization can't make a proof more credible. I disagree with that, of course, but maybe I read too much into what he said and made a straw man.

via patrissimo, I found this very nice post that debunks "hypercomputation".

Comments

[jcreed.livejournal.com]

What about the situation where there is an algorithm that always solves problems in NP in polynomial time, but you can't prove that it does? There is more than one quantifier alternation in the question P=NP, remember.

[gustavolacerda.livejournal.com]

I've updated the post.

[gustavolacerda.livejournal.com]

If you gave me such an algorithm, I could prove, for any instance size, that "P=NP" holds for instances up to that size.

Maybe what I said above is meaningless. Let me try again:
If you gave me such an algorithm, I hope I could come up with a function f, for any instance size, that "f=NP" holds for instances up to that size.

[easwaran.livejournal.com]

That would give you a proof that P=NP, if you could come up with an algorithm for generating a proof up to each instance size.

This is something I noticed last spring - P=NP could be undecidable and true or undecidable and false, while the Riemann hypothesis (and I suspect the other Clay millenium problems) must be true if undecidable.

[rdore.livejournal.com]

P=NP is a Sigma₂ formula over the *natural numbers*, although you need to be more careful:


There exists a code for a TM m and an exponent k

So that for every: code for an input i and code for a computation tableau t

If (t codes the computation of m on input i)

Then (t is of length at most |i|^k, and if t halts it gives the correct decision)


I think basically what Aaronson is arguing that statements in first order arithmetic have a definite truth value, even if you can't prove what it is. This is not a mathematical claim.

It is much more reasonable to argue that higher order arithmetical statements don't have a clear truth value. They talk about sets of natural numbers and it seems harder to claim absolutely which sets of natural numbers you can reason about

And CH talks about sets of sets of natural numbers, so you have even less grounds on which to argue there.



if it can't, then ZFC is not "meaningful-statement complete", which is a bad thing.

What do you mean by a meaningful statement?

[gustavolacerda.livejournal.com]

I just spoke to Matt Szudzik, who told me that statements are still "meaningful" if the formula has up to one real-valued quantifier. A statement is "meaningful" in my definition, if it can be translated into a statement about a Turing Machine (namely, whether it halts and what it outputs).

He also told an amusing story about someone who tried to make a programming language based on Set Theory. Guess what? He never managed to make it work...

[(Anonymous)]

Hi Gustavo:

Have you ever tried to program this?

Aaron

[gustavolacerda.livejournal.com]

Hello Aaron (Aaron who?),

What is "this"?

Gustavo