Gödel's incompleteness theorems

Gödel's incompleteness theorems is the name given to two theorems, proved by Kurt Gödel in 1931. They are about limitations in all but the most trivial formal systems for arithmetic of mathematical interest. The theorems are very important for the philosophy of mathematics. The idea behind the theorems is that some mathematical systems are not complete. Most people think they show that Hilbert's program to find a complete and consistent set of axioms for all of mathematics is impossible. This would give a negative answer to Hilbert's second problem.

In a formal system, there are axioms. All axioms are supposed to be true, even without a proof. A theorem then serves to come up with other true statements from the axioms, using certain rules. A sequence of such statements is called a proof of a statement, because it shows that the statement is true under all circumstances. Ideally, it should be possible to construct all true statements in the formal system in that manner. A system that has this property is called complete, one that does not is called incomplete. Another thing wanted of a theory is that there should be no contradictions. This means that it is not possible to prove that a statement is true and false at the same time. A system that does not include theories that allow this is called consistent.

Gödel said that every non-trivial formal system is either incomplete or inconsistent.

The first theorem says that for a given (non-trivial) formal system, there will be statements that are true in that system, but that they cannot be proved to be true inside the system. The second theorem says that if a system can be proved to be consistent using its own logic, then there will be a theorem in the system that is contradictory.