[Overview] [Previous] [Next]

Formal Systems

Two thousand years ago, Euclid set a standard for rigor in geometrical proofs. The rest of mathematics has never succeeded in reaching this standard.

The required properties of a satisfactory formal system are that it be

A number of mathematicians have attempted to put mathematics on a firmer, more logical footing. A major effort was mounted at the end of the 19th century by Alfred North Whitehead and Bertrand Russell; their Principia Mathematica attempted to use axiomatic set theory to form a foundation for all of mathematics. This attempt foundered when it was discovered that set theory is not consistent.

Here is the now-famous problem that demolished the Principia Mathematica. Consider the set of all sets that do not have themselves as a member. Is this set a member of itself?

Kurt Gödel explored the very notions of completeness and consistency. He invented a numbering scheme (Gödel numbers) that allowed him to express proofs as numbers (much as we might consider a computer program to be a very large binary number). He was able to prove the following result:

If it is possible to prove, within a formal system, that the system is consistent, then the formal system is not, in fact, consistent.

Or, equivalently,

If a formal system is consistent, then it is impossible to prove (within the system) that it is consistent.

This result sets very definite limits on the kinds of things that we can know. In particular, it shows that any attempt to prove mathematics consistent is foredoomed to failure.

Copyright © 1996 by David Matuszek
Last modified Apr 17, 1996