17
$\begingroup$

Bourbaki used a very very strange notation for the epsilon-calculus consisting of $\tau$s and $\blacksquare$. In fact, that box should not be filled in, but for some reason, I can't produce a \Box.

Anyway, I was wondering if someone could explain to me what the linkages back to the tau mean, what the boxes mean. Whenever I read that book, I replace the $\tau$s with Hilbert's $\varepsilon$s. I mean, they went to an awful lot of trouble to use this notation, so it must mean something nontrivial, right?

You can see it on the first page of the google books link I've posted. I'm not sure if it's supposed to be intentionally vague, but they never introduce any metamathematical rules to deal with linkages except for the criteria of substitution, which pretty much cannot interact with $\tau$ terms.

Also, of course, since it's a book written to be completely a pain in neck to read, they use a hilbert calculus, and even worse, without primitive equality for determining whether or not two assemblies are equivalent.

$\endgroup$
6
  • $\begingroup$ I've forced this question into wiki mode, because I'm afraid that it will be voted down for being about metamathematics rather than mathematics itself. $\endgroup$ Feb 6, 2010 at 3:51
  • $\begingroup$ However, this is the first correct use of the tag [metamathematics]. This is literally about symbols on ticker tapes and such. $\endgroup$ Feb 6, 2010 at 3:53
  • 22
    $\begingroup$ metamathematics is the mathematics of mathematics. It is a branch of mathematics that includes model theory, proof theory, etc. I don't understand your comment about being the only valid use of the 'metamathematics' tag. $\endgroup$ Feb 6, 2010 at 5:24
  • 3
    $\begingroup$ Well, ya see, there's "real" metamathematics, and "applied" metamathematics... I hope someone catches that reference. $\endgroup$ Feb 6, 2010 at 16:19
  • 2
    $\begingroup$ In the sense of Hardy. $\endgroup$ Feb 6, 2010 at 16:19

5 Answers 5

27
$\begingroup$

Let me address the part of the question about "what the linkages back to the tau mean, what the boxes mean." The usual notation for using Hilbert's epsilon symbol is that one writes $(\varepsilon x)\phi(x)$ to mean "some (unspecified) $x$ satisfying $\phi$ (if one exists, and an arbitrary object otherwise)." If, like Bourbaki, one wants to avoid quantifiers in the official notation and use $\varepsilon$ instead (specifically, expressing $(\exists x)\phi(x)$ as $\phi((\varepsilon x)\phi(x))$), then any non-trivial formula will contain lots of $\varepsilon$'s, applied to lots of variables, all nested together in a complicated mess. To slightly reduce the complication, let me suppose that bound variables have been renamed so that each occurrence of $\varepsilon$ uses a different variable. Bourbaki's notation (even more complicated, in my opinion) is what you would get if you do the following for each occurrence of $\varepsilon$ in the formula. (1) Replace this $\varepsilon$ with $\tau$. (2) Erase the variable that comes right after the $\varepsilon$. (3) Replace all subsequent occurrences of that variable with a box. (4) Link each of those boxes to the $\tau$ you wrote in (1). So $(\varepsilon x)\phi(x)$ becomes $\tau\phi(\square)$ with a link from the $\tau$ to the boxes (as many boxes as there were $x$'s in $\phi(x)$).

One might wonder why Bourbaki does all this. As far as I know, the point of the boxes and links is that there are no bound variables in the official notation; they've all been replaced by boxes. So Bourbaki doesn't need to define things like free and bound occurrences of a variable. Where I (and just about everybody else) would say that a variable occurs free in a formula, Bourbaki can simply say the variable occurs in the formula.

I suspect that Bourbaki chose to use Hilbert's $\varepsilon$ operator as a clever way of getting the axiom of choice and the logical quantifiers all at once. And I have no idea why they changed $\varepsilon$ to $\tau$ (although, while typing this answer, I noticed that I'd much rather type tau than varepsilon).

$\endgroup$
8
  • 2
    $\begingroup$ Adrian Mathias in "A term of length..." points out that $\epsilon$ "is visually too close to the sign $\in$ for the membership relation" and gives a hint to his Danish Lectures. To learn more about $\tau$, please read tauday.com/tau-manifesto.pdf ;-) $\endgroup$ Apr 1, 2011 at 9:37
  • $\begingroup$ I didn't notice this answer when you posted it. I came back to this question because I was talking about it with someone, and this is fantastic. I've chosen this as the new 'best answer'. Thanks! $\endgroup$ Aug 1, 2012 at 21:06
  • 5
    $\begingroup$ While Bourbaki's solution looks weird to modern eyes, a treatment of bound variables require a surprising among of care to get right (try to reproduce capture-avoiding substitution from a book on lambda calculus). Once you replace his links by deBrujin indexes (which I find sensible), what he does seems isomorphic to the idea behind the "locally nameless representation" of binding: chargueraud.org/research/2009/ln/main.pdf $\endgroup$ Dec 17, 2015 at 7:19
  • $\begingroup$ @Blaisorblade I believe that de Bruijn indices would be problematic, because they require integers and counting... which is defined later in the book. $\endgroup$ Apr 19, 2020 at 17:21
  • 1
    $\begingroup$ @Mageek Interesting point, but I'm sure those "arrows" are defined even later than naturals. You need to take for granted some amount of (very weak) maths to even define the syntax. The naturals for de Bruijn indexes aren't a big problem (you only need a fixed amount of naturals, that can be computed once you write the book, so you don't even need the axiom of infinity). $\endgroup$ Apr 21, 2020 at 15:56
24
$\begingroup$

You must read the charming essay lampooning this notation, while also giving a thorough logical analysis of it, by Adrian Mathias.

He describes it thus:

A calculation of the number of symbols required to give Bourbaki's definition of the number 1; to which must be added 1,179,618,517,981 disambiguatory links. The implications for Bourbaki's philosophical claims and the mental health of their readers are discussed.

$\endgroup$
13
  • 3
    $\begingroup$ Adrian taught me set theory! I don't think he ever forgave Bourbaki for eschewing the axiom(-scheme) of replacement. He seems to have been having little swipes at them ever since :-) $\endgroup$ Feb 6, 2010 at 7:30
  • 4
    $\begingroup$ Adrian is great, I agree. But this article is more than a little swipe---it makes them look completely ridiciulous about math logic. He has another article called "The ignorance of Bourbaki", if you follow the link on his name, which is directly critical of this particular Bourbaki volume, as well as some follow-up articles. $\endgroup$ Feb 6, 2010 at 14:14
  • 5
    $\begingroup$ Those are some impressive articles. I had no idea Bourbaki was so set on pretending Godel's work didn't exist. $\endgroup$
    – S. Carnahan
    Feb 6, 2010 at 23:06
  • 3
    $\begingroup$ Here's a PDF link for those of us who don't have easy access to a DVI reader: dpmms.cam.ac.uk/~ardm/inefff.pdf $\endgroup$ Nov 20, 2015 at 14:32
  • 2
    $\begingroup$ @Blaisorblade Thank you for the link. I don't think Bourbaki's acknowledgement of incompleteness constitutes much of a rebuttal of Mathias's point, since the argument was that Gødel's work did not yield a substantial change in Bourbaki's philosophy toward formalization of mathematics. Mathias seems to draw his evidence not from the set theory text, but from contemporary articles by members of the group. $\endgroup$
    – S. Carnahan
    Dec 17, 2015 at 13:30
14
$\begingroup$

Matthias' polemics are funny at points but also misleading in several respects:

  1. ZFC also has enormous length and depth of deductions for trivial material. According to Norman Megill's metamath page, "complete proof of 2 + 2 = 4 involves 2,452 subtheorems including the 150 [depth of the proof tree] above. ... These have a total of 25,933 steps — this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms." Megill's system is based on a formalism for substitutions so there may be an enormous savings here compared to the way in which Matthias performs the counts (i.e., the full expanded size in symbols) for Bourbaki's system. If I correctly recall other information from Megill about the proof length he estimated for various results in ZFC, the number of symbols required can be orders of magnitude larger and this is what should be compared to Matthias' numbers.

  2. The proof sizes are enormously implementation dependent. Bourbaki proof length could be a matter of inessential design decisions. Matthias claims at the end of the article that there is a problem using Hilbert epsilon-notation for incomplete or undecidable systems, but he gives no indication that this or any other problem is insurmountable in the Bourbaki approach.

  3. Indeed, Matthias himself appears to have surmounted the problem in his other papers, by expressing Bourbaki set theory as a subsystem of ZFC. So either he has demonstrated that some reasonably powerful subsystems of ZFC have proofs and definitions that get radically shorter upon adding Replacement, or that the enormous "term" he attributes to the Theorie des Ensembles shrinks to a more ZFC-like size when implemented in a different framework.

EDIT. A search for Norman Megill's calculations of proof lengths in ZFC found the following:

"even trivial proofs require an astonishing number of steps directly from axioms. Existence of the empty set can be proved with 11,225,997 steps and transfinite recursion can be proved with 11,777,866,897,976 steps."

and

"The proofs exist only in principle, of course, but their lengths were backcomputed from what would result from more traditional proofs were they fully expanded. ..... In the current version of my proof database which has been reorganized somewhat, the numbers are:

empty set = 6,175,677 steps

transf. rec. = 24,326,750,185,446 steps"

That's only the number of steps. The number of symbols would be much, much higher.

$\endgroup$
10
  • 2
    $\begingroup$ Why does it take so many steps to prove the empty set exists? If $B$ is any set, then the Comprehension axiom says {$x\in B | x \neq x$} exists, and this is empty. I understand that a formal version of this argument would be longer, filling in all the logical steps, but what are most of those 6 million steps in Megils' proof about? $\endgroup$ Jul 14, 2010 at 11:06
  • 2
    $\begingroup$ I don't know, but both Megill's and Matthias' numbers seem to indicate that when you deliberately strip away the higher-level interface that we implicitly use to handle the (also implicit, or unspecified) lower-level proof language, things balloon. $\endgroup$
    – T..
    Jul 14, 2010 at 15:48
  • 5
    $\begingroup$ The outline is: Separation Axiom instance $\forall A\exists B\forall z(z\in B\iff z\in A\wedge \neg z= z)$. Universal instantiation strips off A quantifier. Existential instantiation produces $\forall z(z\in B\iff z\in A\wedge \neg z=z)$. State a tautology and apply MP to get $\forall z(z=z\to z\notin B)$. Equality axiom $\forall z\, z=z$. Another tautology and MPs give $\forall z\, z\notin B$. Existential generalization yields $\exists B\forall z\, z\notin B$, as desired. $\endgroup$ Jul 15, 2010 at 2:41
  • 4
    $\begingroup$ Another issue is that Mathias was computing the size of the term defining $1$, not the proof that it exists (or that it is the multiplicative identity). So the relevant comparison would be the fact that in ZFC, the empty set is defined by the formula $\forall z\, \neg z\notin x$, which has 6 symbols. The natural number $1$ (usually taken to be {0}) is defined by $\forall y\, (y\in x \iff \forall z\, \neg z\in y)$, which has 14 symbols. $\endgroup$ Jul 15, 2010 at 2:50
  • 2
    $\begingroup$ Megill's program is a proof checker, so I assume he is counting something akin to the number of nodes in a parse tree for each sentence of the proof, and the number of comparisons of such nodes needed to see that, e.g., your first step is an instance of Separation. Your much smaller counts are for the higher-level interface where a proof checker is in place to do this. In similar fashion, Bourbaki only gives a (presumably short enough to fit on a page or several such) high level definition of "1" that unwinds at a lower level into Matthias' monstrosity. $\endgroup$
    – T..
    Jul 15, 2010 at 6:12
6
$\begingroup$

I would like just to mention about "what the linkages back to the tau mean, what the boxes mean", that this notation has been revisited by Nicolaas Govert de Bruijn in the framework of the lambda-calculus and is largely used in theoretical computer science as a very convenient tool and is known now as "de Bruijn" indices. A literature can be found about this.

$\endgroup$
1
  • 2
    $\begingroup$ Since Bourbaki uses names for free variables, he's using a variant of deBrujin indexes — we call it "locally nameless representation". See my comment to the other answer: mathoverflow.net/questions/14356/… $\endgroup$ Dec 17, 2015 at 7:28
1
$\begingroup$

The notation using links was invented by Charles Saunders Peirce with his existential diagrams in 1883. It was reinvented by Willard van Orman Quine in his book Mathematical Logic in 1940. (Quine did not use the notation.) Bourbaki reinvented it in 1970.

I submit that the notation with links is more fundamental than de Bruijn indices because that still adds certain implementation details. The notation with links may seem awkward but for example in the theory of interpretations there are lots of artificial problems of keeping track of variable-names. These can be side-stepped using the links.

I think that the use of links dictates a co-inductive, top-down, `decompositional' view of syntax.

$\endgroup$
2
  • 1
    $\begingroup$ The statement about 1970 is not true. The link occurs in a draft by Bourbaki of around 1951 (E I.1 Etat 3). In His article Foundations of mathematics for the working mathematician (J. Symbolic Logic 14), published in 1949, however, He uses a "surrounding line". $\endgroup$ Nov 26, 2020 at 11:44
  • 1
    $\begingroup$ Link to the 1949 Bourbaki paper in JSL: jstor.org/stable/2268971. The 'surrounding line' line is near the bottom of page 3, where you can see a circle. $\endgroup$
    – David Roberts
    Nov 27, 2020 at 6:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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