Cardinality of sets in constructive mathematics is not as well behaved as in classical mathematics. Cardinalities of finite sets are *not* natural numbers, and cardinalities are *not* linearly ordered.

First of all, constructively we cannot measure the size of finite sets with natural numbers. As soon as we require that the cardinality of singletons be 1, we’re in trouble (recall that a set `S` is a *singleton* when there exists an element of `S` and, for all `x, y`, if `x in S and y in S` then `x = y`):

Proposition:Suppose `c` is a map which assigns to each finite set a natural number, such that `c(S) = 1` if, and only if, `S` is a singleton. Then the law of excluded middle holds.

*Proof.* (Think of `c` as a candidate map for measuring cardinality.) Consider an arbitrary truth value `p in Omega` and let `S = {T, p}` where `T` is the truth value “true”. Either `c(S) = 1` or `c(S) != 1`. If `c(S) = 1` then `S` is a singleton, therefore `T = p` and `p` holds. If `c(S) != 1` then `S` is not a singleton, therefore `T != p` and `not p` holds. This establishes `p or not p`. QED.

(Side remark: *decidable* finite sets do have a well-defined number of elements, which is a natural number, because every such set has a listing without repetitions. See this constructive stone for details.)

If the natural numbers are not suitable for measuring the size of a finite set, then perhaps some other linear order is?

Proposition:Let `<` be an irreflexive relation on a set or class `P` such that `x < y or x = y or y < x` for all `x, y in P`. Suppose `c` is a map which assigns to each set a value in `P` such that `c(A) = c(B)` if, and only if, there is a bijection between `A` and `B`. Then the law of excluded middle holds.

*Proof.* (Think of `P` as the class of cardinal numbers, `<` the strict order on them, and `c` a candidate cardinality function.) Given any truth value `p in Omega`, consider the sets `A = {T, p}` and `B = {T}`. Either `c(A) < c(B)`, or `c(A) = c(B)`, or `c(B) < c(A)`. If `c(A) = c(B)` then `A` and `B` are in bijective correspondence, therefore `A` is a singleton and `T = p`, which means that `p` holds. If `c(A) < c(B)` or `c(B) < c(A)` then by irreflexivity of `<` we have `c(A) != c(B)`, therefore `A` is not a singleton and `T != p`, which means that `not p` holds. In any case, `p or not p` holds. QED.

The previous proposition tells us that we cannot hope to have a sensible notion of cardinals ordered by a strict linear order. Perhaps a non-strict linear order can be used to measure cardinalities constructively? The answer is negative:

Proposition:Let `<=` be a partial order on a set or class `P` such that `x <= y or y <= x` for all `x, y in P`. Suppose `c` is a map which assigns to each set a value in `P` such that `c(A) <= c(B)` if, and only if, there is an injection of `A` into `B`. Then the following non-constructive law holds: `forall p, q in Omega, (p => q) or (q => p)`.

*Proof.* Consider arbitrary truth values `p, q in Omega`. Let `S = {1}`, `A = {x in S ; p}` and `B = {x in S ; q}`. By assumption, either `c(A) <= c(B)` or `c(B) <= c(A)`. In the first case we have an injection `i : A -> B`, therefore `p => q`. Indeed, if `p` holds then `1 in A` and so `i(1) = 1 in B`, hence `q` holds. Similarly, if `c(B) <= c(A)` then `q => p`. In either case, `(p => q) or (q => p)`. QED.

The logical law `(p => q) or (q => p)` was studied in Michael A. E. Dummett, “A Propositional Calculus with a Denumerable Matrix”, Journal of Symbolic Logic, Vol 24 No. 2 (1959), pp 97-103. It is not provable constructively, and it is implied by the law of excluded middle, see this Coq library for proofs.

I would be curious to know if the assumptions of the above proposition imply the law of excluded middle:

Question:Let `<=` be a partial order on a set or class `P` such that `x <= y or y <= x` for all `x, y in P`. Suppose `c` is a map which assigns to each set a value in `P` such that `c(A) <= c(B)` if, and only if, there is an injection of `A` into `B`. Does the law of excluded middle follow?

By the way, nothing much changes if in the proposition above we replace the existence of an injection of `A` into `B` with the existence of a surjection from `B` onto `A`. That’s an exercise for you.

It would be wrong to conclude from this post that cardinality of sets does not make sense constructively. We can still compare sets by their sizes, for example, we could say that `A` is smaller than `B` when there is an injection of `A` into `B`. That would give us a reflexive, transitive relation on sets. However, whatever our notion of size is, we cannot expect it to be a linear order: there will always be sets which are incomparable in size.

I’m enjoying this series, but can’t shake the feeling that what you are showing is not the difficulties for constructivist mathematics per se, but the difficulties of conceiving it as “just” classical mathematics minus the law of the excluded middle.

Letâ€™s say we flip the assumption around and start with the decidable finite cases as the “normal” ones. Then it is the introduction of undecidability and infinity that blurs things and invalidates the law of the excluded middle, and requires more care to avoid paradoxes and fallacies.

With this approach, we end up with a mathematics where the constructive portions look a lot more like our naive intuitions and experience of numbers, and the â€œstonesâ€ become those of classical mathematics.

I realize this might seem heretical to pure mathematicians trained in the last century or so ;-), but it is essentially orthodox in theoretical computer science, for example.

This is a wonderful series. Thanks for posting it!

The proofs so far seem all to rely on a “denotational” equality between propositions. It seems trivial that `p or not p` with such a coarse equality, since you can always just test whether `p = T`.

(Maybe I don’t understand what you mean by an arbitrary truth value `p in Omega`–is that different from a proposition?)

This “denotational” equality seems inherently nonconstructive to me. What do we get if we use a finer equality? Is that meaningful in this setting?

Iâ€™m starting to doubt that sets are the proper abstraction to study. Wouldnâ€™t lists be more appropriate?

If you do insist on using sets, Iâ€™d at least like to know what the word means to you. Is it something I can define in Agda, or do I need to postulate (âŸ¨SetâŸ© : Set) as well as all the ZFC axioms?

Reply to Jake (3): what do you mean by “test whether `p = T`”? It sounds like you expect equality to be somehow classical, i.e., two things are either definitely equal or definitely not-equal. In reality, the truth value `p = T` is `p`. Equality on the set of truth values `Omega` is the same thing as logical equivalence, i.e., `p = q` means `(p => q) and (q => p)`. It’s not like we get to choose different equalities on our sets. Equality is a primitive notion, and it makes perfect sense constructively.

Reply to Samuel (4): lists are too limited because not every mathematical object is a list, or the image of a list. I am doing constructive mathematics informally in the style of Bishop. But if you press me, I will say that I am using higher-order intuitionistic logic, i.e., the internal language of a topos. This would be a bit like an impredicative Agda in which Prop is a type. And by the way, ZFC implies classical logic (because the axiom of choice implies the law of excluded middle). There is IZF, intuitionistic Zermelo-Fraenkel, but I don’t need that. Topos if fine, and most of the arguments can be rephrased in type theory, if you read “set” as “setoid” and `Omega` as Prop.

Andrej (5): no, I don’t expect equality to be classical; I am coming at this with a syntactic prejudice, so whether some proposition `p` (to me, some syntax tree) is equal to `T` must be decided.

In the argument “if `c(S) != 1` then `S` is not a singleton, therefore `T != p` and `not p` holds”, I find it troubling that `S` not a singleton implies `T != p`. Can we not have a set `S = {T, p}` where we don’t know whether `T = p`? Or, does it even make sense to call the set a singleton or not when we don’t know whether `T = p`?

Jake (6): the details are as follows. Suppose `S = {T, p}`. The statement “`S` is a singleton” is equivalent to `p`. Indeed: if `p` holds then `T = p` and `S = {T}`, a singleton. Conversely, if `S` is a singleton then `T = p`, which means that `p` holds.

In other words, if you do not know whether `p` holds then you do not know whether `S` is a singleton, and vice versa. But if you know that `S` is not a singleton, then you know that `p` does not hold.

Maybe the right spin here is that the classical concept of cardinality is really not all that important. After all, it has rather poor properties when considered constructively, and I cannot think of very many things in math, other than those to do with cardinality itself, that rely on sets having definite sizes that are lined up linearly. It’s just a weird, possibly irrelevant, and, in the infinite case, rather poorly defined notion (relying as it does on arbitrary functions) anyway.

Andrej (7): Thanks for the explication (and for editing my previous comment). In other words the existence of `c` implies that we know whether each `S` is a singleton or not, and therefore that `p or not p`.

In the first proof you said:

“Either c(S)=1 or c(S)â‰ 1. … This establishes pâˆ¨Â¬p.”IANAM (I am not a mathematician), but isn’t this circular? You presuppose in the first sentence what you were trying to prove.

This is probably just a silly misunderstanding on my part, but anyway, I had to ask. :)Rok: there is no circularity. Here `c` is a function which maps into the natural numbers `N`. For the natural numbers we can prove by induction that `forall n : NN, n = 1 or n != 1` (try it). So what you call “presupposition”, namely that “either `c(S) = 1` or `c(S) != 1`” is something that we can actually prove separately.

Ah, it really was a very silly remark. Thanks for the explanation. :)