# Is Rosser's trick necessary?

A version of Gödel's first incompleteness theorem goes as follows:

Any true, definably axiomatized theory $T$ in the language of arithmetic is incomplete.

(by $T$ being true I mean $\mathbb{N}\vDash T$). An explicit proof of this (avoiding Tarski's undefinability result) proceeds by constructing a Gödel sentence for the theory, i.e. a sentence $\sigma$ such that $Q\vdash (\sigma\iff \lnot\mathrm{Bwb}_T(\ulcorner\sigma\urcorner))$, where $Q$ is Robinson's arithmetic and $\mathrm{Bwb}$ is the provability predicate.

One can do a bit of shuffling around with the hypotheses and get Rosser's version of the theorem:

Any consistent, recursively axiomatized theory $T$ in the language of arithmetic which extends $Q$ is incomplete.

Rosser's proof of this version involves a clever diagonalization in the spirit of the Gödel sentence. But is this trickery necessary? One can show fairly easily that, under the assumptions of Rosser's theorem, $T$ does not prove its Gödel sentence $\sigma$, but I can see no obvious way of showing that $T$ does not prove $\lnot\sigma$ without adding assumptions like trueness, $\omega$-consistency or something similar.

My question is then whether Rosser's trick is really necessary to produce his result. To be specific, is there a theory, satisfying the assumptions of Rosser's theorem, that proves the negation of its own Gödel sentence?

Note that the obvious first try of $T+\lnot\sigma$ doesn't seem to work, since $\sigma$ might not be the Gödel sentence of this new theory.

• I know this is an old post, but Rosser's trick is not actually necessary. It may be surprising but there is actually a simple computability proof of a general version of the incompleteness theorem. It is interesting that it is very similar to the proof of Godel's original theorem via reduction to the unsolvability of the halting problem, just using the unsolvability of a weaker computability problem. – user21820 Sep 13 '18 at 14:20

Let me restrict attention to consistent, recursively axiomatized extensions $T$ of Peano Arithmetic PA.
Preliminary consideration: For such $T$, one can formalize in $T$ the proof that consistency of $T$ implies that the Gödel sentence $\sigma$ of $T$ is unprovable. Since $\sigma$ asserts precisely this unprovability, we get that Con($T$) implies $\sigma$, provably in $T$. (This is the heart of the proof of the second incompleteness theorem.) Conversely, $\sigma$, asserting that something (namely itself) is unprovable in $T$, immediately implies Con($T$). Thus, the Gödel sentence $\sigma$ is provably (in $T$) equivalent to the consistency of $T$.
In view of this preliminary consideration, your question is equivalent to asking whether some such theory $T$ can prove its own inconsistency (while actually being consistent). The answer is yes. Let $T$ be PA plus $\neg$Con(PA). This theory is consistent, by Gödel's second incompleteness theorem. But since it extends PA and asserts the inconsistency of PA, it proves its own inconsistency.