Bourbaki's definition of the number 1

Question

According to a polemical article by Adrian Mathias, Robert Solovay showed that Bourbaki's definition of the number 1, written out using the formalism in the 1970 edition of Théorie des Ensembles, requires

2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 $\approx$ 2.4 $\cdot$ 10⁵⁴

symbols and

871,880,233,733,949,069,946,182,804,910,912,227,472,430,953,034,182,177 $\approx$ 8.7 $\cdot$ 10⁵³

connective links used in their treatment of bound variables. Mathias notes that at 80 symbols per line, 50 lines per page, 1,000 pages per book, this definition would fill up 6 $\cdot$ 10⁴⁷ books. (If each book weighed a kilogram, these books would be about 200,000 times the mass of the Milky Way.)

My question: can anyone verify Solovay's calculation?

Solovay originally did this calculation using a program in Lisp. I asked him if he still had it, but it seems he does not. He has asked Mathias, and if it turns up I'll let people know.

(I conjecture that Bourbaki's proof of 1+1=2, written on paper, would not fit inside the observable Universe.)

Answer 1

These calculations have been carried out by José Grimm; see [1] as well as [2]. According to one version of the formalism in the original Bourbaki, Grimm gets $$16420314314806459564661629306079999627642979365493156625 \approx 1.6 \times 10^{55}$$ (see page 517 of [1, version 10]). The discrepancy with Solovay's number is probably due to some subtle difference of interpretation of some detail. Note that the English translation of Bourbaki introduces some "small" changes and Grimm gets a rather different value: $$5733067044017980337582376403672241161543539419681476659296689 \approx 5.7 \times 10^{60}$$ EDIT: As suggested in the comments, here are the full citations for Grimm's papers.

[1] José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. inria-00440786v10. doi:10.6092/issn.1972-5787/4771

[2] Grimm, J. (2010). Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. Journal of Formalized Reasoning, 3(1), 79-126. doi:10.6092/issn.1972-5787/1899

Answer 2

There are some interesting issues here, as I will elaborate. Let me first make a full quote of §4.2 "Bourbaki on formalization" from Thomas Hales' 2014 Bourbaki seminar "Developments in formal proofs" ((1)).

Over the past generation, the mantle for Bourbaki-style mathematics has passed to the formal proof community, in the way it deliberates carefully on matters of notation and terminology, finds the appropriate level of generalization of concepts, and situates different branches of mathematics within a coherent framework. The opening quote claims that formalized mathematics is absolutely unrealizable. Bourbaki objected that formal proofs are too long ("la moindre démonstration . . . exigerait déjà des centaines de signes" [translation by YCor: "any proof... would require hundreds of signs")], that it would be a burden to forego the convenience of abuses of notation, and that they do not leave room for useful metamathematical arguments and abbreviations ((2)). Bourbaki is correct in the strict sense that no human artifact is absolutely trustworthy and that the standards of mathematics evolve in a historical process, according to available technology. Nevertheless, the technological barriers hindering formalization have fallen one after another. Today, computer verifications that check millions of inferences are routine. As Gonthier has convincingly shown in the Odd Order theorem project, many abuses of notation can actually be described by precise rules and implemented as algorithms, making the term abuse of notation really something of a misnomer, and allowing mathematicians to work formally with customary notation. Finally, the trend over the past decades has been to move more and more features out of the metatheory and into the theory by making use of features of higher-order logic and reflection. In particular, it is now standard to treat abbreviations and definitions as part of the logic itself rather than metatheory.

So Bourbaki's point (at that time, namely in the few years before 1970) was that writing formal proofs, although precisely defined, is a hopeless task. For this reason, Bourbaki made no effort of efficiency.

To give an illustrating example, assume that I'm writing an exercise program in some language, computing $n\mapsto \sum_{k=1}^nf(k+a_n)$, where $a(n)$ is the $n$-the decimal of $\pi$, and $f(n)$ say is $\lfloor n^{3/2}\rfloor$, which I previously defined as functions in the same programming language (the only point with this choice is that $f$ is much faster to compute than $a$). If I do it crudely $$(j:=0; \quad \text{for } k=1..n\;\; j:= j+f(k+a_n);\quad \text{return }j)$$ then I will compute $a(n)$ $n$ times. If instead I write $$(j:=0;\quad a:=a(n); \quad \text{for } k=1..n\;\; j:= j+f(k+a);\quad \text{return }j)$$ I'll compute $a(n)$ only once and hence this will be far quicker, although at first sight this is the same "algorithm". If I roughly say what should be the principle of the proof, this aspect will not appear.

The point of Bourbaki, once they assume that formalizing proofs is not worth an explicit realization, was therefore not to make this realization any practical. The possible (likely) fact that the size of the resulting formal proof of $1+1=2$ is huge is therefore anecdotical: for instance, if $N$ is the already huge proof of $0+1=1$ (or any related prior result), it's very possible that the formal proof will contain identical copies of this proof $N$ times, resulting in something of size $\ge N^2$. The conclusion is that the Bourbaki's formalization is highly unpractical— this conclusion was already Bourbaki's (yet based on a clear underestimate, which would appear today as efficient). Given that this formalization was written just to exist and without practical concern, this is not a big deal (although the paper advertized by the OP makes a lot of conclusions from this fact).

Most likely, the main ideas of Bourbaki's foundations could be formalized in a more efficient way (more efficient than highly inefficient is not too hard— should we bluster if $10^{54}$ is upgraded to $10^{20}$?), but I have no idea whether they could be formalized in a useful practical way. (There might also be good reasons that Bourbaki's foundations are not prone to efficient formalization; the estimate asked by OP is not a sufficient one, for the reason elaborated in the previous paragraph.) Given that Bourbaki's foundations have an interest which is now essentially reduced to historical (including for the aspects other than this exact formalization), and other foundations have been successfully formalized by others in the last 15 years, I'm not sure if anybody would spend energy on this.

At a historical level, one can wonder whether Bourbaki's 1970 belief that formal proofs are not to be written down, has had any counterproductive effect in the next few decades; this is hard to measure and the paper ((3)) linked by the OP speculates on this with no serious grounds. Let me make a quote from the conclusion of ((3)).

Bourbaki themselves took the first course: as remarked by Corry, they shied away from their own foundations. I expect that they came to the conclusion that logic is crazy — they had to conclude that to protect their sanity; but were they aware that the picture of logic they were giving to their disciples is merely a grotesque distortion and diminution of that subject ? Is it too fanciful to see here, in this choice of formalism, with its unintuitive treatment of quantifiers, the reason for the phenomenon (which many mathematicians in various European countries have drawn to my attention whilst beseeching me not to betray their identity, lest the all-powerful Bourbachistes take revenge by depriving them progressively of research grants, office facilities and ultimately of employment) that where the influence of Bourbaki is strong, support for logic is weak ? How does one get the message across, to those who have accepted the Bourbachiste gospel, that logicians are actually not interested in a formal system of such purposeless prolixity, still less do they advocate it as the proper intellectual framework for doing mathematics ?

In regard to the fact that Bourbaki invited Hales to talk on formal proofs, I found the "revenge" claim particularly crisp today! ((3)) was written earlier, but whether there was a ban in the 1990s against elaboration and study of formal proofs, I'll leave it to better witnesses of that time and subject.

((1)) Th. Hales. Developments in formal proofs

((2)) N. Bourbaki. Théorie des ensembles [Set theory], 1970.

((3)) A. Mathias. A term of length 4,523,659,424,929 (1999). Link

Answer 3

I asked Robert Solovay if he still had the program he used to compute the length of Bourbaki's definition of "1" (using their 1970 definition of ordered pairs). He didn't, but Adrian Mathias did, and Solovay has allowed me to release it. So, here are three documents. They don't settle every question one might have, but they should be useful to people attempting to check this calculation.

• calcusol.pdf. This is a document entitled "The Bourbaki Constant 1". It begins:

This is a private document [for the eyes of RMS and ARDM only] which extends ARDM's computation of the length of the Bourbaki rendition of "The ineffable name of 1" to the case when the Kuratowski ordered pair is employed. My plan is to write programs in Allegro Common Lisp to compute the relevant numbers.

I program using the style of "literate programming" introduced by Knuth. However the Web and Tangle introduced by Knuth [which have been refined to CWEb and CTangle by Levy] are limited to languages closely linked to C or Pascal. So I prefer to use a more flexible literate programming language which permits fairly arbitrary target languages. Currently, I use Nuweb which is available on the TEX archives in the directory /web/nuweb.

One of the nice things about literate programming is that one can write programs in the natural psychological order, but arrange that the output files have the order needed for the target programming language. We will exploit this heavily in what follows.

• solfact.txt. This is a short document including the output of the program described in the previous document. Here it is, in its entirety:

From [email protected] Wed Nov 11 13:39:46 1998
Date: Tue, 10 Nov 1998 23:43:04 -0800 (PST)
From: "Robert M. Solovay" 
To: [email protected]
Cc: [email protected]
Subject: Results

Adrian,

    Here is the printout of my calculation of the length of the
Bourbaki term for 1. If we do the original definition, I get approx.

4.524 * 10^{12}

    If we use the Kuratowski ordered pair, I get approx.

2.41 * 10^{54}

    This is big, but not nearly as big as the 2 * 10^{73} that you
claim. This is certainly related to the smaller estimate that I have
for the size of the Kuratowski ordered pair.

    I omitted some trivial lines from this printout where I "gave
the wrong commands to the genie".


USER(1): (setq p 0) ;;;[Doing the original Bourbaki definition where
                    ;;; ordered pair is a basic undefined notion.]
0

USER(3): (load "compute.cl")
; Loading ./compute.cl
T
USER(4): J_length
4523659424929
USER(5): (log J_length 10)
12.65549
USER(6): J_links
1179618517981
USER(7): (log J_links 10)
12.071742
USER(8): (setq p 1) ;;; Now use Kuratowski ordered pair

1

USER(10): (load "compute.cl")
; Loading ./compute.cl
T
USER(11): J_length
2409875496393137472149767527877436912979508338752092897
USER(12): (log J_length 10)
54.381996
USER(13): J_links
871880233733949069946182804910912227472430953034182177
USER(14): (log J_links 10)
53.940456

• solpair.pdf. This is a short note on some of Bourbaki's definitions including the definition of ordered pair.

Answer 4

I was able to reproduce Mathias's results with some Haskell code with some specific details about how many symbols are needed in each term. (As a sanity check, I verified I recovered the same results reported by Mathias term-by-term when the ordered product was primitive.)

When the ordered pair is not primitive, the sizes of the various terms are:

• Size of 1 = 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897
• Size of term A = 15,756,227
• Size of term B = 10,006,221,599,868,316,846
• Size of term C = 59,308,566,315
• Size of term D = 364,936,653,508,895,574,881
• Size of term E = 101,217,516,631

One thing worth noting is that, well, this seems dishonest. I mean, there are a lot of double negations which are not simplified, which bloats the size quite a bit (an additional $1.863\times 10^{53}$ symbols or so). I wouldn't be surprised if there were other simplifications which would cut down the bloat further...not that we'd get anything less than $10^{50}$ or so.

If you'd like to check the number of links, I can do that too.

Addendum. The relation "1+1=2" can be computed, and found to have a length of 22,411,322,875,029,037,193,545,441,224,646,148,573,589,725,893,763,139,344,694,162,029,240,084,343,041 (or approximately $2.24113228750290371 \times 10^{76}$). This is using the definitions in Bourbaki of cardinal addition $\mathfrak{a}+\mathfrak{b}$ using the disjoint sum of the indexed family $f\colon\mathrm{Card}(2)\to\{\mathfrak{a},\mathfrak{b}\}$ considered as a graph. It's really convoluted, but the details can be found in Bourbaki's Theory of Sets Chapter II sections 3.4, 4.1, and 4.8 as well as Proposition 5 (in chapter III, section 3.3); this all works with the Kuratowski ordered pair, not a primitive $\bullet A B$ ordered pair.

For what it's worth, computing the size of 1 was nearly instantaneous, whereas computing the size of "1+1=2" took about 7 minutes and 30 seconds.

Answer 5

Mathias, Grimm, and some people who've contributed to this Q&A seem to take these numbers as evidence of the impracticality of working formally in Bourbaki's theory. YCor explicitly called it unpractical, and said that Bourbaki shared that belief, which may be true. In light of that, I think it's worth writing a bit about the premise that seems to underlie the question.

If you define $F_1=F_2=1,\; F_{n+2}=F_n+F_{n+1}$, and eliminate $F$ from the expression $F_{250}$ by substitution, you get a tree of about $1.6\times 10^{52}$ nodes, or a string of that many symbols in Bourbaki/Polish notation.

I don't think it follows that the definition is a bad one. It's hard to see how you could avoid the blowup without introducing complications that would interfere with the definition's intended use.

You could object that this isn't a comparable situation because $250>1$, but that scarcely matters. Bourbaki happened to put a bunch of structure underneath $1$, but even if $1$ is primitive in your proof system, as soon as you do anything remotely interesting with it, you will have the same problem. The mere statement of your upper bound in Ramsey theory, never mind the proof, will have over Graham's-number symbols in it.

There is a simple way to get a better measure of the complexity of $F_{250}$ without changing the definition: merge common subtrees. The result is a dag of 249 nodes, of which 248 are additions: one for $F_3$, one for $F_4$, $\ldots$

Here's what happens when you merge common subtrees of the expressions from Grimm page 514. (The one called M is Solovay's, and the one called SS is mentioned in Timothy Chow's answer.)

expression	tree size	tree links	dag size	dag links
SS	57330670440×1050	21634097377×1050	13153	876
SM	315628276×1050	114233082×1050	13015	876
S	171713×1050	64721×1050	8061	544
M	24098×1050	8718×1050	7971	544

I calculated these with a Python program that constructs the complete dags in memory and then collects statistics with and without duplication counts. The construction consumes a whopping several megabytes of RAM due to CPython's inefficient object representation, and takes a noticeable fraction of a second due to CPython being slow. If my code were published in a series of books, and each book weighed 1 kilogram, the total mass of all the books would be a few grams.

The dags are still much larger than the code that made them. The remaining bloat can be blamed on the definition of $\exists$, which uses its body twice in a way that precludes sharing, and on complicated constructions that can't be shared because they have children, particularly ordered pairs. These problems can be solved by introducing parametrized subtrees. One approach is to express the dag as a tree without duplication by introducing a "structural let" that assigns names to subtrees, and then permit the named subtrees to have holes whose values are specified at each use point. (Or you can keep the dag and add $\phi$ nodes – see Appel.) With this extra flexibility you can write any of these expressions in just a few hundred nodes.

I want to stress that these concise expressions are fully formally equivalent to the original strings. Not a single double negative has been eliminated. Given the concise formula and an index, you can compute the symbol at that index in the original string.

In this framework – which is just a small subset of what's available in a proof system like Coq – it hardly matters what's primitive. If Bourbaki's pairing operator $\supset$ isn't primitive, you can define it once at the top of the expression; the space cost is constant regardless of how many times it's used. If the expression is a proposition whose proof will be formally checked, the axioms of $\supset$ need to be proven and checked as theorems only once each, adding a constant startup time regardless of how many times they're used. These costs aren't fundamentally different from the costs of implementing $\supset$ as primitive. Only if you convert to the normal form will you see a difference, and there is no reason ever to do that. It's an abstraction violation.

To summarize:

• These gigantic normal forms show up in all formal systems, not just Bourbaki's.
• They aren't a good measure of practicality or anything else.