Godel's First Incompleteness Theorem

Gödel's First Incompleteness Theorem is a theorem that asserts that any axiomatic theory $F$, which can prove anything that Peano arithmetic can, is either inconsistent (i.e. it can both prove and disprove any given statement) or incomplete (i.e. there is a statement that it cannot prove nor disprove using the axioms only), or trivial (like $0=1=\infty$).

The theorem is closely related to both Godel's Completeness Theorem (that a theory is consistent iff it has a model) and Godel's Second Incompleteness Theorem (that a consistent theory cannot prove its own consistency).

Proof

Firstly, suppose that $F$ is inconsistent; i.e. it proves a contradiction. Then, by ex falso quodlibet, we can use that contradiction to prove any statement.

Now suppose that $F$ is consistent (i.e. it can prove any statement using only its axioms). Then there is a Turing machine $T$ that, given (an encoding of) some Turing machine $T'$ and some input $x$, (effectively) searches through every valid proof or disproof in $F$, of which there are only countably many, until it finds a proof or disproof of ($F$'s version of) the statement "$T'$ eventually halts on input $x$". But we know that, since the halting problem is undecidable by Turing machines, there is some valid input $(T^*, x^*)$ on which $T'$ cannot halt, and so the statement "$T^*$ eventually halts on input $x^*$" is unprovable in $F$, and we are done.

See also