Formalizing the theory of finite sets in type theory

Question

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.

Answer 1

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.

Answer 2

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.