Diagonalization lemma

In mathematical logic, the diagonalization lemma states that for any well formed formula <math>\phi(x)<math>

with a free variable x, there is a sentence ψ such that

<math>P \vdash \psi\leftrightarrow\phi([\psi]) <math>

where [ψ] is the Gödel number for ψ.

Gödel's first incompleteness theorem can be proved via the diagonalization lemma.

It takes its name from Cantor's diagonal argument to prove that the real numbers are uncountable.