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?