<logic> Any of many theorems proved by Kurt Goedel. The following three are normally named after Goedel. When one hears simply "Goedel's theorem" it usually refers to the first incompleteness theorem.
Goedel's completeness theorem (1930).
First-order polyadic predicate logic is semantically complete, that is, all logically valid wffs are theorems.
Goedel's first incompleteness theorem (1931).
Roughly, any consistent or omega-consistent formal system of arithmetic of "sufficient strength" is incomplete (negation incomplete and omega-incomplete). To be of sufficient strength, the system must (1) have decidable sets of wffs and proofs, and (2) represent every decidable set of natural numbers.
See arithmetic, formal systems of, representation of a set
Goedel's second incompleteness theorem (1931).
The consistency of a system of "sufficient strength" (same as for the first incompleteness theorem) is not provable in the system, unless the system is inconsistent. The second incompleteness theorem is a corollary of the first.
See Hilbert's program
[Glossary of First-Order Logic]
Try this search on OneLook / Google