In my first post on this blog, I defined and proved my favorite fact: The halting problem is undecidable. You should probably read that post if you don’t know what that means, but in brief, it means that it is impossible to write a computer program that will always correctly tell you whether any given computer program will run forever or eventually stop.

I promised to talk about some of the far-reaching consequences of this fact in future posts, and here I am keeping my promise, if a little late. (Don’t get used to me keeping my promises on this blog, though…) I’ll start with arguably the biggest consequence of the halting problem’s undecidability: Gödel’s First Incompleteness Theorem.

As is my m.o., I’ll try to keep the discussion accessible to laypeople; I’ll provide lots of context; and I’ll just generally be extremely long-winded.

This post will be even more long-winded than usual because I feel the need to provide way too much context. To sort of acknowledge that this post is absurdly long, I’ve put a little (*) in the heading of sections that are less tangential. I’m incredibly biased, of course, but I suggest attempting to make it through the whole thing, and if you get tired somewhere around Euclid or Cantor, skip ahead to the next asterisk.

[toc]

The Halting Problem’s Strong Connection with Mathematics (*)

While I think that the fact that the halting problem is undecidable is pretty surprising, before I presented the proof, I gave a rough argument for why one might expect the halting problem to be undecidable. The basic idea is that any program that solved the halting problem would also solve lots of open questions in mathematics (though, of course, it might take the program more than the age of the universe to do it). For example, I showed that the Collatz conjecture, a problem that’s stumped mathematicians for 75 years or so (Paul Erd?s famously said of it, “Mathematics is not yet ripe for such problems”), could be easily resolved by a program that solved the halting problem.

There’s a lot that’s special about the Collatz conjecture, but the argument that I used was quite general and applies to tons of open problems in mathematics. Indeed, given any conjecture of the form “Every integer has property P,” if we can write a computer program that tells us whether or not a given integer has property P, then we can write a computer program that runs forever if the conjecture is true and halts if it isn’t. (Simply write a program that checks all integers for property P and stops if it finds one that doesn’t have it.)

So, a program that solved the halting problem would be a godly tool for mathematicians (ignoring the fact that it might not be practical due to time constraints). This method (or a slight modification) would solve, for example, Goldbach’s conjecture, the twin primes conjecture (and numerous other conjectures about the number of various types of primes), the question of the existence of odd perfect numbers, the inverse Galois problem, etc., all of which have been open problems for over a century.

In fact, this relationship actually goes the other way as well: To put it informally, if mathematicians had some godly tool that solved general problems in mathematics (or any respectably large subset of problems in mathematics), then they would be able to write a computer program that solved the halting problem. Since this can’t be done, it follows that mathematicians can’t have their godly tool. In fact, they can’t have anything remotely close to that. (I think mathematicians are mostly happy about that, so don’t feel bad for them.)

The formal version of this fact is called Gödel’s First Incompleteness Theorem. It’s an incredibly important fact, first proved by Kurt Gödel in 1930. Gödel’s proof is pretty involved and wouldn’t be suitable for this blog, but a proof using basic computer science is essentially trivial.

Regardless, I’m going to put my own spin on it, and I’ll characteristically go on a tangent or four on the way. Here’s tangent number one:

Euclid’s Axioms

Around 300 BC or so, the Greek mathematician Euclid outlined a famous set of axioms in the field of geometry. In other words, he came up with a very simple set of statements that he would assume to be true in order to prove more interesting things. The goal of any decent set of axioms is to be as boring as possible–Every axiom should be obviously and intuitively true, and there shouldn’t be very many of them–and Euclid’s axioms are the prototypical example. You might recognize them from high school geometry, but more likely your teacher cheated and let you use fancier axioms. Here they are (in my own clumsy wording):

1. There is exactly one line connecting any two distinct points.
2. Any line segment can be extended to arbitrary length.
3. For every two distinct points, there is exactly one circle centered at the first and touching the second.
4. All right angles are equal.
5. Given a line L and a point P, there is exactly one line that touches P and is parallel to  L. (Euclid used a different, equivalent axiom.)

These are all incredibly obvious facts. Some of them might seem so obvious that they’re not worth mentioning. Of course there’s only one line between a pair of distinct points, for example. And, there are only five of them. However, you can prove a lot of stuff from these axioms, e.g. the Pythagorean Theorem.

However, generations of mathematicians, including Euclid, were not happy with the fifth axiom, known as the parallel postulate. In their eyes, the fifth axiom seemed more like something that needed to be proven than an axiom; it certainly sounds like a less trivial statement than the first four. But, the parallel postulate was a key step in many geometric proofs. So, in order to get rid of this ugly axiom without losing a ton of geometry, they spent a couple thousand years trying to prove that the parallel postulate logically followed directly from the other four axioms.

It wasn’t until the mid-19th century that mathematicians discovered that there are “geometries” in which the parallel postulate is false. In order to see this, you need to relax the definitions of “point” and “line” a bit, so the language gets a little bit messy. I’ll try my best to be clear.

Consider a sphere, and call a pair of classical points “an elliptical point” if they are exactly opposite each other on the sphere. Note that a single elliptical point is made up of two classical points. If a circle on a the sphere is made up of elliptical points, call it “an elliptical line.” Elliptical lines are also called great circles because they are the largest circles that you can draw on a sphere–The Earth’s equator is a nice example. You can think of them as any circle that divides the sphere into two equal halves.

A quick check shows that elliptical points and elliptical lines satisfy the first four axioms. However, they don’t satisfy the second because all elliptical lines cross. (If you’re following, you should be able to picture this easily.) So, obviously the fifth axiom can’t follow from the first four because we have a counter-example! (Our counterexample is called an elliptical non-Euclidean geometry.)

This example is illustrative. While mathematicians often think of axioms as assumptions, they’re perhaps better thought of as pieces of a definition. Neither Euclid nor I phrased them like this, but axioms one through four essentially define some properties of things that mathematicians have agreed to call points, lines, and angles. However, those definitions are more general than the English definitions of those words; in particular, elliptical points and elliptical lines are perfectly good points and lines under the first four axioms. The fifth axiom serves to narrow the definitions so that they represent something much closer to the English notions of points, lines, and angles.

Cantor, Dedekind, and the Axiomatization of Mathematics

The incredible success of Euclid’s axioms leads to a natural question: Can we come up with a nice set of axioms for more general concepts in mathematics?

In the late nineteenth century, mathematicians started to realize that this question was fundamental to their field. Arguably the first big leap in logic was the attempt to characterize the notion of a set by Georg Cantor. Cantor’s set theory essentially defined sets intuitively–A set is a collection of things that are defined by some axioms. For example, the set of natural numbers can be defined as follows:

1. Zero is a natural number
2. Every natural number has exactly one “successor.” (One is zero’s successor. 84 is 83’s successor.)
3. Any successor of a natural number is a natural number.
4. Ain’t nothing else a natural number. (Elephants, for example, don’t count. Mathematicians often assume an axiom like this implicitly.)
5. Zero is not the successor of any natural number. (Note that -1 is not a natural number.)
6. Distinct natural numbers have distinct successors. (One’s successor is different from two’s successor.)

Mathematicians began to rely heavily on this concept of a set defined by axioms by the turn of the century, and it proved to be very useful. For example, distilling out the concept of a set allowed mathematicians to more easily talk about sets that contained other sets. In particular, Dedekind and Cantor together used this new paradigm to formalize the concept of the real numbers; they each defined the real numbers in a different way as a set of sets. These were the first truly rigorous and modern definitions of the reals, and they used these definitions to discover many of the real numbers’ most important properties. In short, they discovered extremely important facts about the mathematical world and finally put a fundamental concept in mathematics on stable, modern footing.

Well, not quite… It turns out that Cantor’s intuitive set theory simply doesn’t work–It allows you to define paradoxical objects, and is therefore inconsistent.

The classic example is Russell’s paradox: Bertrand Russell pointed out that if a set can contain other sets, then surely it can contain itself. Russell then considered the set of all sets that do not contain themselves–Call it S. Russell then asked “Does S contain itself?” If S contains itself then it should not be included in S by definition, but then it doesn’t contain itself, which means that it should be included in S by definition, which means it contains itself…

This particular paradox might seem a bit cheap, but it’s merely the simplest example in a long list of paradoxes discovered in what is now called naive set theory. Because such objects exist in naive set theory, the theory allows you to “prove” two contradictory facts (e.g., that S contains itself and doesn’t contain itself). Obviously, nothing “proven” in such a theory can be trusted because someone might “prove” its opposite as well! Indeed, it’s not hard to see that any fact, true or false, can be “proven” starting from naive set theory.

In the terminology of logicians, naive set theory is inconsistent.

Russell, Principia, and the Axiomatization of All of Mathematics

After the failure of Cantor’s set theory, the race was on to put mathematics on solid footing. Some mathematicians, philosophers, and logicians wanted to axiomatize all of mathematics; they wanted to find a set of axioms from which all mathematical truths could be derived, and they wanted these axioms to be consistent.

Bertrand Russell was arguably the leader of this movement. He published his first book on the subject, The Principles of Mathematics, in 1903, in which he detailed his paradox. In 1910, he and Alfred North Whitehead published the first volume of their attempt to axiomatize all of mathematics: Principia Mathematica.

In PM, Russel and Whitehead defined a system of types in which one object could not contain another of the same type, thus avoiding Russell’s paradox. (Under these axioms, there was no question as to whether the set S contains itself because nothing can contain itself.) After defining this new kind of set, PM undertook the task of proving what they could about specific sets under these axioms–e.g. the natural numbers, the integers, the real numbers, etc.

It would be an extreme understatement to call this a slow and tedious process. On page 379, PM finally manages to prove that . (The authors famously commented “The above proposition is occasionally useful.”) Two more volumes were published in 1912 and 1913 respectively. Whitehead and Russell planned to continue beyond the third, but the tedium eventually tired them out.

Many mathematicians believed that Russell and Whitehead had accomplished their task of finding axioms that could in principle be used to develop all of mathematics, though many were not happy with the specific axiom scheme that they chose (nor with their notation).

Gödel’s First Incompleteness Theorem (*)

However, Principia was not successful. In fact, in 1930, the twenty-four-year-old mathematician Kurt Gödel proved that any attempt to axiomatize all of mathematics was guaranteed to fail. In short, if a set of axioms is sound (i.e. if every statement that can be logically derived from the axioms is true–I won’t bother to worry about what truth means here) and strong enough to prove some basic facts, then there must be statements that can neither be proven nor disproven under the axioms.

Gödel’s original proof is beautiful but tedious. Wikipedia has a decent sketch of it that may interest you. However, there is an extremely short, elegant proof that uses the fact that the halting problem is undecidable. (Remember that?) Here’s how it goes:

First, we choose a set of axioms that is strong enough to prove that the halting problem is undecidable. In particular, this set of axioms must be strong enough to reason about computer programs or algorithms. (In a more formal presentation, these notions would be much more clearly defined.)

Just so that you have a rough image in your mind, it might be helpful to think of the three axioms of equality plus some additional axioms that we won’t worry about:

1. For any x, x = x.
2. For any x and y, if x = y then y = x.
3. For any x, y, and z, if x = y and y = z, then x = z.
4. …

Suppose for the purposes of contradiction that every mathematical truth can be derived from these axioms in finitely many steps. (In a more formal presentation, this notion would be much more clearly defined.) Let’s use this assumption to write a computer program, P, that solves the halting problem, a contradiction:

Since we want P to solve the halting problem it will naturally take as input a description of another computer program, Q. After taking its input, P will enumerate all of the theorems that follow logically from the axioms. So, using our example axioms, P might list theorems like this:

1. For any x, x = x. (Axiom)
2. For any x and y, if x = y then y = x. (Axiom)
3. For any x, y, and z, if x = y and y = z, then x = z. (Axiom)
4. For any w, x, y, and z, if w = x, x = y, and y = z, then w = z. (Iterating theorem three twice)
5. For any x, y, and z, if x = y and z = y, then x = z. (Combining theorems two and three)
6. …

If P happens to arrive at the theorem “Q eventually halts,” then P will output that fact. If P happens to arrive at the theorem “Q runs forever,” then P will output that fact. Obviously, Q must do one of these things, and since we assumed that our axioms can derive every mathematical truth in finitely many steps, it must be the case that P will eventually output the correct answer.

But, this means that P solves the halting problem. Since we’ve already proven that that’s impossible, our assumption must have been wrong. In particular, there is no set of axioms from which all mathematical truths follow. Russell’s attempts were guaranteed to fail from the beginning.

What’s This Mean? (*)

To understand what Gödel’s First Incompleteness Theorem means, it helps to think of the case of Euclid’s first four axioms and their relationship to the parallel postulate. The first four axioms provide loose definitions of points, lines, and angles, so it’s possible to interpret those terms in a few different ways. In particular, there are ways to interpret the definitions that allow for different versions of the parallel postulate.

GFIT essentially says that this ambiguity always comes up in any set of axioms, and it happens for objects that are much more fundamental than points, lines, and angles. Even the most basic objects in mathematics, the set and the natural numbers, cannot be defined in an unambiguous way.

Zermelo, Fraenkel, Choice, and the Axiomitization of Some of Mathematics

This is an extremely deep fact. The current gold standard of axioms is called Zermelo-Fraenkel set theory, and it is an extremely powerful beast, with extremely simple and intuitive axioms (like Euclid’s first four) that manage to avoid the paradoxes of naive set theory and still provide the foundations for extremely rich mathematics.

However, ZF is not perfect. There are extremely important problems in mathematics that cannot be resolved using the axioms of ZF.

The standard example is the axiom of choice, which, to oversimplify, merely says that if we have any (possibly infinite) collection of sets, we can always successfully choose one element from each set. It turns out that that incredibly and seemingly obvious simple statement cannot be proven in ZF. I think that to most people first encountering it, the axiom of choice feels a bit like the parallel postulate–It’s something that’s clearly true, but it seems a bit too involved to require it’s own axiom. The problem with the axiom of choice is that, though it is itself intuitive, it leads directly to incredibly unsettling results, such as the Banach-Tarski paradox, which is a bit too much for me to get into in this post.

While most mathematicians accept the axiom of choice and use it relatively freely, it’s still common practice to mention whether or not a theorem relies on it, and it’s still a common goal to try to prove as much as possible without using AC. There are even mathematicians who prove theorems that follow from the negation of the axiom of choice. Again, what this represents is not a disagreement about things that are true of sets, but rather what we mean by the word itself.

The Infinite Expanses of Unprovable Theorems… and Computer Science (*)

Of course, the axiom of choice isn’t the end of the story. There’s an infinite hierarchy of theorems (an uncountable hierarchy, actually), each independent of ZF and all theorems that come before it in the hierarchy. Indeed, there are infinitely many such hierarchies. This means that mathematicians keep bumping into theorems that they’d like to prove, only to find (usually after a lot of banging their heads against various walls) that the question depends in a subtle way on the definitions of basic concepts in mathematics. No matter how much they pin down the definitions, there will always be something that they haven’t considered. (Wikipedia has a nice list of theorems proven to be independent of ZF with the axiom of choice for those who are interested.)

This is beautifully counter-intuitive for people who aren’t mathematicians. Researchers outside of pure math basically just completely ignore it in their own work, and even mathematicians tend to ignore it when they can. It’s often viewed as a beautiful theorem that has little practical implications.

Indeed, computer scientists like GFIT largely because of the beautiful proof that I presented above is inherently a computer science proof. (It’s pretty much indisputably the proof of GFIT that’s in THE BOOK.) For theoretical computer scientists (which I guess I am or soon will be), however, the infinite expanse of unprovable theorems that GFIT implies is becoming a bit harder to ignore. That’s because complexity theory has piled up a long list of unproven conjectures, some of which have incredibly important applications in society. There’s the very strange prospect that many or all of the long-standing open problems in complexity theory are simply independent of our chosen axioms.

What would it mean to have something so incredibly practical as the strength of an encryption scheme (e.g. the security of our entire banking system…) depend on something as abstract as our choice of axioms? I may dedicate a post to this topic at some point

There’s also weird philosophical implications of GFIT. Maybe I’ll write about those at some point as well.

Anyway, that’s my very long rant. If you like rants like this, you might consider subscribing to my RSS or following me on Twitter.

I appreciate feedback, so please feel free to comment or e-mail me or mention me on Twitter or whatever. I can’t promise a response, but I think I’m usually pretty good about it.

Also, I wanted to give a quick thank you to the people who up-voted (Is that the right terminology?) my post on the halting problem on reddit. That was really cool. I mostly wrote this post because people there showed interest.