Definition
Alfred Tarski's undefinability theorem (1936): for any language rich enough to express arithmetic, there is no formula Tr(x) in the language such that for every sentence S, Tr(⌜S⌝) ↔ S (where ⌜S⌝ is the Gödel number of S). The truth predicate for a language cannot be defined inside the language. Truth must be defined in a strictly stronger meta-language.
Why it matters
How it works
Proof by diagonalization: suppose Tr(x) is definable in language L. By Gödel's self-reference construction, build a sentence λ in L whose decoded content is ¬Tr(⌜λ⌝) — "I am not true." Now ask whether λ is true. If yes, Tr(⌜λ⌝) holds, so ¬Tr(⌜λ⌝) is false, so λ is false. If no, Tr(⌜λ⌝) is false, so ¬Tr(⌜λ⌝) is true, so λ is true. Either way, contradiction. So Tr(x) cannot exist in L.