 As it happens, if the formal system \(F\) under consideration is indeed consistent, Rosser’s provability predicate is co-extensional with the ordinary provability predicate. Applying the Diagonalization Lemma to the negation of Rosser’s provability predicate \(\Prov^*(x)\) gives: