Rosser's trick
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 (Smorynski 1977, p. 840; Mendelson 1977, p. 160). 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 (informally) "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 formula_1 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 formula_2 which has the intended meaning that formula_3 is a natural number code (a Gödel number) for a formula and formula_4 is the Gödel number for a proof, from the axioms of formula_1, of the formula encoded by formula_3. (In the remainder of this article, no distinction is made between the number formula_3 and the formula  encoded by formula_3, and the number coding a formula formula_9 is denoted formula_10). Furthermore, the formula formula_11 is defined as formula_12. It is intended to define the set of formulas provable from formula_1. The assumptions on formula_1 also show that it is able to define a negation function formula_15, with the property that if formula_3 is a code for a formula formula_9 then formula_15 is a code for the formula formula_19. The negation function may take any value whatsoever for inputs that are not codes of formulas. The Gödel sentence of the theory formula_1 is a formula formula_9, sometimes denoted  formula_22, such that formula_1 proves formula_9 ↔formula_25. Gödel's proof shows that if formula_1 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 formula_27, in which PA is Peano axioms, proves formula_28. 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. The Rosser  sentence. For a fixed arithmetical theory formula_1, let formula_2 and formula_31 be the associated proof predicate and negation function. A modified proof predicate formula_32 is defined as: which means that This modified proof predicate is used to define a modified provability predicate:formula_35: Informally, formula_35 is the claim that formula_3 is provable via some coded proof formula_4 such that there is no smaller coded proof of the negation of formula_3. Under the assumption that formula_1 is consistent, for each formula formula_9 the formula formula_43 will hold if and only if formula_44 holds, because if there is a code for the  proof of formula_9, then (following the consistency of formula_1) there is no code for the proof of formula_19. However, formula_44 and formula_43 have different properties from the point of view of provability in formula_1. An immediate consequence of the definition is that if formula_1 includes enough arithmetic, then it can prove that for every formula formula_9, formula_53 implies formula_54. This is because otherwise, there are two numbers formula_55, coding for the proofs of formula_9 and formula_19, respectively, satisfying both formula_58 and formula_59. (In fact formula_1 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 formula_61 be a formula such that formula_1 proves ρ ↔ ¬ Pvbl(#ρ). formula_61 ↔formula_64. The formula formula_61 is the Rosser sentence of the theory formula_1. Rosser's theorem. Let formula_1 be an effective, consistent theory including a sufficient amount of arithmetic, with Rosser sentence formula_61. Then the following hold (Mendelson 1977, p. 160): In order to prove this, one first shows that for a formula formula_3 and a number formula_74, if formula_75 holds, then formula_1 proves formula_75. This is shown in a similar manner to what  is done in Gödel's proof of the first incompleteness theorem: formula_1 proves formula_79, a relation between two concrete natural numbers; one then goes over all the natural numbers formula_80 smaller than formula_74 one by one, and for each formula_82, formula_1 proves formula_84, again, a relation between two concrete numbers. The assumption that formula_1 includes enough arithmetic (in fact, what is required is basic first-order logic) ensures that formula_1 also proves formula_35 in that case. Furthermore, if formula_1 is consistent and proves formula_9, then there is a number formula_74 coding for its proof in formula_1, and there is no  number coding for the proof of the negation of formula_9 in formula_1. Therefore formula_75 holds, and thus formula_1 proves formula_43. The proof of (1) is similar to that in Gödel's proof of the first incompleteness theorem: Assume formula_1 proves formula_61; then it follows, by the previous elaboration, that formula_1 proves formula_100. Thus formula_1 also proves formula_72. But we assumed formula_1 proves formula_61, and this is impossible if formula_1 is consistent. We are forced to conclude that formula_1 does not prove formula_61. The proof of (2) also uses the particular form of formula_108. Assume formula_1 proves formula_72; then it follows , by the previous elaboration, that formula_1 proves formula_112. But by the immediate consequence of the definition of Rosser's provability predicate, mentioned in the previous section, it follows that formula_1 proves formula_114. Thus formula_1 also proves formula_61. But we assumed formula_1 proves formula_72, and this is impossible if formula_1 is consistent. We are forced to conclude that formula_1 does not prove formula_72.