In this question: What is the definition of "canonical"?
, people gave interesting "philosophical" takes on what the word "canonical" means. Moreover I percieved an underlying opinion that there was no formal mathematical definition.
Whilst looking for something else entirely, I just ran into Bill Messing's post
http://www.cs.nyu.edu/pipermail/fom/2007-December/012359.html
on the FOM (Foundations of Mathematics) mailing list. I'll just quote the last paragraph:
"It is my impression that there is very little FOM discussion of either
Hilbert's epsilon symbol or of Bourbaki formulation of set theory. In
particular the chapitre IV Structures of Bourbaki. For reasons,
altogether mysterious to me, the second edition (1970) of this book
supressed the appendix of the first edition (1958). This appendix gave
what is, as far as I know, the only rigorous mathematical discussion of
the definition of the word "canonical". Given the fact that Chevalley
was, early in his career, a close friend of Herbrand and also very
interested in logic, I have guessed that it was Chevalley who was the
author of this appendix. But I have never asked any of the current or
past members of Bourbaki whom I know whether this is correct."
It's a 4-day weekend here in the UK and I'm very unlikely to get to a library to find out what this suppressed appendix says. Wouldn't surprise me if someone could find this appendix on the web somewhere though! Is there really a mathematical definition of "canonical"??
NOTE: if anyone has more "philosophical" definitions of the word, they can put them in the other thread. I am hoping for something different here.
Best Answer
Although the Bourbaki formulation of set theory is very seldom used in foundations, the existence of a definable Hilbert $\varepsilon$ operator has been well studied by set theorists but under a different name. The hypothesis that there is a definable well-ordering of the universe of sets is denoted V = OD (or V = HOD); this hypothesis is equivalent to the existence of a definable Hilbert $\varepsilon$ operator.
More precisely, an ordinal definable set is a set $x$ which is the unique solution to a formula $\phi(x,\alpha)$ where $\alpha$ is an ordinal parameter. Using the reflection principle and syntactic tricks, one can show that there is a single formula $\theta(x,\alpha)$ such that for every ordinal $\alpha$ there is a unique $x$ satisfying $\theta(x,\alpha)$ and every ordinal definable set is the unique solution of $\theta(x,\alpha)$ for some ordinal $\alpha$. Therefore, the (proper class) function $T$ defined by $T(\alpha) = x$ iff $\theta(x,\alpha)$ enumerates all ordinal definable sets.
The axiom V = OD is the sentence $\forall x \exists \alpha \theta(x,\alpha)$. If this statement is true, then given any formula $\phi(x,y,z,\ldots)$, one can define a Hilbert $\varepsilon$ operator $\varepsilon x \phi(x,y,z,\ldots)$ to be $T(\alpha)$ where $\alpha$ is the first ordinal $\alpha$ such that $\phi(T(\alpha),y,z,\ldots)$ (when there is one).
The statement V = OD is independent of ZFC. It implies the axiom of choice, but the axiom of choice does not imply V = OD; V = OD is implied by the axiom of constructibility V = L.
When I wrote the above (which is actually a reply to Messing) I was expecting that Bourbaki would define canonical in terms of their $\tau$ operator (Bourbaki's $\varepsilon$ operator). However, I was happily surprised when reading the 'état 9' that Thomas Sauvaget found, they make the correct observation that $\varepsilon$ operators do not generally give canonical objects.
A term is said to be 'canonically associated' to structures of a given species if (1) it makes no mention of objects other than 'constants' associated to such structures and (2) it is invariant under transport of structure. Thus, in the species of two element fields the terms 0 and 1 are canonically associated to the field F, but $\varepsilon x(x \in F)$ is not since there is no reason to believe that it is invariant under transport of structures. They also remark that $\varepsilon x(x \in F)$ is actually invariant under automorphisms, so the weaker requirement of invariance under automorphisms does not suffice for being canonical.
To translate 'canonically associated' in modern terms:
1) This condition amounts to saying that the 'term' is definable without parameters, without any choices involved. (Note that the language is not necessarily first-order.)
2) This amounts to 'functoriality' (in the loose sense) of the term over the core groupoid of the concrete category associated to the given species of structures.
So this seems to capture most of the points brought up in the answers to the earlier question.