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 metaundecidable 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"?

In the theory of computation, a problem is said to be undecidable if it is a yes/no problem with infinitely many instances, and no algorithm exists that answers the problem for all instances correctly.

Alan Turing invented the Turing machine in order to prove the existence of undecidable problems; in particular, the undecideability of the halting problem, the question whether or not a given Turing machine will eventually halt its operation on a given input.

His work, published in 1936, is closely related to Kurt Gödel's earlier (1930) work on the incompleteness of mathematical logic.

Log in or register to write something here or to contact authors.