Confused about Wikipedia definition of NP

I've been checking my understanding of the definitions of NP and NP-complete and I am confused by some of the definitions given on Wikipedia; for example, the article about NP-complete describes NP as:

the set of all decision problems whose solutions can be verified in polynomial time

And the Wikipedia article about NP says:

Intuitively, NP is the set of all decision problems for which the instances where the answer is "yes" have efficiently verifiable proofs of the fact that the answer is indeed "yes." More precisely, these proofs have to be verifiable in polynomial time by a deterministic Turing machine.

Taking these definitions at face value, it would seem that the set $S$ of all sentences provable in ZFC is in NP because the set of all valid ZFC proofs is in P. However there are theorems in ZFC that require super-polynomial proofs, so $S \in P → ¬Con(ZFC)$, or in other words it is impossible to prove that P=NP.

Shouldn't it be said in both cases that the size of the solution or proof must be bounded by a polynomial in the size of the problem? The Wikipedia language suggests that it is sufficient for the solution to be verified in time polynomial in its own size, which I am arguing is not enough to define NP. Am I right to raise this objection? In any case, how should I best understand these definitions?

-
In the Wikipedia there is no formal definition since the term used is "efficiently verifiable". Do you guess how to translate this expression to a formal setting? – boumol Oct 9 '11 at 7:27
@boumol, I'm interpreting that to mean "verifiable in polynomial time in its own length". But I think what it really should mean is "verifiable in polynomial time in the length of the problem". – Dan Brumleve Oct 9 '11 at 7:28
"Efficient" always means "verifiable in polynomial time in the length of the input". And in this case the input is the formula, not the ZFC-proof. – boumol Oct 9 '11 at 7:34
@boumol, that exactly what I'm not sure about. Will you please add that as an answer if you can explain how to parse it from the Wikipedia definitions? – Dan Brumleve Oct 9 '11 at 7:38

Yes, the "proof" has to be polynomial in the size of the original question.

The first quoted statement:

the set of all decision problems whose solutions can be verified in polynomial time

If you take the decision problem $\{ \phi : \phi \text{ is provable in ZFC}\}$ then the solutions to this problem cannot even be verified computably (that is, the problem is not even decidable) so they certainly cannot be verified in polynomial time. In general, if a statement is not provable in ZFC, there is no way to make a certificate (warrant) that would allow someone else to verify this fact.

But it is not clear what it means to "verify a solution" to a decision problem. It would suggest to me that you are given the input and the solution (yes or no) and have to verify based on that. In reality, of course, for NP you are given a certificate to use for the verification of each positive answer. The article does have a definition below the introduction that is formally correct. It seems to me that this quoted sentence is such an analogy that there is no easy way to make it more precise.

The second quoted statement:

Intuitively, NP is the set of all decision problems for which the instances where the answer is "yes" have efficiently verifiable proofs of the fact that the answer is indeed "yes." More precisely, these proofs have to be verifiable in polynomial time by a deterministic Turing machine.

The thing they call a "proof" there is what I call a certificate. It makes sense to me that for a family of certificates for a problem to be efficiently verifiable, the certificates cannot be too long compared to the numbers they certify. So the certificate for $n$ should be bounded by a polynomial function of $n$. But this takes a very careful reading of the text, and it's true that the second quoted phrase doesn't say what the "polynomial time" is a function of. On the other hand, the article does have a more formal definition below the introduction.

I think your confusion is reasonable for someone learning the field. Perhaps you could consider clarifying the NP article to point out that the size of the "proof" has to be bounded by a polynomial function of the size of the original question. The formal definitions in both articles seem correct. The problem of making an introduction which is both formally correct but also accessible to untrained readers is a particular challenge for Wikipedia.

-
Thanks Carl! I'm understanding that "certificate", "warrant", "witness" are more appropriate words to use than "proof" and "solution" when polynomial size is assumed. I see that the polynomial size constraint is explicitly stated in this section. – Dan Brumleve Oct 10 '11 at 5:22
@Dan Brumleve: My only concern with the word "proof" is that we already have a meaning for that term, and in general the certificate for an instance of an NP problem may not be a formal proof in the usual sense. For example a certificate for the knapsack problem (as usually formalized) is just a list of numbers. – Carl Mummert Oct 10 '11 at 11:06
You seem to be confusing NP with the intersection of NP and co-NP (although if I'm misunderstanding you, I apologise). NP problems have polynomial certificates that the answer is yes; co-NP problems have polynomial certificates that the answer is no. It's not known whether NP = co-NP. – Peter Taylor Oct 10 '11 at 12:10
@Peter Taylor: Thanks. Yes, an NP problem must have short certificates for positive answers, but not necessarily for negative answers. I tried not to contradict that in my text; I edited the third paragraph to emphasize it more. In the 2nd paragraph, I was really just pointing out how tenuous the link is between the first quoted statement and the definition of NP. I was also pointing out that the problem $\{\phi : \text{ZFC} \vdash \phi\}$, mentioned in the question, is not decidable, hence not in NP. Perhaps you would instinctively prove that particular problem is not in NP by other means. – Carl Mummert Oct 10 '11 at 12:26
The first quoted phrase from Wikipedia would certainly be better if it said "the set of all decision problems whose positive solutions can be verified in polynomial time". – Carl Mummert Oct 10 '11 at 12:30

I think your confusion arises from not discerning NP with NP completeness.

In computation theory, a useful to describe a problem is as a formal language. The language defines the alphabet (when talking about a logic system those could be the numerals, literals, quantifiers and so on), and which words are legitimate (which would be well structured syllogisms. When discussing ZFC you could restrict them to the syllogisms which coexist with the ZFC axioms). The problem is then reduced to deciding whether an arbitrary word over the given alphabet is in the set of words.

There are many possible ways to define "deciding", the most straightforward one would be to demonstrate a Turing machine which, given a word, either accepts it or rejects it in a finite number of steps.

NP is the class of all languages which can be decided in a polynomial time (that is, that there's a bound over the number of needed steps for an arbitrary word, which is polynomial in it's length) using a non deterministic Turing machine. A problem is said to be NP if it is in this class.

For a language to be NP complete, it not suffices for it to be in NP, it must also satisfy the condition that every language in NP can be reduced to it in polynomial time.

This notion is extremely important for various reasons, one of which is the fact that proving that a single NP-complete problem is in P would prove that P = NP.

Given the above, you may see that stating that "the set S of all sentences provable in ZFC is in NP because the set of all valid ZFC proofs is in P" is meaningless. In truth, for ZFC to be in P, you must devise an algorithm (or a Turing machine) that given any proof in ZFC could decide it polynomially.

This isn't very simple to do (and would in fact prove that P=NP), because it can be easily shown that, given such an algorithm, one could reduce the satisfiability problem to it, proving that P=NP.

-
Downvoting without explaining yourself isn't a very nice thing to do... – user864940 Oct 9 '11 at 10:54
It is certainly true that given a string $\sigma$ which purports to be a formal proof in ZFC, one can verify in polynomial time whether the string is actually a formal proof in ZFC. So the set of formal proofs in ZFC is a set in P. (Note I am not the person who voted -1.) – Carl Mummert Oct 9 '11 at 11:59
I think this is a fine definition of NP and NPC but it doesn't really answer my question. Also I'm not sure that you are interpreting my ZFC example correctly (the point is that we can't prove it is in NP either (because that also means ZFC is inconsistent), although the way the Wikipedia definition is written suggests that it is). I didn't downvote either. – Dan Brumleve Oct 10 '11 at 5:31