> Let L be the language of [[first-order arithmetic]]. > Let N be the standard structure for L, i.e. N consists of the ordinary > set of natural numbers and their addition and multiplication. Each > sentence in L can be interpreted in N and then becomes either true > or false. > Each formula phi in L has a [[Gödel number]] g(phi). This is a natural number > that "encodes" <math>\varphi.</math> In that way, the language <math>L</math> > can talk about formulas in <math>L,</math> not just about numbers. Let > <math>T</math> denote the set of <math>L</math>-sentences true in > <math>N,</math> and <math>T^*</math> the set of Gödel numbers of the > sentences in <math>T.</math> The following theorem answers the question: Can > <math>T^*</math> be defined by a formula of first-order arithmetic?
> To prove the theorem, we proceed by contradiction and assume that an > L-formula True(n) exists which is true for the natural number n in N if > and only if n is the Gödel number of a sentence in L that is true in N. > We could then use True(n) to define a new L-formula S(m) which is true > for the natural number m if and only if m is the Gödel number of a > formula phi(x) (with a free variable x) such that phi(m) is false when > interpreted in N (i.e. the formula phi(x), when applied to its own Gödel > number, yields a false statement). If we now consider the Gödel number > g of the formula S(m), and ask whether the sentence S(g) is true in N, > we obtain a contradiction. > (This is known as a [[Diagonal lemma|diagonal argument]].)
