At the 1900 International Congress of Mathematicians, David Hilbert proposed twenty-three problems that shaped mathematical research in the 20th century. To bolster his axiomatic approach, he proposed "proving the consistency of Peano arithmetic": in other words, the axioms of arithmetic and the rules of formal deduction cannot yield both a statement and its negation. That is only common sense, you might say: either "2 + 2 = 5" or it does not! Yet no one had proved this in such generality before Hilbert posed the problem—and thirty years later, Kurt Gödel proved it false!
In fact, the Austrian logician proved much more: in any axiomatic system containing the Peano axioms, there are statements that can neither be proved nor disproved. Mathematicians already knew this to be the case in geometry. The parallel postulate cannot be proved from Euclid's other axioms of geometry. Today, this axiom is stated as follows: "Given a point A and a line D, exactly one line through A is parallel to D."
Replacing it with an axiom denying the existence of parallel lines produces another geometry, spherical geometry. Replacing it with an axiom asserting the existence of several parallel lines produces hyperbolic geometry.
Unprovable statements ---------------------------
Once we take account of the time and energy available to us, it is easy to prove that some statements are humanly impossible to prove or disprove. Such statements are said to be undecidable. To see this, we need only consider the length of a proof. There are infinitely many provable statements—for example, statements of the form "the number n is prime"—and their proofs are distinct, so proofs can be arbitrarily long. Beyond a certain length—10100, for example, which is greater than the number of electrons in the universe—a proof may be regarded as beyond human reach, even with the aid of a powerful computer. This is merely common sense, but Gödel's claim goes much further. Arithmetic, with the Peano axioms, contains undecidable statements—and he gives explicit examples. The example in the box might suggest that the problem arises because an axiom—here, the axiom of choice—has been "left out" of Peano arithmetic. You may add it, but Gödel's theorem ensures that other unprovable statements will exist in the new system, and so on. Adding new axioms can never circumvent Gödel's result.