Rosser's trick

Rosser's trick begins with the assumptions of Gödel's incompleteness theorem. A theory 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 Proof_T(x,y) which has the intended meaning that y is a natural number code (a Gödel number) for a formula and x is the Gödel number for a proof, from the axioms of T, of the formula encoded by y. (In the remainder of this article, no distinction is made between the number y and the formula encoded by y, and the number coding a formula φ is denoted #φ). Furthermore, the formula Pvbl_T(y) is defined as ∃x Proof_T(x,y). It is intended to define the set of formulas provable from T.

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

The Gödel sentence of the theoryT is a formula φ, sometimes denoted G_T such that T proves φ ↔ ¬Pvbl_T(#φ). Gödel's proof shows that if 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 T=PA+¬G_PA proves ¬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 T, let Proof_T(x,y) and neg(x) be the associated proof predicate and negation function.

A modified proof predicate Proof^R_T(x,y) is defined as:

${\displaystyle \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))],}$

which means that

${\displaystyle \lnot \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\to \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))].}$

This modified proof predicate is used to define a modified provability predicate Pvbl^R_T(y):

${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)\equiv \exists x\operatorname {Proof} _{T}^{R}(x,y).}$

Informally, Pvbl^R_T(y) is the claim that y is provable via some coded proof x such that there is no smaller coded proof of the negation of y. Under the assumption that T is consistent, for each formula φ the formula Pvbl^R_T(#φ) will hold if and only if Pvbl_T(#φ) holds, because if there is a code for the proof of φ, then (following the consistency of T) there is no code for the proof of ¬φ. However, Pvbl_T and Pvbl^R_T have different properties from the point of view of provability in T.

An immediate consequence of the definition is that if T includes enough arithmetic, then it can prove that for every formula φ, Pvbl^R_T(φ) implies ¬Pvbl^R_T(neg(φ)). This is because otherwise, there are two numbers n,m, coding for the proofs of φ and ¬φ, respectively, satisfying both n<m and m<n. (In fact 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 ρ be a formula such that T proves ρ ↔ ¬ Pvbl^R_T(#ρ). The formula ρ is the Rosser sentence of the theory T.

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

1. T does not prove ρ
2. T does not prove ¬ρ.

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

The assumption that T includes enough arithmetic (in fact, what is required is basic first-order logic) ensures that T also proves Pvbl^R_T(y) in that case.

Furthermore, if T is consistent and proves φ, then there is a number e coding for its proof in T, and there is no number coding for the proof of the negation of φ in T. Therefore Proof^R_T(e,y) holds, and thus T proves Pvbl^R_T(#φ).

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

The proof of (2) also uses the particular form of Proof^R_T. Assume T proves ¬ρ; then it follows, by the previous elaboration, that T proves Pvbl^R_T(neg(#ρ)). But by the immedeate consequence of the definition of Rosser's provability predicate, mentioned in the previous section, it follows that T proves ¬Pvbl^R_T(#ρ). Thus T also proves ρ. But we assumed T proves ¬ρ, and this is impossible if T is consistent. We are forced to conclude that T does not prove ¬ρ.

• 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
• Rosser (1936), "Extensions of some theorems of Gödel and Church", Journal of Symbolic Logic, v. 1, pp. 87–91.

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