elementary set theory - Finding explicit bijections between sets of the same cardinality

This is kind of a general question about establishing that two sets have the same cardinality. The definition of two sets $S$ and $T$ having the same cardinality is that there is a function $f: S \to T$ that is one-to-one and onto all of $T$.

My question is: are there any two sets for which we (and by that I mean "the mathematical community" or whatever) know that the two sets have the same cardinality by other means, but cannot find a bijection between them? I feel like the continuum hypothesis is in some vague sense related to this, but anyways I'm curious and would like to know.

Answer

This is independent from ZFC.

There is a first-order formula $\varphi$ such that $$\mathrm{ZFC} + V=L \vdash(\forall S)(\forall T)\Big(\big(\operatorname{card}(S)=\operatorname{card}(T)\big)\rightarrow\big(\{x \mid \varphi(x, S, T)\}\text{ is a bijection from }S\text{ to }T\big)\Big).$$

So it's consistent with ZFC that we can explicitly specify a bijection between any two sets of the same cardinality (assuming that ZFC is consistent, of course). [By the way, the formula $\varphi$ can be spelled out — it's not mysterious, just long if written out in full.]

On the other hand, if, for example, you use finite forcing to make $\aleph_1^{\,L}$ countable, then, in the generic extension, there is a bijection between $\omega$ and $\aleph_1^{\,L},$ but there is no bijection between them that is definable without parameters.

So (again assuming the consistency of ZFC), there is a model of ZFC in which $\aleph_1^{\,L}$ is countable but in which there is no definable bijection between $\omega$ and $\aleph_1^{\,L}.$

---

Some brief remarks on how to prove the statements above:

The existence of explicit bijections in $L$ is due to the fact that there is, if $V=L,$ a definable well-ordering of the universe.

The non-existence of a definable bijection between the two specified countable sets in the generic extension above can be proven using the homogeneity of the partial ordering used in the forcing argument.