Bourbaki's epsilon-calculus notation
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).
You must read the charming essay lampooning this notation, while also giving a thorough logical analysis of it, by Adrian Mathias.
- Adrian Mathias, A Term of Length 4,523,659,424,929, Synthese 133 (2002) 75--86
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.
Matthias' polemics are funny at points but also misleading in several respects:
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.
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.
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.