A standard way of demonstrating that two collections of combinatorial objects have the same cardinality is to exhibit a bijection between them. Browsing through some examples (here, there, yonder) quickly reveals that combinatorialists call such bijections explicit, presumably to differentiate them from other less palpable kinds of bijections. Wikipedia speaks of the method of bijective proof.

It seems that we have here a typical example of an informal mathematical notion that is quite familiar to most mathematicians, however it is difficult to pin down a proper and satisfying mathematical definition. I asked the local combinatorialists and did not really get a good answer.

Question: What is a proper mathematical definition of an explicit bijection?

Often we ask for an explicit bijection between two families of combinatorial objects, i.e., bijections $b_n : A_n \to B_n$, one for each $n \in \mathbb{N}$. Here $(A_n)_n$ and $(B_n)_n$ are two families of combinatorial objects, parametrized by $n$. The parameter need not be a single number.

Here are some unsatisfactory answers:

1. "A bijection is explicit if it is computable." This definition is too wide, because it allows silly algorithms that order combinatorial objects according to the layout of the sequences of bits that represent them, and use the order to establish a bijection. Bit representations typically have nothing to do with the combinatorial content of the objects under consideration.

2. "A bijection is explicit if it can be written down as an expression." This takes us back several centuries in terms of level of mathematical abstraction, and also varies a lot depending on what expressions are allowed. We really should be looking for a combinatorially meaningful notion, not a syntactic surrogate.

3. "A bijection is explicit if we can give a constructive proof of its existence." Well, a constructive proof certainly guarantees that a computable bijection exists, and can moreover be extracted from the proof, but this still feels too permissive. For example, we can always compose an explicit bijection so obtained with a computable automorphism of one of the sets, and still have a constructive proof. But such an automorphism could completely obfuscate the combinatorial structure of the set.

4. "Well-order $V_\omega$ (as all combinatorial objects easily live in it) and take the first bijection under the well ordering." Only a set theorist would have such thoughts. Again, we should strive for a definition which will be accepted as natural by combinatorialists.

Let me also say that I would prefer to not generalize the question to "what is an explicit thing?" At least in combinatorics "explicit bijections" are a well-established and useful notion, whereas mathematicians in general do not posses a universally agreed upon notion of "explicit thing".