55
$\begingroup$

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$ 1054

symbols and

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

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$ 1047 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.)

$\endgroup$
  • 49
    $\begingroup$ I'm going to move comments to chat. Honestly, I'm finding some of the language used in comments pretty abusive (such as saying that the OP is "ranting" when in fact he's quoting someone, or saying the style of the question is "awful"). Let's tone it down, please. $\endgroup$ – Todd Trimble Apr 15 at 16:21
  • 1
    $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$ – Todd Trimble Apr 15 at 16:21
  • 4
    $\begingroup$ I was able to confirm Matthias' calculations that the ordered pair $(x, y)$ has a length of 4545 symbols. I can continue trying to confirm the estimates for the length of the Cartesian product $X\times Y$, and then...whatever else. $\endgroup$ – Alex Nelson Apr 17 at 2:15
  • 5
    $\begingroup$ The Cartesian product is a term represented by 3,184,591,216,053,048,167 symbols(!), confirming the number reported by Matthias. $\endgroup$ – Alex Nelson Apr 17 at 2:19
43
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • 3
    $\begingroup$ Might be good to add the titles of the linked articles in case the links break at some point in the future. $\endgroup$ – user76284 Apr 15 at 22:20
30
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • 3
    $\begingroup$ PS: about the estimate: if we start from $2$ and iterate $n$ times the squaring function, we get $2^{2^n}$, which in 7 steps reaches $2^{128}\sim 10^{39}$ and in 8 steps reaches $2^{256}\sim 10^{77}$. Hence assuming that every step in an intuitive proof roughly squares the size of the formal proof makes such estimates far from surprising. $\endgroup$ – YCor Apr 15 at 15:31
  • 2
    $\begingroup$ PPS Here's (on YouTube) Th. Hales' video of the quoted June 2014 Bourbaki seminar, and Thierry Coquand's talk the same day, the latter being in French. $\endgroup$ – YCor Apr 15 at 16:03
  • 1
    $\begingroup$ @user21820 See en.wikipedia.org/wiki/Extension_by_definitions . Since ACA0 is a two-sorted theory, you’d also need extension by definition of a new sort, which is not treated in the article: this amounts to fixing a formula $\delta(x)$ and defining $\exists X\,\phi(X)$ as $\exists x\,(\delta(x)\land\phi(x))$ and $\forall X\,\phi(X)$ as $\forall x\,(\delta(x)\to\phi(x))$. No such thing is possible for ACA0. More generally, you cannot even interpret ACA0 in PA, as ACA0 is finitely axiomatizable and PA is reflexive. $\endgroup$ – Emil Jeřábek Apr 16 at 9:25
  • 3
    $\begingroup$ @user21820 Whatever you have in mind, this is not what defitional expansion means. The point of extension by definitions is that you DO NOT increase the expressive power of the theory, only adding new names for things that are already definable in the original language. That’s why they are called DEFINITIONS. If you do something else, you need to call it differently. And please, take the discussion elsewhere, as it is completely irrelevant to the original question, YCor’s answer, and my original comment. $\endgroup$ – Emil Jeřábek Apr 16 at 9:56
  • 3
    $\begingroup$ @EmilJeřábek: Yes, my initial comment was based on a misunderstanding of what you meant. But I was just asking a question, no need for you to get so riled up as to use caps. Anyway, thanks for your responses. $\endgroup$ – user21820 Apr 16 at 10:07
21
$\begingroup$

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 solovay@math.berkeley.edu Wed Nov 11 13:39:46 1998
Date: Tue, 10 Nov 1998 23:43:04 -0800 (PST)
From: "Robert M. Solovay" 
To: amathias@rasputin.uniandes.edu.co
Cc: solovay@math.berkeley.edu
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.
| cite | improve this answer | |
$\endgroup$
  • 10
    $\begingroup$ There seems to be a rule of thumb in the logic community: if Solovay says it, it's correct. He seems to have garnered the reputation of being very, very careful. For example, he was the one who alerted Nash to a hole in his (Nash's) embedding theorem. $\endgroup$ – Todd Trimble Apr 17 at 19:28
20
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ Hmm...actually, if we simplify it further with substitutions, we can cut the representation of 1 down to $6.011873743380472\times 10^{37}$ symbols. $\endgroup$ – Alex Nelson Apr 17 at 4:22
  • 1
    $\begingroup$ Do you mean Mathias? $\endgroup$ – Asaf Karagila Apr 17 at 7:54
  • 1
    $\begingroup$ Damn it, man, I'm a mathematician, not a spelling bee champion! Err, I mean, thanks, I'll fix that :p $\endgroup$ – Alex Nelson Apr 17 at 13:34
  • 3
    $\begingroup$ Nice! By the way, this particular result 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 was calculated by Robert Solovay, not Adrian Mathias. See my own answer for Solovay's software. $\endgroup$ – John Baez Apr 17 at 19:53
  • 2
    $\begingroup$ And for the sake of completeness, using a primitive ordered pair, the length of "1+1=2" is a modest 19,516,572,617,436,743,593 $\approx 1.9\times 10^{19}$ symbols. $\endgroup$ – Alex Nelson Apr 17 at 22:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.