In mathematical logic, Rosser's trick is a method for proving a variant of Gödel's incompleteness theorems not relying on 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".
Rosser's trick begins with the assumptions of Gödel's incompleteness theorem.
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
is the Gödel number for a proof, from the axioms of
(In the remainder of this article, no distinction is made between the number
, and the number coding a formula
It is intended to define the set of formulas provable from
also show that it is able to define a negation function
The negation function may take any value whatsoever for inputs that are not codes of formulas.
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.
, in which PA is Peano axioms, proves
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
be the associated proof predicate and negation function.
This modified proof predicate is used to define a modified provability predicate
such that there is no smaller coded proof of the negation of
have different properties from the point of view of provability in
includes enough arithmetic, then it can prove that for every formula
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
is the Rosser sentence of the theory
be an effective, consistent theory including a sufficient amount of arithmetic, with Rosser sentence
Then the following hold (Mendelson 1977, p. 160): In order to prove this, one first shows that for a formula
This is shown in a similar manner to what is done in Gödel's proof of the first incompleteness theorem:
, again, a relation between two concrete numbers.
includes enough arithmetic (in fact, what is required is basic first-order logic) ensures that
, and there is no number coding for the proof of the negation of
But by the immediate consequence of the definition of Rosser's provability predicate, mentioned in the previous section, it follows that