I should like to consider a family of natural questions concerning the Gödel sentence — the sentence asserting its own non-provability, used by Gödel to prove the incompleteness theorem — and specifically the question whether we are really entitled to speak of the Gödel sentence. Is it unique? Is it unique up to equivalence? Up to provable equivalence? Could there be more than one Gödel sentence, perhaps for different manners of arithmetizing the syntax? Are they all provably equivalent? These questions have come up a number of times in various contexts, and since James Propp just sent me an email inquiry about it yesterday, let me address the questions here in reply (he is planning an upcoming post in a few weeks about incompleteness and self-reference — check back later for the link). I shall make use only of elementary classical incompleteness ideas, and I assume this has all been known for some time.

For definiteness, let us take first-order Peano Arithmetic ($\newcommand\PA{\text{PA}}\PA$) as the base theory over which we are considering provability, although similar observations can be made concerning other base theories. By formalizing the syntax in arithmetic using Gödel coding, we may easily produce an arithmetically expressible provability predicate $\newcommand\Prov{\text{Prov}}\Prov(x)$, which asserts that $x$ is the Gödel code of a $\PA$-provable sentence. By using this predicate and the fixed-point lemma, we may construct a sentence $\psi$ that asserts its own non-provability, meaning precisely: $\PA\vdash\psi\leftrightarrow\neg\Prov(\ulcorner\psi\urcorner)$. Such a sentence $\psi$ is known as the Gödel sentence, and we may use it to prove Gödel’s first incompleteness theorem as follows. Namely, it is easy to see that $\psi$ cannot be provable in $\PA$, for if it were, then in virtue of what $\psi$ asserts, we will have also proved that $\psi$ is not provable, contrary to fact. So $\psi$ is not provable, and therefore we see that indeed $\psi$ is actually true. So the sentence $\psi$ is true, yet unprovable. By paying a little closer attention to the argument, what we have actually argued is that $\PA$ itself proves that if $\newcommand\Con{\text{Con}}\Con(\PA)$, then $\psi$.

Of course, there are many fixed points, and for example any sentence that is provably equivalent to $\psi$, such as $\psi\wedge\psi$, is also provably equivalent to its own non-provability, and therefore serves as yet another Gödel sentence. In this trivial sense, there are infinitely many different Gödel sentences. But these particular sentences, by construction, are provably equivalent. Are all the Gödel sentences equivalent?

Indeed, a bit more generally, suppose that we have two implementations of the provability predicate, using perhaps different formalizations of the syntax, with $\varphi$ and $\psi$ being fixed points of non-provability-in-$\PA$, so that $\varphi$ and $\psi$ each assert their own non-provability with respect to those predicates. Must $\PA$ prove that $\varphi$ and $\psi$ are equivalent?

The first, main answer is that yes, indeed, if we have used a natural provability predicate, then all the Gödel sentences are provably equivalent, and this remains true even for different natural manners of formalizing the syntax. In this sense, therefore, there really is only one Gödel sentence and we are entitled to speak of the Gödel sentence. The reason is that every such Gödel sentence is provably equivalent to the assertion $\Con(\PA)$, and for natural formalizations of the syntax, meaning implementations where we can provably translate proofs from one system to another and the meta-theory, these assertions are all equivalent. To see this, suppose that $\psi$ is a Gödel sentence, which means that $\psi$ asserts its own non-provability. Since $\psi$ implies that there is a non-provable sentence, namely $\psi$ itself, it follows immediately that $\psi$ implies $\Con(\PA)$; conversely, if $\Con(\PA)$ holds, then the argument of the first incompleteness theorem that I mentioned above shows that $\psi$ is true. So $\PA\vdash\Con(\PA)\leftrightarrow\psi$. So all the fixed points are equivalent to the assertion $\Con(\PA)$. For systems where we can provably translate proofs from one system to another, the corresponding consistency assertions $\Con(\PA)$ are equivalent. And so it is fine to speak of the Gödel sentence.

But let me now discuss what happens if we should implement a more exotic form of the provability predicate. For example, consider the Rosser provability predicate, where we say that a sentence $\sigma$ is Rosser provable, if there is a proof of $\sigma$, but no shorter proof of $\neg\sigma$, meaning no proof of $\neg\sigma$ with a smaller Gödel code. The Rosser sentence $\rho$ is a non-provability fixed point of this notion, saying, “I am not Rosser provable.” Since Rosser provability is intuitively a stronger notion of provability, it would be reasonable to expect that the Rosser non-provability assertion is weaker than the Gödel sentence, and indeed that is the case. If the base theory is consistent, then the Rosser sentence cannot be provable, since if it were, then there would have to be a smaller proof of $\neg\rho$, violating consistency; but also, $\neg\rho$ cannot be provable, since this sentence implies immediately that $\rho$ is also provable with a shorter proof, in light of what $\rho$ asserts. So $\PA$ proves that $\Con(\PA)$ implies both $\Con(\PA+\rho)$ and $\Con(\PA+\neg\rho)$, and moreover, $\PA\vdash\Con(\PA)\to\rho$. But since $\PA\vdash\Con(\PA)\to\Con(\PA+\rho)$, it follows that $\PA$, if consistent, cannot prove the converse, $\rho\to\Con(\PA)$, since otherwise $\PA+\rho$ would prove its own consistency, in violation of the second incompleteness theorem. So the Rosser sentence $\rho$ is strictly weaker than $\Con(\PA)$ over $\PA$, and hence also strictly weaker than the usual Gödel sentence. But since the Rosser sentence $\rho$ is itself a fixed point of non-provability with respect to the Rosser formalization of provability, it shows that exotic formalizations of the provability predicate can indeed give rise to inequivalent fixed-point assertions.

Note that the Rosser provability predicate does not sustain provable translations to any of the usual (natural) formalizations of provability, because we cannot prove in $\PA$ as a general statement that whenever a statement is provable, then it is Rosser provable. We can, however, generally translate specific proofs to Rosser proofs, and to the meta-theory, assuming that the base theory is consistent.

Lastly, let’s consider a somewhat more exotic provability predicate, arising from the Feferman-style enumerations of $\PA$, which are arithmetically definable but not computably axiomatizable. Specifically, consider the axiomatization of $\PA$, where we continue to add the usual $\PA$ axioms, but only so long as the resulting theory remains consistent. This way of describing the theory gives rise to a corresponding provability predicate, which expresses provability in that enumerated theory. So sentence $\theta$ is Feferman provable, if it is provable using axioms that come from a consistent initial segment of the $\PA$ axiomatization. If $\phi$ is a Feferman-non-provability fixed point, then $\PA$ proves that $\phi$ is equivalent to the assertion that $\phi$ is not Feferman provable. Since $\PA$ easily proves that the Feferman theory is consistent, and also that any finite collection of $\PA$ axioms are part of the Feferman theory, it follows that the negation of any particular theorem of $\PA$ is a Feferman-non-provability fixed point, since $\PA$ proves that it is false and also that it is not provable in the Feferman theory. But those statements are not equivalent to the usual Gödel sentence, since they are inconsistent with $\PA$.