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.
Solution 1:
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.