We’ve spent the last two posts understanding formal systems, so it might worth taking a step back and asking the question: “why do we care about formal systems?”.

Godel’s first incompleteness theorem tells us that consistent formal systems are incomplete, but what if formal systems are uninteresting in the first place? If all you’ve ever seen are the toy examples from my previous posts, it may not be very interesting or surprising that they have limitations.

Many of the most influential mathematicians of the 19th and 20th centuries did not take this view. In fact, their explicit mission was to put all of mathematics on solid foundations by constructing a formal system in which one could derive the rest of mathematics! David Hilbert was one such mathematician who formulated Hilbert’s Program. Another attempt was Principia Mathematica by Alfred North Whitehead and Bertrand Russell. These dreams were, of course, dashed by Godel in 1931 - but the fact that the preeminent mathematicians of the time were making it their life’s work to find a formal system on which to base all other mathematics should tell you that formal systems can be quite interesting and powerful and that Godel’s result came as quite a surprise.

That is essentially an appeal to second order knowledge; very smart people thought formal systems were interesting and important - so should you. But let me try to convey why mathematicians were so interested in formal systems.

Math is hard. When a mathematician claims to have proven something, it is by no means immediately obvious whether the proof is correct or whether there is some subtle mistake or unjustified leap buried deep inside it. Let’s take a famous recent example: Andrew Wiles’ proof of Fermat’s Last Theorem. Wiles presented his original proof in 1993. It was 129 pages long. One of the referees reviewing Wiles’ proof asked a series of questions which uncovered a gap in the proof. Wiles then spent over a year trying to bridge that gap and repair the proof. In the later half of 1994, he found a solution and resubmitted his manuscript. About a year later, in May of 1995, the proof was accepted as correct.

That was for one of the most famous problems in mathematics, where everyone involved would be highly motivated to make sure the proof was airtight, and to do so as fast as possible. You can imagine less effort and scrutiny going into verifying the proofs of lesser known conjectures. If small mistakes in proofs go unnoticed, and those proofs are then used as building blocks in other proofs, those mistakes can proliferate in a troubling way.

How nice would it be, then, if all proofs were trivial to verify by a computer? That is the promise of a formal system. Formal systems are designed so that every step in a proof must be justified by previous lines in the proof (or axioms) and a transformation rule. Furthermore, the set of axioms and transformation rules are finite and “easily recognized”. More precisely, it should be relatively straightforward to write a (provably finite) computer program that checks, for every line in the proof, whether that line is the result of combining prior lines in the proof (or axioms) and a transformation rule. In this way, a proof in a given formal system could be submitted for verification to a computer, rather than a set of human referees, and the computer could mechanically and tirelessly verify that every single line in the proof follows directly from the axioms and transformation rules of the system and is therefore justified. This allows humans to focus their attention solely on the axioms and transformation rules of the system. If those are sound, then everything proven within the system must also be sound.

This was the hope of Hilbert, Russell, and others. That mathematicians could find a small, finite collection of axioms and transformation rules from which all other mathematical truths could be derived, and that those derivations could be effectively verified by a provably finite computer program. And this was the hope that Godel destroyed.