 When applied to the formula \(\neg \textrm{Prov}_{\mathsf{P}}(x)\), the Diagonal Lemma yields a sentence \(G_{\mathsf{P}}\)—i.e., the so-called Gödel sentence for \(\mathsf{P}\)—such that \(\mathsf{P} \vdash G_P \leftrightarrow \neg \textrm{Prov}_{\mathsf{P}}(\ulcorner G_{\mathsf{P}} \urcorner)\). \(G_{\mathsf{P}}\) is thus interpretable as “saying of itself” that it is unprovable in \(\mathsf{P}\).  Gödel showed that this formula has the following properties: 