Rosser's trick begins with the assumptions of Gödel's incompleteness theorem. A theory ${\displaystyle T}$  is selected which is effective, consistent, and includes a sufficient fragment of elementary arithmetic.

Gödel's proof shows that for any such theory there is a formula ${\displaystyle \operatorname {Proof} _{T}(x,y)}$  which has the intended meaning that ${\displaystyle y}$  is a natural number code (a Gödel number) for a formula and ${\displaystyle x}$  is the Gödel number for a proof, from the axioms of ${\displaystyle T}$ , of the formula encoded by ${\displaystyle y}$ . (In the remainder of this article, no distinction is made between the number ${\displaystyle y}$  and the formula encoded by ${\displaystyle y}$ , and the number coding a formula ${\displaystyle \phi }$  is denoted ${\displaystyle \#\phi }$ .) Furthermore, the formula ${\displaystyle \operatorname {Pvbl} _{T}(y)}$  is defined as ${\displaystyle \exists x\operatorname {Proof} _{T}(x,y)}$ . It is intended to define the set of formulas provable from ${\displaystyle T}$ .

The assumptions on ${\displaystyle T}$  also show that it is able to define a negation function ${\displaystyle {\text{neg}}(y)}$ , with the property that if ${\displaystyle y}$  is a code for a formula ${\displaystyle \phi }$  then ${\displaystyle {\text{neg}}(y)}$  is a code for the formula ${\displaystyle \neg \phi }$ . The negation function may take any value whatsoever for inputs that are not codes of formulas.

The Gödel sentence of the theory ${\displaystyle T}$  is a formula ${\displaystyle \phi }$ , sometimes denoted ${\displaystyle G_{T}}$ , such that ${\displaystyle T}$  proves ${\displaystyle \phi }$  ↔${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )}$ . Gödel's proof shows that if ${\displaystyle T}$  is consistent then it cannot prove its Gödel sentence; but in order to show that the negation of the Gödel sentence is also not provable, it is necessary to add a stronger assumption that the theory is ω-consistent, not merely consistent. For example, the theory ${\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}}$ , in which PA is Peano axioms, proves ${\displaystyle \neg G_{T}}$ . Rosser (1936) constructed a different self-referential sentence that can be used to replace the Gödel sentence in Gödel's proof, removing the need to assume ω-consistency.

For a fixed arithmetical theory ${\displaystyle T}$ , let ${\displaystyle \operatorname {Proof} _{T}(x,y)}$  and ${\displaystyle {\text{neg}}(x)}$  be the associated proof predicate and negation function.

A modified proof predicate ${\displaystyle \operatorname {Proof} _{T}^{R}(x,y)}$  is defined as:

which means that

This modified proof predicate is used to define a modified provability predicate ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$ :

Informally, ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$  is the claim that ${\displaystyle y}$  is provable via some coded proof ${\displaystyle x}$  such that there is no smaller coded proof of the negation of ${\displaystyle y}$ . Under the assumption that ${\displaystyle T}$  is consistent, for each formula ${\displaystyle \phi }$  the formula ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$  will hold if and only if ${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$  holds, because if there is a code for the proof of ${\displaystyle \phi }$ , then (following the consistency of ${\displaystyle T}$ ) there is no code for the proof of ${\displaystyle \neg \phi }$ . However, ${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$  and ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$  have different properties from the point of view of provability in ${\displaystyle T}$ .

An immediate consequence of the definition is that if ${\displaystyle T}$  includes enough arithmetic, then it can prove that for every formula ${\displaystyle \phi }$ , ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )}$  implies ${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))}$ . This is because otherwise, there are two numbers ${\displaystyle n,m}$ , coding for the proofs of ${\displaystyle \phi }$  and ${\displaystyle \neg \phi }$ , respectively, satisfying both ${\displaystyle n<m}$  and ${\displaystyle m<n}$ . (In fact ${\displaystyle T}$  only needs to prove that such a situation cannot hold for any two numbers, as well as to include some first-order logic)

Using the diagonal lemma, let ${\displaystyle \rho }$  be a formula such that ${\displaystyle T}$  proves ρ ↔ ¬ Pvbl^R
_T(#ρ). ${\displaystyle \rho }$  ↔${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\rho )}$ . The formula ${\displaystyle \rho }$  is the Rosser sentence of the theory ${\displaystyle T}$ .

Let ${\displaystyle T}$  be an effective, consistent theory including a sufficient amount of arithmetic, with Rosser sentence ${\displaystyle \rho }$ . Then the following hold (Mendelson 1977, p. 160):

1. ${\displaystyle T}$  does not prove ${\displaystyle \rho }$ 
2. ${\displaystyle T}$  does not prove ${\displaystyle \neg \rho }$ 

In order to prove this, one first shows that for a formula ${\displaystyle y}$  and a number ${\displaystyle e}$ , if ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$  holds, then ${\displaystyle T}$  proves ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$ . This is shown in a similar manner to what is done in Gödel's proof of the first incompleteness theorem: ${\displaystyle T}$  proves ${\displaystyle \operatorname {Proof} _{T}(e,y)}$ , a relation between two concrete natural numbers; one then goes over all the natural numbers ${\displaystyle z}$  smaller than ${\displaystyle e}$  one by one, and for each ${\displaystyle z}$ , ${\displaystyle T}$  proves ${\displaystyle \neg \operatorname {Proof} _{T}(z,{\text{(neg}}(y))}$ , again, a relation between two concrete numbers.

The assumption that ${\displaystyle T}$  includes enough arithmetic (in fact, what is required is basic first-order logic) ensures that ${\displaystyle T}$  also proves ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$  in that case.

Furthermore, if ${\displaystyle T}$  is consistent and proves ${\displaystyle \phi }$ , then there is a number ${\displaystyle e}$  coding for its proof in ${\displaystyle T}$ , and there is no number coding for the proof of the negation of ${\displaystyle \phi }$  in ${\displaystyle T}$ . Therefore ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$  holds, and thus ${\displaystyle T}$  proves ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$ .

The proof of (1) is similar to that in Gödel's proof of the first incompleteness theorem: Assume ${\displaystyle T}$  proves ${\displaystyle \rho }$ ; then it follows, by the previous elaboration, that ${\displaystyle T}$  proves ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\rho )}$ . Thus ${\displaystyle T}$  also proves ${\displaystyle \neg \rho }$ . But we assumed ${\displaystyle T}$  proves ${\displaystyle \rho }$ , and this is impossible if ${\displaystyle T}$  is consistent. We are forced to conclude that ${\displaystyle T}$  does not prove ${\displaystyle \rho }$ .

The proof of (2) also uses the particular form of ${\displaystyle \operatorname {Proof} _{T}^{R}}$ . Assume ${\displaystyle T}$  proves ${\displaystyle \neg \rho }$ ; then it follows, by the previous elaboration, that ${\displaystyle T}$  proves ${\displaystyle \operatorname {Pvbl} _{T}^{R}({\text{neg}}\#(\rho ))}$ . But by the immediate consequence of the definition of Rosser's provability predicate, mentioned in the previous section, it follows that ${\displaystyle T}$  proves ${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}$ . Thus ${\displaystyle T}$  also proves ${\displaystyle \rho }$ . But we assumed ${\displaystyle T}$  proves ${\displaystyle \neg \rho }$ , and this is impossible if ${\displaystyle T}$  is consistent. We are forced to conclude that ${\displaystyle T}$  does not prove ${\displaystyle \neg \rho }$ .

• Mendelson (1977), Introduction to Mathematical Logic
• Smorynski (1977), "The incompleteness theorems", in Handbook of Mathematical Logic, Jon Barwise, Ed., North Holland, 1982, ISBN 0-444-86388-5
• Barkley Rosser (September 1936). "Extensions of some theorems of Gödel and Church". Journal of Symbolic Logic. 1 (3): 87–91. doi:10.2307/2269028. JSTOR 2269028. S2CID 36635388.

• Avigad (2007), "Computability and Incompleteness", lecture notes.