The main difficulty of the first incompleteness theorem of Gödel is the complicated condition of $\omega $-consistency. Rosser found a trick that avoids this awkward assumption. This web page presents the idea as an extended exercise, using the key idea of diagonalisation together with representability of computable operations and the pairing function.

Assume that $T$ is a consistent recursive ${L}_{A}$ theory and ${\mathrm{Proof}}_{T}(x,y)$ is a ${\Delta}_{0}$ formula such that

$$\text{DOR}\u22a2\exists x\u200a{\mathrm{Proof}}_{T}(x,\u231c\theta \u231d)\iff T\u22a2\theta $$for each sentence $\theta $. The existence of such a ${\mathrm{Proof}}_{T}(x,y)$ follows from the fact that $T$ is recursive. Suppose also that $N(x,y,z)$ is a ${\Delta}_{0}$ formula such that

$$\text{DOR}\u22a2\exists x\u200aN(x,\u231c\varphi \u231d,\u231c\psi \u231d)\iff \psi \text{is}\neg \varphi $$Thus the formula $N$ strongly represents the recursive operation of decoding a Gödel-number, putting a not-sign in front of a formula and then recalculating the Gödel-number.

We use $x=\u27e8{x}_{0},{x}_{1},{x}_{2}\u27e9$ for a ${\Delta}_{0}$ formula coding triples.

The Rosser variant of ${\mathrm{Proof}}_{T}(x,y)$ is ${\text{RProof}}_{T}(x,y)$ defined to be

$$\exists {x}_{0},{x}_{1},{x}_{2}<x\u200a\left(x=\u27e8{x}_{0},{x}_{1},{x}_{2}\u27e9\wedge {\mathrm{Proof}}_{T}({x}_{0},y)\wedge N({x}_{1},y,{x}_{2})\wedge \forall z<{x}_{0}\u200a\neg {\mathrm{Proof}}_{T}(z,{x}_{2})\right)$$Read this informally as
${x}_{0}$ is a proof of $y$ and there
is no shorter proof of the negation of $y$

. You
can think of a Rosser proof as a very special case of an ordinary proof that
gives more information. Obviously, for a consistent theory, if there
is an ordinary proof of a statement then there is a Rosser proof of
the same statement.

Let $G$ be a sentence such that

$$\text{DOR}\u22a2G\leftrightarrow \forall x\u200a\neg {\mathrm{RProof}}_{T}(x,\u231cG\u231d)$$(You might like to ask yourself, What, informally, does $G$ say?

and
what about $\neg G$?)

Exercise.

Prove that $\text{DOR}\u22a2\exists x\u200a{\mathrm{RProof}}_{T}(x,\u231c\theta \u231d)\iff T\u22a2\theta $.

Exercise.

Prove that $T\u22acG$.

Exercise.

Prove that $T\u22ac\neg G$.