If you’ve read through the entire Godel series thus far, you now have the prerequisite knowledge to precisely understand that statement that Godel’s first incompleteness theorem is making.

Here, again, is Godel’s first incompleteness theorem:

Any consistent formal system F that is sufficiently strong is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.

This theorem pertains only to formal systems, which are very rigid systems in which one starts from a set of axioms and transforms them using the predefined transformation rules of the system to derive more theorems. The theorem is not making a statement about informal proofs which are allowed to use any assumptions or leaps of logic that seem “obviously true”. Formal systems in isolation can be somewhat meaningless, but they are usually designed with an interpretation in mind. One can use such an interpretation to translate formulas within a formal system into mathematical statements.

Furthermore, this theorem is dealing with sufficiently strong formal systems, by which we mean that the formal system can capture all primitive recursive relations.

The theorem says that if such a formal system is consistent, meaning that there are no formulas \(\varphi\) for which it can derive both \(\varphi\) and its negation \(\lnot \varphi\), then it is incomplete, meaning that there exists some formula \(\varphi\) for which it cannot derive either \(\varphi\) or \(\lnot \varphi\).

The important implication of this is that one of \(\varphi\) or \(\lnot \varphi\) must be true, so if the formal system can derive neither, then there exists a true statement that the formal system can express, but not derive.

Why is that so surprising?

I personally find it quite intuitive (although apparently wrong) that “mathematical truth” and “provable” are two ways of saying the same thing. Before studying Godel, if someone had told me that there was a true statement which was “unprovable”, I’d be pretty confused as to what they meant by “true”. How are you sure it’s true if you can’t prove it?

Now having a deeper understanding of Godel’s work, I understand there are a few problems with that line of thought. For one, provable using what initial assumptions? Every proof has to start somewhere, and those are the starting axioms that you assume to be true.

I also now know that one way to show that a “true” statement is unprovable is by showing that neither it nor it’s negation can be proven. The beauty of this technique is that sidesteps the problem of having to somehow show that a statement is true without being able to prove it. Instead, all you need to agree on is that one of X or “not X” must be true. If a system can prove neither, then there exists a true statement that it cannot prove.

I want to quickly clarify that Godel’s theorem does not say that there are true statements that cannot be proven under any formal system. Just that, for a given formal system, there exist true statements that cannot be proven. It’s a subtle distinction, but an important one. It means that we cannot find a single set of initial assumptions (and transformation rules) from which to derive all mathematical truths. We may be able to derive all truths, but different truths may need different starting assumptions. You have to admit, something feels very unsatisfying about that.

If you find this extremely counterintuitive, you’re not alone. As explained in Why do we care about formal systems?, finding a single set of initial assumptions from which to derive all mathematical truths was not some unrealistic ideal that no mathematicians found plausible. On the contrary, in the early 1900’s many of the world’s foremost mathematicians were explicitly working towards this goal.

So, when Godel published his paper On Formally Undecidable Propositions of Principia Mathematica And Related Systems, it seriously shocked the mathematical community. In a single instant, the goal of finding a single formal system on which all math could be based - likely the life’s work of many mathematicians at the time - was shown to be unattainable. Scientifically minded people often say that being proven wrong is a gift because it’s in those moments when you learn the most. Even so, I suspect that this was a tough pill for some to swallow.

The proof

In a future series of posts we will outline how Godel actually went about proving this theorem.