Simple City

I’ve just uploaded the slides [pdf] from a talk I gave yesterday at the University of Leeds, about concrete incompleteness. The topic is the same as my recent New Scientist article, but in greater technical detail, though the intention was still that it be reasonably accessible to non-logicians. I’ll tell the central story here as a sort of commentary, and there are equations and other gory details available in the slides.

Since Kurt Gödel proved his celebrated first incompleteness theorem, we have known that arithmetic (that is to say the positive whole numbers with addition and multiplication) will always contain unprovable statements. This means that no matter what fundamental axioms we choose to underlie arithmetic, there will always be some statement T such that neither it nor its negation ‘not T’ can be deduced from our axioms. These are called independent or unprovable statements[1].

But of course, it never makes sense to say “T is an unprovable statement” without reference to some specific axiomatic system: different axioms, different provable & unprovable statements.

The standard axioms for arithmetic were written down by Giuseppe Peano in 19th century Italy. Forty years later, Gödel’s theorem implied that Peano’s axioms must be incomplete. The question for today is: are they incomplete in a way that matters to non-logicians? In the course of studying number theory, or combinatorics, are you liable to run into an unprovable statement? Or are such things really curiosities of no wider importance?

Since then, several concrete instances of incompleteness have been found, examples being the termination of Goodstein sequences, the Paris-Harrington variant of Ramsey’s theorem, and Kruskal’s theorem on finite trees as well as Harvey Friedman’s finite miniaturization of that result.

Now, that last result of 2002 represented a big step forward in unprovability theory, for the following reason: attempts to axiomatise arithmetic did not stop with Peano. In the mean time, a wealth of stronger axiomatic systems have been investigated. In particular, for much modern mathematics, it is not enough to talk just about plain whole numbers. We also need to consider how sets of such numbers behave. This is the key, for example, to building a coherent theory of real and complex numbers. Peano’s axioms are first order, meaning that they discuss only numbers. To axiomatise the behaviour of sets of numbers, we need what is known as second order logic. But which sets of numbers should we axiomatize? The minimum second-order system which extends Peano arithmetic is called ACA₀, or “arithmetical comprehension”. Here we can sensibly analyse all the sets of numbers which Peano describes. However there are also many stronger systems, notably ATR₀, or “arithmetical transfinite recursion”. This system provides a much richer class of sets, defined via certain infinite processes, unavailable in weaker systems. This is the right level at which to build up a large amount of analysis, calculus, and topology. On the other hand, Friedman’s variant of Kruskal’s theorem is purely finitary in nature, involving only plain whole numbers. It’s natural home would seem to be ACA₀, and yet it is unprovable not just at that level, but in ATR₀ too.

This was certainly a striking result, but recent developments have taken us much further. Way, way beyond second order arithmetic is the the system of Zermelo-Fraenkel set theory, ZFC[2]. This allows not just all possible sets of numbers, but also sets of sets of numbers, sets of sets of sets, and so on ad infinitum (and indeed considerably beyond that). As such, ZFC has become the standard foundation for the whole of mathematics. For most purposes it represents massive overkill.

Of course though, Gödel’s theorem applies here too: there must be questions which even ZFC cannot answer. From a set theorist’s perspective, the primary examples concern the existence of large cardinals.

ZFC is the modern setting for the great work that Georg Cantor did in the late 19th century, disassembling the concept of infinity. Cantor showed that there is not just one level of infinity, but an infinite ladder with each rung infinitely higher the last. What’s more, there is no ultimate infinity beyond all the others: this ladder has no top rung. One can ask though, whether or not there are rungs so far up that that they are unapproachable from below. These, if they exist, are called “large cardinals”, and their existence is independent of the axioms of ZFC. Set theorists have been studying multiple varieties of large cardinals, and the logical dependencies between them, for over 100 years.

Returning to the finite realm, and the arithmetic of the plain whole numbers, Gödel assures us that here too, not even ZFC will be enough to resolve all possible queries. There must be statements about numbers which are unprovable in ZFC. So we can repeat the earlier question: are these the sort of things which working mathematicians, who are not logicians or set theorists, need to worry about?

This question has received a brand new answer, in the subject of Boolean Relation Theory developed by Harvey Frieman in a forthcoming book (section 3 on this page has downloadable pdfs). In it, he considers a very simple class of functions of whole numbers, known as the Expansive Linear Growth (ELG) functions, and then identifies a certain configuration of inputs and outputs which such functions may exhibit. (The details are on my slide number 12.) The question is: does every ELG function exhibit such a configuration? And the answer is not deducible within ZFC. Certainly, one cannot construct a counterexample. But we have to pass to a stronger system, which contains certain large cardinals, in order to prove the answer “yes”.

I believe that this is an important result. The situations described by Boolean relation theory are indisputably elementary, and (perhaps somewhat disputably) they seem natural. What is more, they are ripe for generalisation. Replacing the natural numbers with different underlying structures, and considering different classes of sets and functions defined by analytic or geometric conditions, we can ask similar questions about the configurations of inputs and outputs which emerge. This may well represent a door through which questions of provability enter mainstream mathematics, not in ones and twos, but in truly significant quantities.

In syntactic terms, the unprovable statements of Boolean relation theory have complexity at the level of Π⁰₂. Friedman additionally set himself the goal of finding a simpler Π⁰₁ sentence, which depends on large cardinals, while at the same time providing “clear and compelling information in the finite mathematical realm”. In a separate development, he claims to have found exactly that, in the form of a statement about directed graphs living among the rational numbers. Unfortunately there are several intermediate definitions needed to present it. None of them are at all difficult, but they do mount up, to the point where I can’t say I have much of a mental picture of what exactly is being asserted. Some details, pared down as much as I can, are in my slides 14-16, and a fuller account is in section 0.14D of the introduction [large pdf] to Harvey’s book.

Ok, that’s it for now, but I do intend to write more on this topic – hence the “1” in the post title. Next time I’ll be musing about the philosophical implications of having syntactically simple statements about natural numbers, which can only be resolved using large cardinals.

[1] They’re sometimes called ‘undecidable’ statements, but – warning! – that word is also used in a different way, to do with algorithms. Generally I prefer ‘uncomputable’ for the algorithmic notion, but maybe that’s just me.

[2] Technically, that’s Zermelo-Fraenkel set theory plus the Axiom of Choice. But I don’t want to think about that here – there’s already enough unprovability on the table. So we’ll just take Choice as given.