# G12. Understanding Godel's First Incompleteness Theorem - A Summary

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.