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".

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 theory T 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.

...
Wikipedia