Any consistent, sufficiently powerful formal system is incomplete. Such a system cannot prove its own consistency. Applies to ZFC. Uses arithmetization and diagonalization.