On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Someone left a nodeshell here. All right, I'll bite.

This was the title of Kurt Gödel's famous paper where he proved that any finite formal system of sufficient power to be meaningful necessarily contains "undecidable propositions", that is, well-formed formulas for which a proof of truth or falsity could not be generated using the system in question. See Also: Gödel's Incompleteness Theorem

This paper dashed the hopes of the formalists, led by David Hilbert, who thought all mathematics could be brought under a program of formal systems. Principia Mathematica was the mammoth attempt by Bertrand Russell and Alfred North Whitehead to do just that.

Or, in the original German, ``Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme''. The theorem proved therein is also known as Gödel's Incompleteness Theorem.

The proof of incompleteness assumes, of course, that said formal system is consistent.

Yes, outside links are naughty, but see http://www.ddc.net/ygg/etext/godel/index.htm