Kurt Goedel (commonly spelled Godel, but it should really have an umlaut over the "o") proved that there are mathematical statements (or formulae) which have no proof. They cannot be proved true, they cannot be proved false. (And this is a stronger result than, "there are formulae that cannot be proved within the lifetime of this universe" - the result holds even if infinite time were available.) These statements are called undecidable. The result has trickled down into general consciousness these days, but at the time it was scandalous. "On Formally Undecidable Propositions of Principa Mathematics and Related Systems" is the title of the paper, and it is commonly called Godel's theorem.

He achieved his proof by formally constructing a mathematical statement, saying "This statement has no proof". He invented an ingenious method of encoding, called Godel numbering. Symbols, strings of symbols, axioms, and proofs were all encoded as numbers and mathematical operations. It was a mind-boggling accomplishment.

Godel's theorem could be considered the first step in a chain of questions. The first question is, "Is there such a thing as an undecidable formula (i.e. a formula with no proof of it's truth or falsehood)?" The answer is "yes", Godel showed an example. The second question would be "Is there such a thing as a *meta*undecidable formula (i.e. a formula with no proof of it's decidability or undecidability)?" I don't know the answer. If the answer is yes, it begs the third question, "Is there such a thing as a metametaundecidable formula?". As long as the answer is yes, there's another question to be asked. Is there only one "yes", the one Godel found? Is there an infinite number of "yes"es? Is there a finite number, and if so, how many steps to the last "yes"?