As a consequence, a certain equivalence is a theorem of T. This equivalence has the form "G holds if and only if the formula satisfying ... is not a theorem of T", where the formula satisfying ... is in fact the formula G itself. This equivalence is what is used in Gödel's proof of the incompleteness theorem.

Thus it makes good sense to say that the Gödel sentence G is self-referential, and there is no mystery about how sentences that are in this sense self-referential can be constructed (in various ways) for different theories T.

Gödel's original proof of his theorem, using the Gödel sentence G, is vivid and memorable, but it has given many people the incorrect impression that G must be used to prove the incompleteness theorem for T, or that sentences undecidable in T must be in this sense self-referential.

To counter this impression, it is a good idea to be aware that ordinary mathematical theories T - formalized arithmetic, analysis, set theory - can be proved incomplete (if sound) without invoking any self-referential sentences. One such proof goes as follows.

A *Diophantine equation* is an equation of the form
p(x_{1},..x_{n})=0, where
p(x_{1},..x_{n}) is a polynomial with
integer coefficients. For example,
11x^{5}-38xy^{8}+18133=0 is a Diophantine
equation. A *solution* of such an equation is an n-tuple of
integers x_{1},..x_{n}, such that
p(x_{1},..x_{n})=0. For example, the triple 3,4,5 is a
solution of the equation x^{2}+y^{2}=z^{2}.

Solving Diophantine equations - i.e. finding their solutions or showing that they have no solutions - is a classical and difficult area in mathematics. It is a consequence of a theorem in logic that there is no general algorithm for solving every such problem, or even for deciding whether or not a given Diophantine equation has any solution at all. This logical fact can (after some tweaking, which is omitted here for simplicity) be formulated as follows:

There is no way of mechanically generating those and only those Diophantine equations P=0 that have no solution.Now a characteristic of formalized mathematical theories T is that there is a way of mechanically generating their theorems. A "theorem proving machine" can be defined which churns out all the statements formally provable in the theory. Such a procedure is mostly useless in practice, but theoretically, we know that the theorems of T can be in this way mechanically generated. Therefore, if we have a formalized theory T of arithmetic, we know that there is a way of mechanically generating those Diophantine equations P=0 for which it is

Thus, we can conclude from the logical fact quoted that unless T proves "P=0 has no solution" for some equation which in fact has a solution (which, by a simple argument omitted here, implies that T is inconsistent), there must be some Diophantine equation without solutions for which this fact cannot be proved in T.

We have, therefore, an improved version of Gödel's theorem for these T: if T is consistent, then some true statement of the form "the Diophantine equation P=0 has no solution" is not provable in T. (And, unless T proves false statements about Diophantine equations, the statement isn't disprovable either.) Keeping this version in mind will remind us that proving Gödel's theorem need not involve the use of self-referential statements.

Note that it is quite irrelevant to this simple argument whether there is any mechanism for expressing self-reference in T. No self-referential sentence in the language of T is introduced or invoked in the argument. All that is required is that T is consistent, and that the theorems of T can be mechanically generated.

The essence of diagonalization is found in the following simple argument: let P(x,y) be a two-place relation, and define a one-place predicate D(x) by

D(x) if and only if not P(x,x)Then D is not equal to any of the predicates P

PThis is so because D is disagrees with every such predicate P_{x}(y) if and only if P(x,y)

Informally, it seems safe to say that some form of diagonalization is used, directly or indirectly, in all known proofs of Gödel's theorem.

*A qualification*: The above comment is based on the standard
semantic, recursion-theoretic or model theoretic proofs known to me of
Gödel's second theorem, or of the first theorem in the form that
proves the undecidability of a statement of the form "For every
natural number k, P(k)" where P is a computable predicate. However,
there are also proofs of the undecidability in arithmetical theories
of logically more complicated statements, and it is not at all clear
that such proofs need to rely on diagonalization. A technical exposition of such a proof, by Kripke.

Now, many feel inclined to say that diagonalization too is a form of self-reference. It may well be possible to give a more precise content to this inclination by giving a suitable definition of "self-reference" and showing that it applies to diagonalization. What has been argued above is only that it is not necessary, in order to prove Gödel's (first) incompleteness theorem for a theory T, to assume that any self-referential statement in the sense defined above can be formulated in T, and that no self-referential statement (again in the sense defined) is used in a proof by diagonalization of the logical fact about Diophantine equations referred to above.