Godel's First Incompleteness Theorem
Gödel's First Incompleteness Theorem is a theorem that asserts that any axiomatic theory 
, 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).
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 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 is consistent (i.e. it can prove any statement using only its axioms). Then there is a Turing machine 
that, given (an encoding of) some Turing machine 
and some input 
, (effectively) searches through every valid proof or disproof in , of which there are only countably many, until it finds a proof or disproof of ('s version of) the statement " eventually halts on input ". But we know that, since the halting problem is undecidable by Turing machines, there is some valid input 
on which cannot halt, and so the statement "
eventually halts on input 
" is unprovable in , and we are done.
