Godel’s incompleteness theorems are two results, proved by Kurt Godel in 1931, that set fundamental limits on formal reasoning. They apply to any formal system that is consistent and powerful enough to carry out a certain amount of elementary arithmetic.
The first incompleteness theorem, as stated by the Stanford Encyclopedia of Philosophy, says that “any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.” In other words, there are true arithmetical statements that the system cannot prove.
The second incompleteness theorem strengthens this by turning the limit on the system itself: “for any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.” A system strong enough to do arithmetic cannot establish its own freedom from contradiction.
Godel’s method, presented in his 1931 paper “On Formally Undecidable Propositions of Principia Mathematica and Related Systems,” encoded statements about a formal system as numbers within that system, allowing the system to refer to its own provability. This idea of representing logic and computation as data anticipated themes that became central to the theory of computability and the design of stored-program computers.