In 1931 the mathematician and logician Kurt Godel proved that within a formal system questions exist that are neither provable nor disprovable on the basis of the axioms that define the system. This is known as Godel's Undecidability Theorem. He also showed that in a sufficiently rich formal system in which decidability of all questions is required, there will be contradictory statements. This is known as his Incompleteness Theorem. In establishing these theorems Godel showed that there are problems that cannot be solved by any set of rules or procedures; instead for these problems one must always extend the set of axioms. This disproved a common belief at the time that the different branches of mathematics could be integrated and placed on a single logical foundation.
Alan Turing later provided a constructive interpretation of Godel's results by placing them on an algorithmic foundation: There are numbers and functions that cannot be computed by any logical machine.
More recently, Gregory Chaitin, a mathematician working at IBM, has stressed that Godel's and Turing's results set fundamental limits on mathematics.
These results, along with quantum uncertainty and the unpredictability of determinstic (chaotic) systems, form a core set of limitations to scientific knowledge that have only come to be appreciated during this century.
But waasn't he one of those [hushed anger] HOMOSEXUALISTS??? So anything that he discovered must be both wrong and evil, and you must be a liberal if you agree with him.[/loony science rejector mode]
For any formal theory T including basic arithmetical truths and also certain truths about formal provability (my emphasis), T includes a statement of its own consistency if and only if T is inconsistent. ...So, as I was saying, an implicit assumption of Godel's work is that only so-called finitistic proof methods are allowed.In 1936 Gerhard Gentzen proved the consistency of first order arithmetic. ... Gentzen showed that the consistency of first order arithmetic is provable, over the very weak base theory of primitive recursive arithmetic mentioned earlier, using the principle of quantifier free transfinite induction ...
Gentzen's proof also highlights one commonly missed aspect of Gödel's second incompleteness theorem. It's sometimes claimed that the consistency of a theory can only be proved in a stronger theory. The theory obtained by adding quantifier free transfinite induction to primitive recursive arithmetic proves the consistency of first order arithmetic but is not stronger than first order arithmetic. ... The resulting theory is not weaker than first order arithmetic either, since it can prove a number theoretical fact - the consistency of first order arithmetic - that first order arithmetic can't. The two theories are simply incomparable.