In mathematical logic, the diagonalization lemma states that for any well formed formula φ(x)

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

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.