Fix a Gödel numbering scheme, and let $\operatorname{Thm}_{\mathsf{PA}}$ be the corresponding numerical provability predicate for Peano arithmetic. Suppose $\theta$ and $\xi$ are two sentences in arithmetic such that $\mathsf{PA} \vdash \theta \leftrightarrow \neg \operatorname{Thm}_{\mathsf{PA}} ( \ulcorner \theta \urcorner)$ and $\mathsf{PA} \vdash \xi\leftrightarrow \neg \operatorname{Thm}_{\mathsf{PA}} ( \ulcorner \xi\urcorner)$. Why must it be the case that $\mathsf{PA} \vdash \theta \leftrightarrow \xi$?

A few notes:

  • The diagonal lemma asserts existence but not uniqueness, so the usual construction of the Gödel sentence is non-unique.
  • The key difference with this post is that we're considering a fixed Gödel numbering scheme throughout.
  • This is an exercise in Leary and Kristiansen's Friendly Introduction to Mathematical Logic (chapter 6.6 exercise 2).
  • 1
    $\begingroup$ Incidentally, the accepted answer to the linked post is wrong: even if we allow the Godel numbering system to vary, as long as it satisfies some extremely mild conditions we'll still get the equivalence. $\endgroup$ Apr 29, 2022 at 12:47
  • $\begingroup$ I wrote the post cited above, which @NoahSchweber has also commented on. Incidentally, this problem is so similar to the one in my post that I pose to discredit the answer I had originally accepted. Except in this case, the encoding scheme is the same, but two separate Godel sentences are compared. It's unfortunate that "A Friendly Introduction to Mathematical Logic" does not provide the answer to this problem. $\endgroup$
    – Doug
    May 5, 2022 at 4:56
  • $\begingroup$ @NoahSchweber & Dave: what do you guys think of my answer? Seems straightforward $\endgroup$
    – Doug
    May 11, 2022 at 15:19
  • $\begingroup$ @Doug Yes, that's quite right. Incidentally the "different coding schemes" version isn't much different: you basically show that "$Con_{PA}$" according to a "reasonable" scheme amounts to a particular statement $\psi$ relativized to an interpreted structure $\mathfrak{A}$, where the interpretation of $\mathfrak{A}$ corresponds to the scheme used. The same structure, even interpreted two different ways, can't have two different properties. (Of course there's more to it than this and the messiness of the details explains why I haven't written it out yet, but it really is the same at the core.) $\endgroup$ May 11, 2022 at 15:30
  • $\begingroup$ @NoahSchweber I'm still having trouble with multiple encoding schemes. Essentially, you have two different Con[PA] statements. Proving them equivalent yields the generalization of the result below. I understand that they represent the same statement about PA. I just can't see (yet) that both versions of Con[PA] are provably equivalent within the system. In your version, where you reason about structures, presumably you will have to map that reasoning back into PA to prove it within PA. Sorry if I'm being sense. I appreciate your help $\endgroup$
    – Doug
    May 11, 2022 at 22:28

1 Answer 1


Could the answer be as simple as this?

I'm paraphrasing Note 2 from here. Every Godel Sentences is equivalent to the statement $Con_{PA}$, where $Con_{PA}$ is defined as:

$$Con_{PA} = \neg\exists x \;\; Thm_{PA}(\ulcorner x \urcorner) \;\land\; \neg Thm_{PA}(\ulcorner x \urcorner)$$

$Con_{PA}$ doesn't depend on the particular Godel Sentence, so it must be equivalent to both $\theta$ and $\xi$. Therefore: $$\theta \leftrightarrow Con_{PA} \leftrightarrow \xi$$

And so:

$$PA \vdash \theta \leftrightarrow \xi$$


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .