 In fact, in favourable circumstances, it can be shown that \(G_F\) is true, provided that \(F\) is indeed consistent. This is the case if, for example, the provability predicate \(\Prov_F (x)\) has been chosen as a \(\Sigma^{0}_1\)-formula: The Gödel sentence is then provably equivalent to the universal formula \(\forall x\neg\Prf_F (x, \ulcorner G_F\urcorner)\).  Such formulas can be proved false whenever they in fact are false: if false, there would be a number \(\boldsymbol{n}\) such that \(F \vdash\Prf_F (\underline{n}, \ulcorner G_F\urcorner)\) (this holds already in Q). This, however, would contradict the incompleteness theorem. Therefore, \(G_F\) cannot be false, and must be true. For this reason, the Gödel sentence is often called “true but unprovable”.