Bigness (Part 1)

Azimuth 2020-04-13

The French mathematicians who went under the pseudonym Nicolas Bourbaki did a lot of good things—but not so much in the foundations of mathematics. In this paper, Adrian Mathias showed that their formalism was incredibly inefficient:

• Adrian R. D. Mathias, A term of length 4,523,659,424,929, Synthese 133 (2002), 75–86.

He proved that the definition of the number 1 in Bourbaki’s 1954 text on set theory requires 4,523,659,424,929 symbols and also 1,179,618,517,981 links connecting symbols, “without which, of course, the formula would be unreadable.”

One reason is that their definition of the number 1 is complicated in the first place. But worse, they don’t take $\exists$ , “there exists”, as primitive. Instead they define it—in a truly wretched way.

They use a version of Hilbert’s “choice operator”. For any formula $\Phi(x)$ they define a quantity $\tau_x(\Phi)$ that’s a choice of $x$ making $\Phi(x)$ true if such a choice exists, and just anything otherwise. Then they define $\exists x \Phi(x)$ to mean $\Phi$ holds for this choice. That is, $\Phi(\tau_x(\Phi))$ .

This builds the axiom of choice into the definition of $\exists$ . That’s a terrible idea (which goes back to Hilbert).

On top of that, their implementation of this idea leads to huge formulas. First, in $\tau_x(\Phi)$ they replace each appearance of $x$ in $\Phi$ with a box, $\square$ , and draw “links” from each box to the $x$ subscript in $\tau_x(\Phi)$ . This creates an ungainly mess. But more importantly, in the expression $\Phi(\tau_x(\Phi))$ , each original appearance of $x$ in $\Phi(x)$ has been replaced by $\tau_x(\Phi)$ . Thus, if the variable $x$ appears $n$ times in $\Phi(x)$ and the variable $y$ appears $m$ times, then the expression $\Phi(\tau_x(\Phi))$ contains the variable $y$ a total of $m + nm$ times.

This creates a combinatorial explosion when we have nested quantifers. And since they define $\forall$ (“for all”) in terms of $\exists$ , both kinds of quantifiers have this explosive effect. Their definition of “1” is rather long, with nested quantifiers, so it becomes huge when you write it out in detail.

And in the 1970 edition of their book, it got much longer! Here they defined ordered pairs in terms of sets rather than taking them as primitive, which is basically a good thing. But this makes their definition of the number 1 much longer. Robert Solovay calculated that this new definition requires

2409875496393137472149767527877436912979508338752092897

symbols and

871880233733949069946182804910912227472430953034182177

links. Mathias writes:

At 80 symbols per line, 50 lines per page, 1,000 pages per book, the shorter version would occupy more than a million books, and the longer, 6 · 10⁴⁷ books.

If each book weighed a kilogram, these books would weigh about 3 · 10¹⁷ times the mass of the Sun.

Puzzle. Using Bourbaki’s later formalism, if you wrote a proof that 1 + 1 = 2 on paper, could it fit inside the observable Universe?

Read the paper for more fun: