# Rosser's trick

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Rosser's_trick
> Markdown URL: https://mediated.wiki/source/Rosser's_trick.md
> Source: https://en.wikipedia.org/wiki/Rosser's_trick
> Source revision: 1302575377
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Method in mathematical logic

For the theorem about the sparseness of prime numbers, see [Rosser's theorem](/source/Rosser's_theorem).

In [mathematical logic](/source/Mathematical_logic), **Rosser's trick** is a method for proving a variant of [Gödel's incompleteness theorems](/source/G%C3%B6del's_incompleteness_theorems) not relying on the assumption that the theory being considered is [ω-consistent](/source/Omega-consistency) (Smorynski 1977, p. 840; Mendelson 1977, p. 160). This method was introduced by [J. Barkley Rosser](/source/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 T {\displaystyle T} is selected which is effective, consistent, and includes a sufficient fragment of [elementary arithmetic](/source/Elementary_arithmetic).

Gödel's proof shows that for any such theory there is a formula Proof T ⁡ ( x , y ) {\displaystyle \operatorname {Proof} _{T}(x,y)} which has the intended meaning that y {\displaystyle y} is a [natural number](/source/Natural_number) code (a Gödel number) for a formula and x {\displaystyle x} is the Gödel number for a proof, from the axioms of T {\displaystyle T} , of the formula encoded by y {\displaystyle y} . (In the remainder of this article, no distinction is made between the number y {\displaystyle y} and the formula encoded by y {\displaystyle y} , and the number coding a formula ϕ {\displaystyle \phi } is denoted # ϕ {\displaystyle \#\phi } .) Furthermore, the formula Pvbl T ⁡ ( y ) {\displaystyle \operatorname {Pvbl} _{T}(y)} is defined as ∃ x Proof T ⁡ ( x , y ) {\displaystyle \exists x\operatorname {Proof} _{T}(x,y)} . It is intended to define the set of formulas provable from T {\displaystyle T} .

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

The Gödel sentence of the theory T {\displaystyle T} is a formula ϕ {\displaystyle \phi } , sometimes denoted G T {\displaystyle G_{T}} , such that T {\displaystyle T} proves ϕ {\displaystyle \phi } ↔ ¬ Pvbl T ⁡ ( # ϕ ) {\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )} . Gödel's proof shows that if T {\displaystyle 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](/source/Omega-consistency), not merely consistent. For example, the theory T = PA + ¬ G P A {\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}} , in which PA is [Peano axioms](/source/Peano_axioms), proves ¬ G T {\displaystyle \neg 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.

## The Rosser sentence

For a fixed arithmetical theory T {\displaystyle T} , let Proof T ⁡ ( x , y ) {\displaystyle \operatorname {Proof} _{T}(x,y)} and neg ( x ) {\displaystyle {\text{neg}}(x)} be the associated proof predicate and negation function.

A modified proof predicate Proof T R ⁡ ( x , y ) {\displaystyle \operatorname {Proof} _{T}^{R}(x,y)} is defined as:

Proof T R ⁡ ( x , y ) ≡ Proof T ⁡ ( x , y ) ∧ ¬ ∃ z ≤ x [ Proof T ⁡ ( z , neg ⁡ ( y ) ) ] , {\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

¬ Proof T R ⁡ ( x , y ) ≡ Proof T ⁡ ( x , y ) → ∃ z ≤ x [ Proof T ⁡ ( z , neg ⁡ ( y ) ) ] . {\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 T R ⁡ ( y ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(y)} :

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

Informally, Pvbl T R ⁡ ( y ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(y)} is the claim that y {\displaystyle y} is provable via some coded proof x {\displaystyle x} such that there is no smaller coded proof of the negation of y {\displaystyle y} . Under the assumption that T {\displaystyle T} is consistent, for each formula ϕ {\displaystyle \phi } the formula Pvbl T R ⁡ ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} will hold if and only if Pvbl T ⁡ ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}(\#\phi )} holds, because if there is a code for the proof of ϕ {\displaystyle \phi } , then (following the consistency of T {\displaystyle T} ) there is no code for the proof of ¬ ϕ {\displaystyle \neg \phi } . However, Pvbl T ⁡ ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}(\#\phi )} and Pvbl T R ⁡ ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} have different properties from the point of view of provability in T {\displaystyle T} .

An immediate consequence of the definition is that if T {\displaystyle T} includes enough arithmetic, then it can prove that for every formula ϕ {\displaystyle \phi } , Pvbl T R ⁡ ( ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )} implies ¬ Pvbl T R ⁡ ( neg ( ϕ ) ) {\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))} . This is because otherwise, there are two numbers n , m {\displaystyle n,m} , coding for the proofs of ϕ {\displaystyle \phi } and ¬ ϕ {\displaystyle \neg \phi } , respectively, satisfying both n < m {\displaystyle n<m} and m < n {\displaystyle m<n} . (In fact T {\displaystyle T} only needs to prove that such a situation cannot hold for any two numbers, as well as to include some [first-order logic](/source/First-order_logic).)

Using the [diagonal lemma](/source/Diagonal_lemma), let ρ {\displaystyle \rho } be a formula such that T {\displaystyle T} proves ρ ⟺ ¬ Pvbl T R ⁡ ( # ρ ) {\displaystyle \rho \iff \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )} . The formula ρ {\displaystyle \rho } is the **Rosser sentence** of the theory T {\displaystyle T} .

## Rosser's theorem

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

1. T {\displaystyle T} does not prove ρ {\displaystyle \rho }

1. T {\displaystyle T} does not prove ¬ ρ {\displaystyle \neg \rho }

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

The assumption that T {\displaystyle T} includes enough arithmetic (in fact, what is required is basic first-order logic) ensures that T {\displaystyle T} also proves Pvbl T R ⁡ ( y ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(y)} in that case.

Furthermore, if T {\displaystyle T} is consistent and proves ϕ {\displaystyle \phi } , then there is a number e {\displaystyle e} coding for its proof in T {\displaystyle T} , and there is no number coding for the proof of the negation of ϕ {\displaystyle \phi } in T {\displaystyle T} . Therefore Proof T R ⁡ ( e , y ) {\displaystyle \operatorname {Proof} _{T}^{R}(e,y)} holds, and thus T {\displaystyle T} proves Pvbl T R ⁡ ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} .

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

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

## References

- [Mendelson](/source/Elliott_Mendelson) (1977), *Introduction to Mathematical Logic*

- Smorynski (1977), "The incompleteness theorems", in *Handbook of Mathematical Logic*, [Jon Barwise](/source/Jon_Barwise), Ed., North Holland, 1982, [ISBN](/source/ISBN_(identifier)) [0-444-86388-5](https://en.wikipedia.org/wiki/Special:BookSources/0-444-86388-5)

- Barkley Rosser (September 1936). ["Extensions of some theorems of Gödel and Church"](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/extensions-of-some-theorems-of-godel-and-church/0461E34DC1F219C459EE84CC2FA89068). *[Journal of Symbolic Logic](/source/Journal_of_Symbolic_Logic)*. **1** (3): 87–91. [doi](/source/Doi_(identifier)):[10.2307/2269028](https://doi.org/10.2307%2F2269028). [JSTOR](/source/JSTOR_(identifier)) [2269028](https://www.jstor.org/stable/2269028). [S2CID](/source/S2CID_(identifier)) [36635388](https://api.semanticscholar.org/CorpusID:36635388).

## External links

- Avigad (2007), "[Computability and Incompleteness](http://www.andrew.cmu.edu/user/avigad/Teaching/candi_notes.pdf)", lecture notes.

---
Adapted from the Wikipedia article [Rosser's trick](https://en.wikipedia.org/wiki/Rosser's_trick) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Rosser's_trick?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.