| HN Mirror

[The following isn't really "like you're five", but given how long it is already that's probably just as well.]

Proofs and formal systems, and why we're kinda screwed

Mathematicians like to prove things. What we would really like would be to be able to find, for every mathematical statement, either a proof that it's true or a proof that it's false.

It wasn't until the early 20th century that mathematicians got a clear enough idea of what proof is to figure out whether that could be done. And it turns out it can't! That was proved in 1931 by Kurt Goedel, who did something that these days is very familiar to anyone in computing but was novel then: he found a way to encode mathematical statements, and sequences of mathematical statements, as numbers, in such a way that properties of those statements turn into properties of the numbers, so that you can use ordinary mathematics to reason about them.

This enabled him to show that if you have any system for doing mathematics that (1) is powerful enough to describe ordinary arithmetical statements and (2) is simple enough that you can check mechanically what is and isn't a proof, then there are statements that that system can neither prove nor disprove. (With a proviso I'll come to in a couple of paragraphs.)

So much for the hopes of mathematicians.

Anyway, despite that setback, mathematicians didn't abandon the idea of building up all of mathematics in some nice simple formalized system in which we can prove and disprove things. We still like to do that, and have come to terms with the fact that there will be things we can neither prove nor disprove.

... Unless the system we're working in happens to be inconsistent, meaning that there's some proposition that it can both prove and disprove. In that case, what actually happens is that it can prove everything, which is of course completely useless. So far as we know, the systems we like to use aren't inconsistent. It would be nice to prove they aren't -- but there's a nice variant of Goedel's theorem that says not just "for any system that isn't inconsistent, there are propositions it can't decide" but "for any system that isn't inconsistent, a formalized statement of its own consistency is a proposition it can't decide".

Once, again, so much for the hopes of mathematicians.

The particular formal system called ZFC

One particular nice simple formalized system is called ZFC, which is short for "Zermelo-Fraenkel set theory with the Axiom of Choice". That's a bit of a mouthful. So, "set theory" means that the basic idea we're starting with is that of a set of things. (In order to do mathematics, we certainly need some idea like that. It turns out that taking it as the foundational idea works fairly well.) Zermelo was a mathematician who came up with one fairly good way to do that. Fraenkel was another mathematician who improved Zermelo's system.

The "Axiom of Choice" -- the C in ZFC -- is a rather technical statement in set theory that turns out to be (1) "obviously true" according to some mathematicians' intuition, (2) useful for proving things we care about, and (3) something that plain old ZF, without the C, can neither prove nor disprove. (Unless, as usual, ZF is actually inconsistent.) In particular, this means that if ZF is a consistent system -- if it isn't able to prove 1+1=3 -- then ZFC is as well. (Because if you could get a contradiction out of ZFC, you could use it to prove not-C within ZF.) So adding the Axiom of Choice to ZF is "safe"; it can't create contradictions that weren't already there. And, since it's useful, we tend to keep it around.

[You can skip the next two paragraphs if you like. They describe the sort of thing you do if you want to build up all of mathematics on top of set theory.]

So, how do you build mathematics out of set theory? The usual sort of game you play is this. We want to be able to talk about numbers. So first of all we find an implementation of numbers in terms of sets. (If you were doing mathematics in a computer you'd want to do roughly the reverse, and build your sets out of numbers.) So we might, e.g., say that 0 "is" the empty set, and then 1 "is" the set containing just 0, and then 2 "is" the set containing just 0 and 1, and so forth. That gets you a load of sets that can (as well as being sets) do double duty as the non-negative integers. Then you construct the integers (negative as well as positive) out of those, and then the rational numbers (ratios of integers) out of those, and then you need some fancier footwork to get the "real numbers" (including things like pi and the square root of 2).

And then you're off to the races, because once you have the real numbers you can do geometry: e.g., three-dimensional space "is" the set of triples (x,y,z) of real numbers, and things like spheres and dodecahedra are just sets of points in space. And now you have numbers and geometrical things, and you can build all the other weirder more abstract things mathematicians like to study in a similar way.

OK, so if we have sets then we have everything, so a formalized set theory is a reasonable thing to try to use as a basis for mathematics. But, ever since Goedel, we know that any formalized system will be unable to decide (i.e., either prove or disprove) some statements we might be interested in.

What that page is about

The Wikipedia page linked here is a list of statements we might be interested in that ZFC is, as it turns out, unable to decide. "Independent of" means "neither provable nor disprovable from".

(There are other systems you can use instead of ZFC. Some of them are other varieties of set theory; some work entirely differently. It usually turns out that you can translate most statements of ordinary mathematics to and fro between them, and that what's provable and what isn't doesn't depend on "implementation details" (e.g., I described one particular way to build non-negative integers out of sets; what if we do it a different way? The answer is usually that it doesn't matter). But some systems are "stronger" than others and can prove or refute more statements. To be usable for mathematics, a system can't be "too much" weaker than ZFC. And since in some sense ZFC encodes most of the things that mathematicians are pretty sure "ought" to be true, most systems people want to use aren't "too much" stronger than ZFC either. A lot of the statements on that page would also be on similar pages about systems other than ZFC.)

A lot of those statements are weird technical things that only a mathematician could care about, and indeed that only a mathematician specifically interested in what's provable from ZFC and what isn't could care about. Some of them are at least potentially interesting to some mathematicians for their own sake, but understanding them generally requires a pile of background that (1) I don't really have myself in most cases and (2) you really don't want me to make this long enough to deal with.

But here's one of them, one of the oldest of them all. Some sets are bigger than others. For instance, {1,2,3} is bigger than {1,2}. What about infinite sets? It's not obvious a priori what "bigger" should even mean for infinite sets, but Georg Cantor (a pioneer of this stuff) found a good answer, whose details we don't need right now. It turns out that the integers are "the same size" as the rational numbers, even though the integers seem like a tiny subset of the rational numbers, but that the real numbers are "bigger". So here's the question: are there any sets bigger than the rational numbers but smaller than the real numbers? This is called the "continuum hypothesis", which is a bit of a stupid name but never mind, and it is neither provable nor disprovable in ZFC.