Can formal logic give a precise notion of "canonical"?

Question

Coming off of this discussion, I'm wondering what the term "canonical" really means. In that thread, many suggested category theory as a way to formalize the concept of what "canonical" means, using the precise term "natural" (and, many suggested that the two were not the same thing). Beyond its formal equivalent in category theory, the word natural seems to have nothing other than an intuitive or even "theological" meaning.

However, I was wondering if there is some way to define the notion of canonical by using formal logic.

Here's my own idea: After all, when we choose something we have to use some sort of logical procedure. The notion of canonicity then might mean that there actually exists some logical way to pick out a particular element, morphism, etc. When there's no canonical choice, it might mean that there is no logical way to pick out one choice over another.

Answer 1

It might be of interest to recall how Bourbaki uses the word "canonical" -- though admittedly this is far from formal logic. When a notion is first defined, for instance the homomorphism from a group to a quotient group, Bourbaki says "this homomorphism is called canonical". This allows him to talk about "the canonical homomorphism from $G$ to $G/H$" without any ambiguity whenever this situation occurs.

So he does not define the term canonical, but only certain canonical maps, sets, objects ...

Answer 2

The term 'canonical' is very general and any attempt to create a "precise notion" may be questioned and can never be proved as such. However, there is a canonical candidate, which at least concerns canonical morphisms for constructs and other structured sets, which has a clear logical character.

First, every mathematical structure on a set is determined by relations between sets. For group structures there is a primary relation $r$ that is a function $G\times G \overset {r}\longrightarrow G$, $(x,y)\underline{r} z \Leftrightarrow z=x\centerdot y$ and some secondary relations which are conditions on $r$ (associativity, unit element and inverses). For a topological space the primary relation could be $2^X \overset{r}\longrightarrow X$, where $2^X$ is the set of all subsets of $X$ and $M\underline{r}x$ is the relation $x\in \bar{M}$ (the closure of $M$).

Whenever the main relation of a mathematical structure is given on the form $F(X)\rightarrow X$, for a functor $F$ in the category Rel (where sets are objects and binary relations are morphisms) which maps morphisms $X\overset {f}\longrightarrow Y$ on $F(X)\overset {F(f)}\longrightarrow F(Y)$, it is possible to define morphisms between the structures as (in general non commuting) diagrams: $\require{AMScd}$ \begin{CD} F(X) @>F(f)>> F(Y)\\ @VrV V @VVsV\\ X @>>f> Y \end{CD} such that

(1) $\quad \rho\underline{F(f)}\sigma \Rightarrow (\rho\underline{r}x\Rightarrow\sigma\underline{s}f(x))$.

This condition on $f$ gives the canonical morphisms to every construct that provide canonical morphisms.

Example: If $F$ is the (contravariant) functor defined as $2^X\overset{2^f}\longrightarrow 2^Y$, where $M\underline{2^f}M'\Leftrightarrow M=f^{-1}(M')$ and $r,s$ are defined as above, then due to (1):

$M=f^{-1}(M')\Rightarrow (x\in \bar{M}\Rightarrow f(x)\in \bar{M}')$, so $x\in \overline{f^{-1}(M')}\Rightarrow f(x)\in \bar{M}'$. (Continuity).