Most proof assistants have a formalization of the concept of "finite set". These formalizations, however, differ wildly (although one hopes that they are all essentially equivalent!). What I don't understand at this point is the design space involved, and what are the pros and cons of each formalization.

In particular, I would like to understand the following:

  • Can I axiomatize finite sets (i.e. types inhabited by a finite number of inhabitants) in simple type theory? System F? What are the drawbacks of doing it this way?
  • I know it can be done 'elegantly' in a dependently typed system. But, from a classical point of view, the resulting definitions seem extremely alien. [I am not saying they are wrong, far from it!]. But I do not understand why they are 'right' either. I understand that they pick out the correct concept, but the deeper reason for 'saying it that way' is what I do not fully grasp.

Basically, I would like a reasoned introduction to the design space of formalizations of the concept of 'finite set' in type theory.


I know it can be done 'elegantly' in a dependently typed system. But, from a classical point of view, the resulting definitions seem extremely alien.

Can you explain what you mean by "alien"? It seems to me that you formalize the concept of finite set in precisely the same way in type theory and in set theory.

In set theory, you proceed by defining the set $Fin(n)$ as $$ \mathrm{Fin}(n) \triangleq \{ k \in \mathbb{N} \;|\; k < n \} $$ Then, you define the finiteness predicate as: $$ \mathrm{Finite}(X) \triangleq \exists n\in\mathbb{N}.\; X \simeq \mathrm{Fin}(n) $$ Where $A \simeq B$ means isomorphism of sets.

In type theory, you can do exactly the same thing! $$ \mathrm{Fin}(n) \triangleq \Sigma k:\mathbb{N}.\; \mathsf{if}\; k < n\,\mathsf{then}\; \mathsf{Unit} \;\mathsf{else}\; \mathsf{Void} $$ Note that $\mathrm{Fin}(n)$ is a type with $n$ elements (since the second component of the pair is proof-irrelevant). Then, you can define the finiteness type constructor as: $$ \mathrm{Finite}(X) \triangleq \Sigma n:\mathbb{N}.\; X \simeq \mathrm{Fin}(n) $$ Where $A \simeq B$ means isomorphism of types.

  • $\begingroup$ Alien because I only ever saw the raw definitions with no accompanying test which explains how to read those definitions. Plus the fact that the usual Fin definition, done inductively, obscures things further. Your short explanation is what I needed to make it click. $\endgroup$ Sep 14 '13 at 12:25

Let me see if I can add anything useful to Neel's answer. The "design space" for finite sets is much larger constructively that it is classically because various definitions of "finite" need not agree constructively. Various definitions in type theory give slightly different concepts. Here are some possibilities.

Kuratowski finite sets ($K$-finite) can be characterized as the free $\lor$-semilattices: given a set, type or object $X$, the elements of the free $\lor$-semilattice $K(X)$ can be thougth of as finite subsets of $X$. Indeed, each such element is generated by:

  • the neutral element $0$, which corresponds to the empty set, or
  • a generator $x \in X$, which corresponds to the singleton $\lbrace x \rbrace$, or
  • a join $S \lor T$ of two elements, which corresponds to a union.

An equivalent formulation of $K(X)$ is: $S \subseteq X$ is $K$-finite if, and only if, there exists $n \in \mathbb{N}$ and an surjection $e : \lbrace 1, \ldots, n \rbrace \to S$.

If we compare this with Neel's definition we see that he requires a bijection $e : \lbrace 1, \ldots, n \rbrace \to S$. This amounts to taking those $K$-finite subsets $S \subseteq X$ which have decidable equality: $\forall x, y \in S . x = y \lor x \neq y$. Let us use $D(X)$ for the collection of decidable $K$-finite subsets of $X$.

Obviously $K(X)$ is closed under finite unions, but it need not be closed under finite intersections. And $D(X)$ is not closed under any operations. Since people expect that finite sets behave a bit like a "Boolean aglebra without a top" one could also try to define them as the free generalized Boolean algebra ($0$, $\lor$, $\land$ and relative complements $\setminus$), but I actually never heard of such an effort.

When deciding what the "correct" definition is, you have to pay attention to what you want to do with the finite sets. And there is no single correct definition. For instance, in what sense of "finite" is the set of complex roots of a polynomial finite?

See Constructively finite? by Thierry Coquand and Arnaud Spiwack for a detailed discussion of finiteness. The lesson is that finiteness is far from obvious constructively.

  • $\begingroup$ Right, I knew just enough of this to know that my question was not trivial. Now I can go and reread the parts of the Coq, Isabelle, and Agda libraries that deal with finite sets, and have a hope of understanding which choices (pun intended) they have made. $\endgroup$ Sep 15 '13 at 14:29
  • $\begingroup$ I wonder how aware the authors of the libraries were of the choices. They probably just walked into one of the definitions. A natural thing to do is to assume that $A$ has decidable equality because then $K(A)$ coincides with $D(A)$ and everything goes smoothly and a lot like in the classical case. The trouble starts once $A$ does not have decidable equality. $\endgroup$ Sep 15 '13 at 15:08
  • $\begingroup$ To be fair, one often uses finite sets to formalize aspects of program verification, and in that case you can usually assume that decidable equality holds. $\endgroup$
    – cody
    Sep 18 '13 at 14:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.