The definition of \NP\ requires, for each member language~$L$, a polynomial-time checking relation~$R$ and a constant~$k$ such that $w \in L \iff \exists y\,(|y| \leq |w|^k \wedge R(w,y))$. We show that this biconditional instantiates, for each member language, Hilbert's triple: a sound, complete, decidable proof system in which truth-in-$L$ and bounded provability coincide by fiat. We show further that the polynomial-time restriction on~$R$ does not exclude Gödel's proof-checking relation, which is itself polynomial-time and fits the definition as a literal instance. Hence \NP, taken as a totality over all polynomial-time~$R$, contains languages for which the biconditional asserts a property that Gödel's First Incompleteness Theorem prohibits. The semantic definition of \NP\ is unsatisfiable, for the same reason that Hilbert's Program is.

翻译：\NP\ 的定义要求：对于每个成员语言~$L$，存在一个多项式时间验证关系~$R$ 和一个常数~$k$，使得 $w \in L \iff \exists y\,(|y| \leq |w|^k \wedge R(w,y))$。我们证明，对于每个成员语言，该双条件语句实例化了希尔伯特三元组：一个可靠、完备且可判定的证明系统，其中在 $L$ 中的真与有界可证性通过定义重合。我们进一步证明，对~$R$ 的多项式时间限制并未排除哥德尔证明检验关系——该关系本身是多项式时间的，且作为字面实例符合该定义。因此，将 \NP 视为所有多项式时间~$R$ 的总体，它包含了那些双条件语句断言了哥德尔第一不完备定理所禁止性质的成员语言。基于与希尔伯特纲领相同的理由，\NP 的语义定义是不可满足的。