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?
 A: 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. 
A: 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. 
