Constructive stone: finite sets

• 07 September 2009
• Andrej Bauer
• Gems and stones

Just like in real life, constructive stones are easier to find than constructive gems, so let me start the series with a stone about constructive finite sets.

There are several possible definitions of finite sets. The one that works best classically and constructively is the following.

Definition: A set `S` is finite when there exists a natural number `n` and a surjective map `e : {1, 2, ..., n} -> S`. We call such an `e` a listing of the elements of `S`.

A listing `e : {1, 2, ..., n} -> S` is conveniently displayed as a list `(e(1), e(2), ..., e(n))`.

Given objects `x_1, x_2, ..., x_n`, not necessarily distinct, we may define the set

`{x_1, ..., x_n} = {x ; x = x_1 or x = x_2 or ... x = x_n}`,

which is finite because it is listed by `(x_1, x_2, ..., x_n)`. Note that a set may have many listings, and that an element may be repeated several times in a given listing. Classical intuition might suggest that we can avoid such repetitions (I can hear you thinking “just remove the repetitions, it's obvious”), however:

Proposition: If every set has a listing without repetitions then the law of excluded middle holds.

Proof. Consider an arbitary truth value `p in Omega`. We need to show that `p or not p` holds. For this purpose consider the finite set `{T, p}` where `T` is the truth value “true”. By assumption, there exists a listing `e : {1, ..., n} -> {T, p}` without repetitions. We know that `n > 0` because `{T, p}` contains an element, namely `T`. If `n = 1` then `T = p`, which means that `p` holds. If `n > 1` then `T != p`, which means that `not p` holds. In either case, `p or not p` holds. QED.

Here are some basic properties of finite sets which hold constructively.

Proposition: (a) Every finite set is either empty or inhabited. (b) If `A` and `B` are finite sets then so are the union `A \cup B` and the cartesian product `A \times B`.

Proof. (a) Recall that a set is inhabited if it contains an element (which is not the same as non-empty). Suppose `e : {1, ..., n} -> S` is a listing of `S`. If `n = 0` then the domain of `e` is the empty set, therefore `S` is also empty. If `n != 0` then `S` is inhabited by `e(1)`.

(b) Suppose `(x_1, ..., x_m)` and `(y_1, ..., y_n)` are listings of `A` and `B`, respectively. Then `A \cup B` is listed by `(x_1, ..., x_m, y_1, ..., y_n)`, and `A \times B` is listed by the “matrix”

`(x_1, y_1), ..., (x_1, y_n)`,
`(x_2, y_1), ..., (x_2, y_n)`,
...,
`(x_m, y_1), ..., (x_m, y_n)`. QED.

So far so good. However:

Proposition: The following are equivalent:

1. The law of excluded middle.
2. Subsets of finite sets are finite.
3. Intersections of finite sets are finite.

Proof. It is well known that in classical mathematics the second and the third claims hold. So we only need to show that each of them implies the law of excluded middle.

Suppose subsets of finite sets are finite. Let `p in Omega` be a truth value and let `S = {1}`. The subset `{x in S ; p}` is finite by assumption, so it is either empty or inhabited. If it is empty then `not p` holds. If it is inhabited then `p` holds. Therefore `p or not p`.

Next, suppose intersections of finite sets are finite. Let `p in Omega` be a truth value and consider the sets `{T}` and `{p}` where `T` is again the truth value “true”. These two sets are finite, therefore by assumption their intersection `{T} \cap {p}` is finite. If it is empty then `T != p` so `not p` holds. If it is inhabited then `T = p` so `p` holds. Therefore `p or not p`. QED.

One way to interpret the last proposition is that we've got the wrong definition of finiteness. Non the less, it is the correct one, at least if you want such theorems as “a polynomial has finitely many roots” to hold. In order to get something that resembles the classical notion of finite sets, we need to bring in decidability.

Definition: (a) A truth value `p` is decidable if `p or not p` holds. (b) A subset `D \subseteq S` is decidable if, for every `x in S`, `x in D` or `not (x in D)`. (c) A set `S` is decidable if, for all `x, y in S`, either `x = y` or `x != y`.

Proposition: (a) A decidable subset of a finite set is finite. (b) The finite subsets of a decidable set are closed under unions and intersections.

Proof. I will leave this one as an exercise. If you try to solve it, make sure you know precisely where you used the assumption of decidability.

Let me finish by saying that in computer science the sort of data structures which are usually called “finite sets” correspond to our decidable finite sets because it is assumed that the elements can be compared for equality. If you try to implement a data structure for finite sets which does not use equality (or a linear order), you will be unable to define intersection and several other operations.

Comments

Bob Harper

10 September 2009 at 00:24

It might be nice to compare various notions of "finite set" from a constructive viewpoint, ie with respect to their computational content. There's a huge (computational) difference between saying "here's a set and a natural number n such that i can map the set injectively into 0..n-1", and "... i can map 0..n-1 onto the set", and "no proper subset of this set can be mapped bijectively to this set".

Peter LeFanu Lumsdaine

11 September 2009 at 07:17

This definition has always slightly puzzled me: not because it's too "un-classical", but because it's not "un-classical" enough --- in particular, I always get nervous when a definition gives 0 special treatment. For instance, as you point out, we can prove "every set is empty or inhabited", i.e. "every finite set has either at most 0 elements or at least 1", but we can't prove analogous things like "every finite set has either at most 1 element, or at least 2" (we can see that this would imply excluded middle by considering the set {T,p} for any truth value p).

On a more practical note, I'd have expected that the same sort of phenomena (like looking at roots of polynomials) that give us finite sets in which we can't decide whether or not there are multiple distinct elements would also give us "finite" sets in which we can't decide whether there's any inhabitant at all?

So I'd rather see a more relaxed definition, something like:

A set S is finite if there is some surjective partial map from some natural number onto S.

Is there a good way to see why this would be unsatisfactory, or why my worries about the standard definition are unfounded?

Andrej Bauer

11 September 2009 at 12:22

Peter (2): There are several notions of constructive finiteness. The one I wrote about is Kuratowski's notion, and it may be characterized as the free join-semilattice completion. The one you suggest ammounts to subsets of finite sets, and that is called subfinite (what is the categorical characterization?). You could restrict subfinite subsets to get a smaller (and more reasonable) class, for example the subsets of finite sets defined by Pi_1^0 predicates are a possibility. Or you could take the intersection of the Kuratowski finite subsets with the compact subsets (with respect to a chosen dominance). There are indeed many possibilites, but the Kuratowski finite sets are the generally accepted "default" notion.