Why is it so difficult to define constructive cardinality?

Question

Consider Frege's cardinality and HoTT set-truncation cardinality, both of which can be well-defined in constructive theory (as SetoidTT and CubicalTT, respectively). Why don’t we regard them as well definitions of constructive cardinality?

Answer 1

Short summary: There is no constructive notion of cardinality that resembles the classical one because the expected properties of cardinality simply do not hold constructively.

Cardinality is supposed to capture the idea that some sets have more elements than others. In constructive mathematics it works in only a very limited fashion. There are several obstructions to having a reasonable notion of cardinality, as well as counter-models dispelling one's expectations.

Since we're going to work constructively, we need to be careful about classically equivalent notions bifurcating. Let us agree on the following definitions (which are constructively the most reasonable versions I know):

Definition: A set $A$ is:

• finite if there is $n \in \mathbb{N}$ and a surjection $\{0, \ldots, n-1\} \to A$,
• subfinite if it is a subset of a finite set,
• infinite if there is an injection $\mathbb{N} \to A$,
• countable if there is a surjection $\mathbb{N} \to \{\star\} + A$ (if $A$ has an element this is equivalent to having a surjection $\mathbb{N} \to A$),
• uncountable if it is not countable,
• subcountable if it is a subset of a countable set.

Cardinality of finite and subfinite sets

Let us imagine that we have an operation which assigns to each set $A$ some quantity $|A|$ called the "cardinality of $A$", capturing the intuitive idea of "number of elements".

The following restrict the possibility of measuring the size of subfinite and finite sets with natural numbers.

Proposition 1: If cardinality assigns to each subset $S \subseteq \{\emptyset\}$ a natural number such that $|S| = 0 \Rightarrow S = \emptyset$ and $|S| = 1 \Rightarrow S = \{\emptyset\}$, then excluded middle holds.

Proof. Given any truth value $p$, if the cardinality of $\{x \in \{\emptyset\} \mid p\}$ is $0$ then $\neg p$, and if the cardinality is $1$ then $p$. $\Box$.

Proposition 2: Suppose cardinality assigns to each finite set a natural number such that: (1) if $|A| \leq 1$ then all elements of $A$ are equal, and (2) if $|A| > 1$ then $A$ contains two different elements. Then excluded middle holds.

Proof. Given any truth value $p$, consider the quotient $A =\{0,1\}/{\sim}$ where $x \sim y \iff (x = y) \lor p$. If $|A| \leq 1$ then $0 \sim 1$ hence $p$, and if $|A| > 1$ then $\neg (0 \sim 1)$ hence $\neg p$. $\Box$

We could restict to finite sets with decidable equality. Every such set is isomorphic to an initial segment $\{0, \ldots, n-1\}$ for a unique $n \in \mathbb{N}$, which is its cardinality. The resulting notion of cardinality is useful for finite combinatorics, but it excludes important examples, such as the set of complex zeros of a polynomial (which is finite but may not have decidable equality).

An interesting possibility would be to measure the size of subfinite and finite sets in the Dedekind-MacNeille completion of $\mathbb{N}$. One could probably get a workable notion of cardinality: the cardinality of a finite set $A$ is the infimum of all $n \in \mathbb{N}$ such that there is a surjection $\{0, \ldots, n-1\} \to A$. Alas, the law of trichotomy $|A| < |B| \lor |A| = |B| \lor |B| < |A|$ would not be provable.

Cardinality of $\mathbb{R}$

If we base cardinality on existence of injections and surjections, then the cardinality of $\mathbb{R}$ is quite under-specified. There always is an injection $\mathbb{N} \to \mathbb{R}$, and that's about it.

Proposition 3: There is no bijection $\mathbb{N} \to \mathbb{R}$.

Proof. If there is such a bijection then $\mathbb{R}$ has decidable equality, but then we can carry out Cantor's diagonalization proof (by nested intervals) to show that there is no surjection $\mathbb{N} \to \mathbb{R}$. $\Box$

Proposition 4: In the effective topos, there is no surjection $\mathbb{N} \to \mathbb{R}$, no surjection $\mathbb{R} \to \mathbb{N}$, no injection $\mathbb{R} \to \mathbb{N}$, and there is $S \subseteq \mathbb{N}$ with a surjection $S \to \mathbb{R}$.

Proposition 5: In the realizability topos over infinite-time Turing machines, there is an injection $\mathbb{R} \to \mathbb{N}$ and there is no surjection $\mathbb{N} \to \mathbb{R}$.

Proof: The paper An injection from the Baire space to natural numbers explains how to embed the Baire space into $\mathbb{N}$. The same technique works for $\mathbb{R}$. $\Box$

Proposition 6: In the parametric realizability topos $\mathsf{PRT}(\mathbb{M}_\mu)$ generated by a Miller sequence, there is a surjection $\mathbb{N} \to \mathbb{R}$, and there is no injection $\mathbb{R} \to \mathbb{N}$.

So, in a constructive settings the reals may be subcountable, countable, or uncountable.

If we define $|A| \leq |B|$ to mean that there is an injection $A \to B$, then it may happen that $|\mathbb{N}| \leq |\mathbb{R}|$ and $|\mathbb{R}| \leq |\mathbb{N}|$ (and there is no bijection $\mathbb{N} \to \mathbb{R}$).

If we define $|A| \leq |B|$ to mean that there is a surjection $B \to A$ (for inhabited $A$), then it may happen that $|\mathbb{R}| \leq |\mathbb{N}|$ (and there is no bijection $\mathbb{N} \to \mathbb{R}$).

Let me also throw in the following wrench, in case you had hopes that at least the demarkation line between finite and infinite is crisp.

Proposition 7: In the effective topos there is a subset of $\mathbb{N}$ which is neither finite nor infinite.

Proof. Consider an immune set. $\Box$.

Cantor-Schröder-Bernstein theorem

Further evidence of the unsatisfactory status of constructive cardinality was provided by Cecilia Pradic and Chad Brown who showed that the Cantor-Schröder-Bernstein theorem implies excluded middle.

Proposition 8: Suppose the following holds for all sets $A$ and $B$: if there are injections $A \to B$ and $B \to A$ then there is a bijection $A \to B$. Then excluded middle holds.

Proof. See arXiv:1904.09193. $\Box$

Cantor's theorem

Finally, there is a little bit of good news.

Proposition 9: (Cantor) There is no surjection $A \to \mathcal{P}(A)$.

Proof. The usual proof by diagonalization is constructive. $\Box$

In summary, there does not seem to be a good constructive notion of cardinality, at least not one that would usefully measure sizes of finite and subfinite sets, and that would offer a definite comparison of the sizes of $\mathbb{N}$ and $\mathbb{R}$.

P.S. The HoTT book has a chapter on cardinality, which very quickly veers into asssuming excluded middle (and is the only such chapter in the book).

Answer 2

In my opinion this is a fairly underexplored topic, like a lot of constructive set theory. Andrej has already done an excellent job of explaining some of the dead ends you encounter if you try to come up with a workable notion of constructive cardinality of sets, but to be honest this kind of thing happens all the time in constructive math. For instance, the law of excluded middle is equivalent to the statement that $\mathbb{Z}$ is a principal ideal domain. That doesn't mean that one should just give up on doing commutative algebra constructively. $\def\Pc{\mathcal{P}}$

---

Large subset arguments

One of the primary applications of cardinality that is constructively salvageable is the following kind of argument:

The function $f : A \to B$ cannot be a surjection because $C \subseteq B$ is too big.

Classically of course we often use this to find an element outside of the range of $f$, which is often not going to be feasible constructively, but the mere non-existence of such a surjection can still sometimes be a non-trivial statement (and in the cases I discuss here we actually are able to do this).

In choiceless classical math, the notion of cardinality bifurcates into two relations:

• $A \leq B$ means that there is an injection from $A$ into $B$.
• $A \leq^\ast B$ means that there is a surjection from a subset of $B$ onto $A$.

(I'm cheating a little bit in that $\leq^\ast$ is typically defined in a more classically minded way, but this is equivalent.) Usually one can't hope to do more constructively than one can do in choiceless classical math (although a surprising amount of applications of countable and dependent choice can be rescued by working 'proof-relevantly' and carrying uniform witnesses of conditions around), so I think it's reasonable to try to think about both of these in a constructive context. One thing to note is that many of the basic properties of $\leq$ and $\leq^\ast$ that can be proven without choice classically are also constructively valid:

• $A \leq B \Rightarrow A \leq^\ast B$.
• $\Pc(A) \not\leq^\ast A$. (The standard proof of Cantor's theorem can be adapted to show this fairly easily, but I'll also prove a stronger statement explicitly later in Proposition 4.)
• $A \leq^\ast B \Rightarrow \Pc(A) \leq \Pc(B)$.
• $\aleph(A) \leq^\ast \Pc(A^2)$, where $\aleph(A)$ is the Hartogs number of $A$ (the supremum of the ordinals that inject into $A$).

The second of these relations, $\leq^\ast$, is the relevant one for large subset arguments. Specifically, we have that if $C \not\leq^\ast A$ and $C \subseteq B$, then $B \not\leq^\ast A$. This can be used to prove non-subcountability results, for instance.

Proposition 1. The lower Dedekind reals are not subcountable.

Proof. The map $f(X) = \sup\left\{\sum_{n \in X_0} 3^{-n} : X_0 \subseteq X~\text{finite}\right\}$ from $\Pc(\mathbb{N})$ to $\mathbb{R}_L$ is an injection. Since $\Pc(\mathbb{N})$ is not subcountable, it follows that $\mathbb{R}_L$ is not subcountable as well. The argument for $\mathbb{R}_U$ is the same. $\square$

The proof that the map $f(X)$ is an injection is a bit technical, so I am going to skip it in this answer. I'll give an easier but conceptually similar proof of another proposition that entails Proposition 1 later though (in Proposition 5).

One thing to note about the above argument is that it is very similar to the classical proof of the uncountability of $\def\Rb{\mathbb{R}}\Rb$ by embedding Cantor space as the standard one-thirds Cantor set. The map $f(X)$ is analogous to the standard embedding (although scaled by a factor of $\frac{3}{2}$).

Now, to be fair, the Proposition 1 can also be proven more easily by modifying Blechschmidt and Hutzler's proof that the MacNeille reals are not countable. Since the MacNeille reals embed into $\mathbb{R}_L$ and $\mathbb{R}_U$, you get that they are not subcountable again by a large subset argument. On some level though I think that the content of these two proofs is pretty closely related if stared at in the right way.

Constructive Cantor-Schröder-Bernstein theorem

The Cantor-Schröder-Bernstein theorem really is a beautiful piece of set theory, so I think it's reasonable to put some effort into trying to rescue it. One of the things I find interested about it is that, while it isn't constructive in the 'official' sense, it is a 'constructive' theorem by the standards of classical math. Not only do you not need the axiom of choice to prove it but you can even write down an entirely explicit formula for the bijection. This formula is explicit enough that the proof works in the category of measurable spaces. Cantor-Schröder-Bernstein doesn't work in the category of topological spaces, though, which is a sign that it isn't going to work constructively, at least not with a naïve translation, since functions between sets in constructive math have something of a 'continuous' character.

In Points and Space (1954), Brouwer introduced the notion of two sets being 'congruent':

Definition 2. $A$ and $B$ are congruent if $A \mathop{\Delta} B := \{x : (x \in A \wedge x \notin B) \vee (x \in B \wedge x \notin A)\}$ is empty.

In other words, two sets are congruent if there is no positive witness that they are different. Another way to state this is that the (proper) classes $\{x : x \notin A\}$ and $\{x : x \notin B\}$ are equal (in the sense of extensionality). As such, congruence of sets is an equivalence relation.

Brouwer gives as an example of congruent but not identical sets $\Rb$ and $\def\Qb{\mathbb{Q}}\Qb \cup (\Rb \setminus \Qb)$. This is part of why to me working with sets up to congruence feels a bit like working with measurable sets modulo null sets, since the decomposition of $\Rb$ into $\Qb$ and $\Rb \setminus \Qb$ is lives in the measurable category, not the continuous category.

In particular though, congruence allows us to fudge the only part of the proof of Cantor-Schröder-Bernstein that isn't constructive. Let's write $X \sim Y$ to denote that $X$ and $Y$ are congruent.

Proposition 3. If $f : A \hookrightarrow B$ and $g : B \hookrightarrow A$ are injections, then there are subsets $A_0 \subseteq A$ and $B_0 \subseteq B$ with $A_0 \sim A$ and $B_0 \sim B$ such that there exists a bijection $h : A_0 \to B_0$.

Proof. Just as in the classical proof, for any $a \in A$, we can find a unique maximal sequence $\dots,b_{-3},a_{-2},b_{-1},a_0,b_1,a_2,b_3,\dots$ indexed by a final segment of $\def\Zb{\mathbb{Z}}\Zb$ such that $a_0 = a$ and $b_{2n+1} = f(a_{2n})$ and $a_{2n+2} = g(b_{2n+1})$ (for all $n$ for which this is defined). Call this the chain of $a$ (and also call this the chain of any $b = b_{2n+1}$ for some $n$). Being in the same chain is an equivalence relation on $A \sqcup B$.

Let $X \subseteq A$ be the set of elements $a$ satisfying that for every $a'$ in the chain of $a$, $g^{-1}(a')$ exists. Let $A_0 = A \cup (A \setminus X)$. (Note that $A_0 \sim A$.) Define $h: A_0 \to B$ by $h(a) = g^{-1}(a)$ if $a \in X$ and $h(a) = f(a)$ if $a \notin X$. Let $B_0$ be the image $f[A_0]$. Note that since being in the same chain is an equivalence relation on $A \sqcup B$ (and since $f$ and $g$ both preserve this equivalence relation), we have that $h$ is an injection and therefore a bijection onto its image. Therefore all we need to show is that $B_0 \sim B$ and we'll be done.

So assume for the sake of contradiction that there is a $b \in B$ with $b \notin B_0$. Since $b \notin B_0$, we must have that any $a \in A$ in the chain of $b$ is not in $X$ and so in particular $g(b) \notin X$. This implies that it cannot be the case that $f^{-1}(b)$ does not exist (otherwise we'd have that $g(b) \in X$). But we also can't have that $f^{-1}(b)$ doesn't exist, because this would imply that $g(b) \in X$, which is a contradiction. So our assumption that there is a $b \in B \setminus B_0$ leads to a contradiction. Since $B_0 \subseteq B$, we therefore have that $B \sim B_0$. $\square$

I think there's another similar statement one can make using locales, although I'm a little bit out of my depth with trying to verify it. Although we don't have that $A$ is $X \cup (A \setminus X)$ constructively, it's still the case that if we interpret $A$ as a discrete locale and think of $X$ and $A \setminus X$ as sublocales, then $A$ is the join of these. If we pass to the dissolution locales of $A$ and $B$, I think we can find an isomorphism assuming the existence of the injections $f$ and $g$, but like I said I'm not completely sure how to verify this.

Cardinality up to congruence

Congruence loses some positive information, of course, but I still think that the proof of Proposition 3 suggests that working up to congruence might make for a smoother theory of some coarse notion of cardinality, which as we saw in Proposition 1 is still enough to prove relatively non-trivial negative statements constructively.

It's a relatively easy exercise to show that congruence of sets plays nicely with $\leq$ and $\leq^\ast$. Specifically, if $A \leq B \sim B' \leq C$, then there are $A' \sim A$ and $C' \sim C$ such that $A' \leq C'$ (with a similar statement for $\leq^\ast$). It's also compatible with a lot of basic set-theoretic operations (such as Cartesian products and disjoint unions). You can even recover some more classical choiceless facts about cardinality working up to congruence. For instance, if $\alpha$ is a trichotomous ordinal and $A \leq^\ast \alpha$, then there is an $A_0 \subseteq A$ with $A_0 \sim A$ such that $A_0 \leq \alpha$.

One notable difficulty with this approach though is that it is not compatible with the power set operation. This is actually fairly easy to see in terms of the example we've already discussed. $\Rb \sim \Qb \cup (\Rb \setminus \Qb)$, but $\Pc(\Rb) \not\sim \Pc(\Qb \cup (\Rb \setminus \Qb))$ (if $\Rb \neq \Qb \cup (\Rb \setminus \Qb)$) because $\Rb \notin \Pc(\Qb \cup (\Rb \setminus \Qb))$.

The thing is though that if we're working up to congruence anyway, maybe the object we should be considering is the power set modulo congruence itself. It's relatively easy to show that if $A \sim B$, then there's a canonical bijection between $\Pc(A)/{\sim}$ and $\Pc(B)/{\sim}$. This loses touch with our more naive notion of cardinality to some extent, but we still have that $\Pc(A)/{\sim} \leq^\ast \Pc(A)$, of course. Moreover, we actually have that $\Pc(A)/{\sim}$ is a retract of $\Pc(A)$: For any $B \subseteq A$, there is a canonical representative of the $\sim$-class of $B$ (among subsets of $A$), namely $\{a \in A : \neg\neg(a \in B)\}$. Therefore $\Pc(A)/{\sim} \leq \Pc(A)$ as well.

The other thing that makes this viable is the fact that Cantor's theorem still works up to congruence in this sense.

Proposition 4. For any $A$, $\Pc(A)/{\sim} \not \leq^\ast A$.

Proof. Fix a partial function $f : {\subseteq}A \to \Pc(A)/{\sim}$. By the above discussion, we may regard this as a function $f : {\subseteq}A \to \Pc(A)$ satisfying that for any $x \in \def\dom{\mathrm{dom}}\dom(f)$, $f(x)$ is $\neg\neg$-stable (i.e., satisfies that for any $a \in A$, $a \in f(x)$ iff $\neg\neg(a \in f(x))$. Let $X = \{x \in A : \neg\neg(x \in \dom(f) \wedge x \notin f(x))\}$. Assume for the sake of contradiction that there is an $a \in \dom(f)$ such that $f(a) = X$. Assume moreover that $a \in X$. This implies that $a \notin f(a) = X$, which is of course a contradiction. Therefore $a \notin X$ and so $\neg\neg(x \notin X)$ and $\neg\neg(x \notin f(a))$, which is also a contradiction. Therefore no such $a$ can exist and $f$ fails to be a surjection. Since this works for any partial function $f$, we have that $\Pc(A)/{\sim}$ is not a subquotient of $A$ (i.e., $\Pc(A)/{\sim} \not\leq^\ast A$. $\square$

We can now use this in large subset arguments fairly easily.

Proposition 5. The MacNeille reals $\Rb_M$ are not subcountable.

Proof. The map $f$ defined in the proof of Proposition $1$ is an injection from $\Pc(\def\Nb{\mathbb{N}}\Nb)/{\sim}$ (regarded as a subset of $\Pc(\Nb)$) into $\Rb_M$ (regarded as a subset of $\Rb_L$). (One quick way to see this is the fact that $\Pc(\Nb)/{\sim}$ is Cantor space and $\Rb_M$ is the classical reals internally in the Boolean subtopos of $\neg\neg$-sheaves, so the classical proof of injectivity of the map of $f$ lifts to a proof here.) $\Pc(\Nb)/{\sim}$ is not subcountable by Proposition 4, so $\Rb_M$ is not subcountable by a large subset argument. $\square$

As mentioned earlier, this also gives a proof that $\Rb_L$ and $\Rb_U$ are not subcountable.

---

For a final thought, as Andrej mentioned in the commments under his answer, one of the things that you can't accomplish by reasoning about cardinality is showing uncountability of the Dedekind reals. Personally, I don't really see this as a failure of the concept of cardinality in the context of constructive math per se. Part of the reason I say this is that a lot of large-scale intuition about cardinality works fine constructively. You can't have an injection from a Grothendieck universe/inaccessible set into any of the flavors of $\Rb$, for instance, or a partial surjection in the other direction, because the big set is 'too big'. Things get 'fuzzy' when you look closely, but as I sort of alluded to at the beginning of my answer, this is fairly common when doing constructive math.

The other part of the reason I say this is that I could easily see someone looking at the facts regarding the Cauchy and Dedekind reals in constructive math and concluding that they're not the "right" definition for the 'full set of real numbers', regarding Cauchy and Dedekind reals as certain special classes of 'nice' real numbers (sort of like the 'good category with bad objects' principle). The MacNeille reals lack good decidability properties, to be sure, but they have the advantage of being a boundedly complete lattice. This means you can actually do things like show that $[0,1]$ is compact in the sense of the finite intersection property. And, as we've seen, you can make fairly classical-looking uncountability arguments go through. Moreover, even though I stated things like Propositions 1 and 5 negatively, they're actually positive in the sense of providing a procedure for building an element not in the range of any given partial map from $\Nb$. In this sense they are as constructive as one could really hope for.

Answer 3

The problem is not whether cardinality is well defined but whether there is anything interesting to say generically: if we go away from classical set theory, in the direction of constructive mathematics, the generic picture potentially has so many possible incarnations that is not to possible to be able to describe them all. For instance, each topos $X$ is a semantic interpretation of set theory. If we consider isomorphism classes of sets in this interpretation, this corresponds subuniverses of the universe of $X$ in the sense of dependent type theory: we are in fact looking at replete and universal classes of maps in $X$: classes of maps stable under pullbacks so that a map isomorphic to a map in the class belongs to the class - if you want your class to be stable under finite union, you may well ask that the class of maps is stable under compositions. If $X$ is the topos of ordinary sets, assuming the excluded middle principle, then cardinals are well ordered and that is it. The only possibility for such subuniverses consists thus in picking a family $C$ of cardinals and to consider maps with fibers of cardinal in the family $C$. But if you take for instance for $X$ the topos of étale sheaves on the big site of schemes of finite presentation on a commutative ring $R$, you may look at the subclass of representable maps, and then at any subclass of interest (étale maps, smooth maps, flat maps, quasi-finite maps, integral maps, radicial maps, proper maps...). Classical finite cardinals correspond in this geometric language to finite étale maps. So what is happening is that subuniverses do not form a totally ordered family anymore, and describing them is not only about size. It is part of the general local or global description of geometric objects. Toposes are so different from each other that it would be unlikely that there is a general description of the structure of cardinals uniformly in all of them: each topos is a specific theory, and classifying subuniverses heavily depends on the theory at hand.