The Gödel-Rosser incompleteness theorem

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

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

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=⟨x_0,x_1,x_2⟩$ 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

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

(You might like to ask yourself, What, informally, does $G$ say? and what about $\neg G$?)