In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, 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
John Barkley Rosser Sr. (December 6, 1907 – September 5, 1989) was an American logician, a student of Alonzo Church, and known for his part in the Church–Rosser theorem, in lambda calculus. He also developed what is now called the "Rosser siev ...
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
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
which has the intended meaning that
is a natural number code (a Gödel number) for a formula and
is the Gödel number for a proof, from the axioms of
, of the formula encoded by
. (In the remainder of this article, no distinction is made between the number
and the formula encoded by
, and the number coding a formula
is denoted
.) Furthermore, the formula
is defined as
. It is intended to define the set of formulas provable from
.
The assumptions on
also show that it is able to define a negation function
, with the property that if
is a code for a formula
then
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
is a formula
, sometimes denoted
, such that
proves
↔
. Gödel's proof shows that if
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
, in which PA is
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
, 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.
The Rosser sentence
For a fixed arithmetical theory
, let
and
be the associated proof predicate and negation function.
A modified proof predicate
is defined as:
which means that
This modified proof predicate is used to define a modified provability predicate
:
Informally,
is the claim that
is provable via some coded proof
such that there is no smaller coded proof of the negation of
. Under the assumption that
is consistent, for each formula
the formula
will hold if and only if
holds, because if there is a code for the proof of
, then (following the consistency of
) there is no code for the proof of
. However,
and
have different properties from the point of view of provability in
.
An immediate consequence of the definition is that if
includes enough arithmetic, then it can prove that for every formula
,
implies
. This is because otherwise, there are two numbers
, coding for the proofs of
and
, respectively, satisfying both