In mathematical logic, Rosser's trick is a method for proving Gödel's incompleteness theorems without the assumption that the theory being considered is ω-consistent. This method was introduced by J. Barkley Rosser in 1936, as an improvement of Gödel's original proof of the incompleteness theorems that was published in 1931. While Gödel's original proof uses a sentence that says "This sentence is not provable", Rosser's trick uses a formula that says "If this sentence is provable, there is a shorter proof of its negation".
Background
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 ProofT which has the intended meaning that y is a natural number code for a formula and x is the Gödel number for a proof, from the axioms of T, of the formula encoded by y.. Furthermore, the formula PvblT is defined as ∃x ProofT. 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, with the property that if y is a code for a formula φ then neg 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 GT such that T proves φ ↔ ¬PvblT. 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+¬GPA proves ¬GT. Rosser 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.
The Rosser sentence
For a fixed arithmetical theory T, let ProofT and neg be the associated proof predicate and negation function. A modified proof predicate ProofRT is defined as: which means that This modified proof predicate is used to define a modified provability predicate PvblRT: Informally, PvblRT 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 PvblRT will hold if and only if PvblT holds, because if there is a code for the proof of φ, then there is no code for the proof of ¬φ. However, PvblT and PvblRT 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 φ, PvblRT implies ¬PvblRT. This is because otherwise, there are two numbers n,m, coding for the proofs of φ and ¬φ, respectively, satisfying both n<m and m<n. Using the diagonal lemma, let ρ be a formula such that T proves ρ ↔ ¬ PvblRT. The formula ρ is the Rosser sentence of the theory T.
Rosser's theorem
Let T be an effective, consistent theory including a sufficient amount of arithmetic, with Rosser sentence ρ. Then the following hold :
T does not prove ρ
T does not prove ¬ρ.
In order to prove this, one first shows that for a formula y and a number e, if ProofRT holds, then T proves ProofRT. This is shown in a similar manner to what is done in Gödel's proof of the first incompleteness theorem: T proves ProofT, a relation between two concrete natural numbers; one then goes over all the natural numbers z smaller than eone by one, and for each z, T proves ¬ProofT, again, a relation between two concrete numbers. The assumption that T includes enough arithmetic ensures that T also proves PvblRT 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 ProofRT holds, and thus T proves PvblRT. The proof of 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 PvblRT. 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 also uses the particular form of ProofRT. Assume T proves ¬ρ; then it follows, by the previous elaboration, that T proves PvblRT. But by the immedeate consequence of the definition of Rosser's provability predicate, mentioned in the previous section, it follows that T proves ¬PvblRT. 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 ¬ρ.
