 The incompleteness theorem which Gödel proved states that if \(\mathsf{P}\) is ω-consistent, then there exists a formula \(G_{\mathsf{P}}\) which is undecidable in \(\mathsf{P}\)—i.e., neither provable nor refutable from its axioms. In order to obtain such a formula, Gödel first demonstrated how it is possible to express various syntactic and metatheoretic properties of \(\mathsf{P}\)-formulas and proofs as primitive recursive relations via a technique which has come to be known as the arithmetization of syntax (see the entry on Gödel’s incompleteness theorems).  Second, he showed that for every primitive recursive relation \(R(x_1,\ldots,x_k)\) there exists a “class sign” (i.e., formula) \(\varphi_R(x_1,\ldots,x_n)\) of \(\mathsf{P}\) such that the fact that \(R(x_1,\ldots,x_n)\) holds of (or does not hold of) a given tuple of numbers \(n_1,\ldots,n_k\) is mirrored by the provability (or refutability) in \(\mathsf{P}\) of the corresponding instance of \(\varphi_R(x_1,\ldots,x_n)\) when the formal numeral \(\overline{n} = s(s(\ldots s(0)))\) (\(n\)-times) is substituted for \(x_i\)—i.e.,