Godel's Incompleteness Theorems
Gödel's Incompleteness Theorems are two theorems published in 1931 by Kurt Gödel that show that all sufficiently strong first-order theories can never yield answers to all mathematical questions—they are incomplete.
Gödel's First Incompleteness Theorem: If T is any consistent, sound, recursively enumerable first-order theory containing the axioms of Peano Arithmetic, there is a sentence G_T such that T cannot prove G_T and such that T cannot prove ~G_T. This means that T is not complete: there is some statement (G_T) that cannot be proved or refuted in the theory T.
The statement G_T says "G_T is not provable in T". This statement is encoded in number theory—symbols of first-order logic are assigned numbers in such a way so that statements in logic can be viewed as statements about numbers. Further, this statement refers to itself; that this is possible is the key to Godel's argument.
Recursively enumerable (r.e.) theories are theories that can be written down in a mechanical way. The restriction to recursively enumerable theories is required, since it is easy to construct non-r.e. theories that are complete—for example, the theory that contains exactly all true statements of number theory is complete, but cannot be written down in a mechanical way.
The first incompleteness theorem is itself a theorem of Peano Arithmetic. A corollary of this fact, noted independently by John von Neumann and Gödel, is the:
Gödel's Second Incompleteness Theorem: If T is any consistent, sound, recursively enumerable first-order theory containing the axioms of Peano Arithmetic, then T cannot prove its own consistency. In particular, Peano Arithmetic cannot prove its own consistency. This means that the consistency of the axioms of Peano Arithmetic and stronger mathematical theories must be justified in other ways, usually by appealing to the fact that the axioms are obviously true or by appealing to the fact that no one has yet derived an inconsistency.
Incompleteness and God
Incompleteness is sometimes used to refute the existence of an omnipotent god: If God were omnipotent, he would act as an oracle (in the mathematical sense) for any mathematical theory. That is, he could decide for any statement S whether S or not-S were true, which contradicts incompleteness. This argument is a more formal version of the "Can God make a rock even He could not move" paradox.
On the other hand, the same Godel who formulated the Incompleteness Theorems used those same tools (Model Theory) to forge an onthological proof of God's existence.
Similarly, the existence of undecidable statements proves the illogic of atheistic attempts to demand proof for the existence of God. Because we know that there exist true statements that we can never logically prove, there are necessarily things that must be believed on the basis of faith, rather than logic. The atheistic mantra that "the burden of proof lies with the believer" ignores this classic result in mathematical logic, and exposes their ignorance. It is notable that Kurt Godel who demonstrated the existence of undecidability in mathematical logic was a devoutly religious man.