{{Short description|Method in mathematical logic}} {{For|the theorem about the sparseness of prime numbers|Rosser's theorem}}
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 [[Omega-consistency|ω-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 <math>T</math> 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 <math>\operatorname{Proof}_T(x,y)</math> which has the intended meaning that <math>y</math> is a [[natural number]] code (a Gödel number) for a formula and <math>x</math> is the Gödel number for a proof, from the axioms of <math>T</math>, of the formula encoded by <math>y</math>. (In the remainder of this article, no distinction is made between the number <math>y</math> and the formula encoded by <math>y</math>, and the number coding a formula <math>\phi</math> is denoted <math>\#\phi</math>.) Furthermore, the formula <math>\operatorname{Pvbl}_T(y)</math> is defined as <math> \exists x\operatorname{Proof}_T(x,y)</math>. It is intended to define the set of formulas provable from <math>T</math>.
The assumptions on <math>T</math> also show that it is able to define a negation function <math>\text{neg}(y)</math>, with the property that if <math>y</math> is a code for a formula <math>\phi</math> then <math>\text{neg}(y)</math> is a code for the formula <math>\neg \phi</math>. The negation function may take any value whatsoever for inputs that are not codes of formulas.
The Gödel sentence of the theory <math>T</math> is a formula <math>\phi</math>, sometimes denoted <math>G_T</math>, such that <math>T</math> proves <math>\phi</math> ↔<math>\neg \operatorname{Pvbl}_T(\#\phi)</math>. Gödel's proof shows that if <math>T</math> 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 [[omega-consistency|ω-consistent]], not merely consistent. For example, the theory <math>T=\text{PA}+\neg \text{G}_{PA}</math>, in which PA is [[Peano axioms]], proves <math>\neg G_T</math>. 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 <math>T</math>, let <math>\operatorname{Proof}_T(x,y)</math> and <math>\text{neg}(x)</math> be the associated proof predicate and negation function.
A modified proof predicate <math>\operatorname{Proof}^R_T(x,y)</math> is defined as:
<math display="block">\operatorname{Proof}^R_T(x,y) \equiv \operatorname{Proof}_T(x,y) \land \lnot \exists z \leq x [ \operatorname{Proof}_T(z,\operatorname{neg}(y))],</math>
which means that
<math display="block">\lnot \operatorname{Proof}^R_T(x,y) \equiv \operatorname{Proof}_T(x,y) \to \exists z \leq x [ \operatorname{Proof}_T(z,\operatorname{neg}(y))].</math>
This modified proof predicate is used to define a modified provability predicate <math>\operatorname{Pvbl}^R_T(y)</math>:
<math display="block">\operatorname{Pvbl}^R_T(y) \equiv \exists x \operatorname{Proof}^R_T(x,y).</math>
Informally, <math>\operatorname{Pvbl}^R_T(y)</math> is the claim that <math>y</math> is provable via some coded proof <math>x</math> such that there is no smaller coded proof of the negation of <math>y</math>. Under the assumption that <math>T</math> is consistent, for each formula <math>\phi</math> the formula <math>\operatorname{Pvbl}^R_T(\#\phi)</math> will hold if and only if <math>\operatorname{Pvbl}_T(\#\phi)</math> holds, because if there is a code for the proof of <math>\phi</math>, then (following the consistency of <math>T</math>) there is no code for the proof of <math>\neg \phi</math>. However, <math>\operatorname{Pvbl}_T(\#\phi)</math> and <math>\operatorname{Pvbl}^R_T(\#\phi)</math> have different properties from the point of view of provability in <math>T</math>.
An immediate consequence of the definition is that if <math>T</math> includes enough arithmetic, then it can prove that for every formula <math>\phi</math>, <math>\operatorname{Pvbl}^R_T(\phi)</math> implies <math>\neg \operatorname{Pvbl}^R_T(\text{neg}(\phi))</math>. This is because otherwise, there are two numbers <math>n,m</math>, coding for the proofs of <math>\phi</math> and <math>\neg \phi</math>, respectively, satisfying both <math>n<m</math> and <math>m<n</math>. (In fact <math>T</math> 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 <math>\rho</math> be a formula such that <math>T</math> proves <math>\rho\iff\neg \operatorname{Pvbl}_T^R(\#\rho)</math>. The formula <math>\rho</math> is the '''Rosser sentence''' of the theory {{nowrap|<math>T</math>.}}
== Rosser's theorem == Let <math>T</math> be an effective, consistent theory including a sufficient amount of arithmetic, with Rosser sentence <math>\rho</math>. Then the following hold (Mendelson 1977, p. 160): # <math>T</math> does not prove <math>\rho</math> # <math>T</math> does not prove <math>\neg \rho</math>
In order to prove this, one first shows that for a formula <math>y</math> and a number <math>e</math>, if <math>\operatorname{Proof}^R_T(e,y)</math> holds, then <math>T</math> proves <math>\operatorname{Proof}^R_T(e,y)</math>. This is shown in a similar manner to what is done in Gödel's proof of the first incompleteness theorem: <math>T</math> proves <math>\operatorname{Proof}_T(e,y)</math>, a relation between two concrete natural numbers; one then goes over all the natural numbers <math>z</matH> smaller than <math>e</math> one by one, and for each <math>z</math>, <math>T</math> proves <math>\neg \operatorname{Proof}_T(z, \text{(neg}(y))</math>, again, a relation between two concrete numbers.
The assumption that <math>T</math> includes enough arithmetic (in fact, what is required is basic first-order logic) ensures that <math>T</math> also proves <math>\operatorname{Pvbl}^R_T(y)</math> in that case.
Furthermore, if <math>T</math> is consistent and proves <math>\phi</math>, then there is a number <math>e</math> coding for its proof in <math>T</math>, and there is no number coding for the proof of the negation of <math>\phi</math> in <math>T</math>. Therefore <math>\operatorname{Proof}^R_T(e,y)</math> holds, and thus <math>T</math> proves <math>\operatorname{Pvbl}^R_T(\#\phi)</math>.
The proof of (1) is similar to that in Gödel's proof of the first incompleteness theorem: Assume <math>T</math> proves <math>\rho</math>; then it follows, by the previous elaboration, that <math>T</math> proves <math>\operatorname{Pvbl}^R_T(\#\rho)</math>. Thus <math>T</math> also proves <math>\neg \rho</math>. But we assumed <math>T</math> proves <math>\rho</math>, and this is impossible if <math>T</math> is consistent. We are forced to conclude that <math>T</math> does not prove <math>\rho</math>.
The proof of (2) also uses the particular form of <math>\operatorname{Proof}^R_T</math>. Assume <math>T</math> proves <math>\neg \rho</math>; then it follows, by the previous elaboration, that <math>T</math> proves <math>\operatorname{Pvbl}^R_T(\text{neg}\#(\rho))</math>. But by the immediate consequence of the definition of Rosser's provability predicate, mentioned in the previous section, it follows that <math>T</math> proves <math>\neg \operatorname{Pvbl}^R_T(\#\rho)</math>. Thus <math>T</math> also proves <math>\rho</math>. But we assumed <math>T</math> proves <math>\neg \rho</math>, and this is impossible if <math>T</math> is consistent. We are forced to conclude that <math>T</math> does not prove <math>\neg \rho</math>.
== References == * [[Elliott Mendelson|Mendelson]] (1977), ''Introduction to Mathematical Logic'' * Smorynski (1977), "The incompleteness theorems", in ''Handbook of Mathematical Logic'', [[Jon Barwise]], Ed., North Holland, 1982, {{isbn|0-444-86388-5}} * {{cite journal | jstor=2269028 | url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/extensions-of-some-theorems-of-godel-and-church/0461E34DC1F219C459EE84CC2FA89068 | author=Barkley Rosser | title=Extensions of some theorems of Gödel and Church | journal=[[Journal of Symbolic Logic]] | volume=1 | number=3 | pages=87–91 | date=September 1936 | doi=10.2307/2269028 | s2cid=36635388 | url-access=subscription }}
== External links == * Avigad (2007), "[http://www.andrew.cmu.edu/user/avigad/Teaching/candi_notes.pdf Computability and Incompleteness]", lecture notes.
[[Category:Mathematical logic]]