lo.logic - candidate for rigorous _mathematical_ definition of "canonical"?

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.

• Next Is there a model theoretic realization of the concept of Arithmetical Hierachy?
• Previous physics - Mathematical definition of running