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$.

I asked a similar question about Rosser sentences a while ago on math.stackexchange and Peter Smith gave some interesting references in his answer: http://math.stackexchange.com/a/372199/9440.

Thanks for those links. I had thought that the next step is to inquire whether the Rosser sentence is unique, and I guess the answer is more complicated than I expected, since it seems that Solovay et al have proved that even with natural provability predicates, the Rosser sentence can be non-unique, depending on the implementation. I find that a bit unsatisfactory…Hmmmnnn…

All Gödel sentences are equivalent, but some are more equivalent than others.

I have a question: in hour argument for the uniqueness of the natural Gödel sentence, you assume that the sentence which asserts yhe consistency of PA is unique. Is that easy to show as well?

No, I didn’t assume that, but what I did assume was that we can provably translate proofs from one formalization to the other (and to/from the meta-theory), and this is what the derivability conditions amount to. Because of this, the assertions Con(PA) for the various natural formalizations of proof are all provably equivalent, since they all express that there is no proof of 0=1 in PA. Because we can provably translate the proofs, if one of them is true, then they are all true.

Thanks, that was illuminating!

Pingback: Breaking logic with self-referential sentences |

Hi Joel. Thanks for this post. It was great. I just want to make sure I understand. So suppose in PA that we have created a code for the meta-language and have identified a statement G, which asserts its own non-provability using the natural provability predicate. Moreover, we have identified a second G’ that also asserts it’s own non-provability using the natural provability predicate. If I then build a new theory PA+G, will I be able to construct a proof within PA+G of G’? If so, can you sketch out what that proof might look like?

Sure. The usual proof of the second incompleteness theorem shows in PA that G is equivalent to Con(PA). And similarly G’ is equivalent to Con(PA). So PA proves that G and G’ are equivalent to each other.

Sorry to harp on this but I’m having a bit of trouble understanding. G and G’ are derived using different codings of the meta-language of PA. So aren’t they equivalent to different versions of Con(PA)?

And then, I suppose, if we find some other sentence, not using Godel’s fixed-point argument, which is also true but unprovable – yet doesn’t assert its own unprovability – wouldn’t it also be equivalent to Con(PA)?

That is to say: is every axiomatic sentence (axiomatic in the sense that axioms are true but unprovable) that is discoverable in PA also equivalent to Con(PA)?

Ah, no, my claim was that for a given coding of the proof theory, all Gödel sentences are equivalent to each other, because they are equivalent to Con(PA) for that encoding. If you have a different metatheoretic encoding of the proof system, then in general you should not expect them to be equivalent, and we can easily make examples where they are not equivalent, by baking arithmetic assertions into the nature of the encoding of proofs.

Thank you for the insight.

So then it sounds like if you imagine all encodings of PA, including simple ones that switch the codes of characters, and more complex ones that represent symbol strings differently (or perhaps even ones that rely on non-lossy compressions of proofs), each Godel sentence G is unique, in that they do not necessarily entail each other.

If you have any links to books or papers that explore these sorts of things, I’d appreciate the references.

Thanks for your help!

Feferman has written on this, from the 1960s. But I don’t really agree with your comments, if they suggest that somehow Gödel sentences are generally inequivalent for different natural ways of formalizing the proof systems. My view is that for all natural, acceptable manners of formalizing the metatheoretic proof system, the Gödel sentences will all be equivalent, and all the Con(PA) assertions will be equivalent; PA will be able to prove the equivalence of the different formalizations. The inequivalent versions will arise only by using strange or devious systems that embed strong arithmetic assertions into the operation of the proof systems, and these will ultimately be viewed as unnatural. These aspects of the proof systems and whether they are “natural” or not are exactly what Feferman was concerned with. It is a notorious difficult problem, to define what we mean by “natural” in mathematics, and I have argued that indeed there is no mathematical robust concept of what counts as natural—one will ultimately be led to formulate more precisely what we mean by natural. And what I would count as a necessary requirement for counting as natural for an implementation of a proof system in arithmetic is that it be PA-provably equivalent to any of the usual standard implementations. In this case, for every natural arithmetized proof system, all the Gödel sentences will be provably equivalent.

I’m fascinated by this distinction between encoding natural vs strange (perhaps exotic?) proof systems. Have you written anything longer-form on the subject that you could send me? – doug.rubino@gmail.com. Thanks so much for taking the time to explain all this.