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?
Yes, the "proof" has to be polynomial in the size of the original question.
The first quoted statement:
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:
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.