 More formally, let \(\ulcorner A \urcorner\) denote the Gödel number of arithmetical formula \(A\), which is the result of assigning a numerical code to \(A\). Let \(\Prov\) be the formalized provability predicate for Peano Arithmetic, which is of the form \(\exists p \, \Proof(p,x)\). Here, \(\Proof\) is the formalized proof predicate of Peano Arithmetic, and \(\Proof(p,x)\) stands for “Gödel number \(p\) codes a correct proof from the axioms of Peano Arithmetic of the formula with Gödel number \(x\)”. (For a more precise formulation, see Smoryński (1985), Davis (1958).) Now, suppose that Peano Arithmetic proves \(A \leftrightarrow \neg\) \(\Prov (\ulcorner A \urcorner)\), then by Gödel’s result, \(A\) is not provable in Peano Arithmetic, and thus it is true, for in fact the self-referential sentence \(A\) states “I am not provable”.