<blockquote>
  <p>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.</p>
</blockquote>

<p>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. </p>

<p>In set theory, you proceed by defining the set $Fin(n)$ as 
$$
  \mathrm{Fin}(n) \triangleq \{ k \in \mathbb{N} \;|\; k &lt; 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. </p>

<p>In type theory, you can do exactly the same thing! 
$$
  \mathrm{Fin}(n) \triangleq \Sigma k:\mathbb{N}.\; \mathsf{if}\; k &lt; 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. </p>

CC BY-SA 3.0
2013-09-14T12:25:21.033Z
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.
Jacques Carette
CC BY-SA 3.0
2013-09-13T12:06:24.410Z
2013-09-13T19:20:08.297Z
2013-09-13T19:20:08.297Z
Neel Krishnaswami
<p>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.</p>

<p><em>Kuratowski finite sets</em> ($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:</p>

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

<p>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 <em>surjection</em> $e : \lbrace 1, \ldots, n \rbrace \to S$.</p>

<p>If we compare this with Neel's definition we see that he requires a <em>bijection</em> $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$.</p>

<p>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.</p>

<p>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 <a href="http://msp.org/pjm/2000/196-1/pjm-v196-n1-p10-s.pdf">the set of complex roots of a polynomial finite</a>?</p>

<p>See <a href="http://hal.archives-ouvertes.fr/docs/00/50/39/17/PDF/Coquand_Spiwack_-_2010_-_Constructively_Finite.pdf">Constructively finite?</a> by Thierry Coquand and Arnaud Spiwack for a detailed discussion of finiteness. The lesson is that finiteness is far from obvious constructively.</p>

CC BY-SA 3.0
2013-09-15T14:29:19.647Z
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.
Jacques Carette
CC BY-SA 3.0
2013-09-15T15:08:07.033Z
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.
Andrej Bauer
CC BY-SA 3.0
2013-09-18T14:46:24.240Z
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.
cody
CC BY-SA 3.0
2013-09-15T08:27:35.640Z
2013-09-15T08:27:35.640Z
Andrej Bauer
<p>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.</p>

<p>In particular, I would like to understand the following:</p>

<ul>
<li>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?</li>
<li>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 <em>correct</em> concept, but the deeper reason for 'saying it that way' is what I do not fully grasp.</li>
</ul>

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

<type-theory><dependent-type><finite>
Formalizing the theory of finite sets in type theory
Jacques Carette
# Formalizing the theory of finite sets in type theory

(Asked by: username_0 on 2013-09-12)

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.

**Tags:** type-theory, dependent-type, finite

---

## 2 answers

### Answer by username_1 on 2013-09-13. Score: 8 | Accepted answer

> 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.

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_2 on 2013-09-15. Score: 6

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](http://msp.org/pjm/2000/196-1/pjm-v196-n1-p10-s.pdf)?

See [Constructively finite?](http://hal.archives-ouvertes.fr/docs/00/50/39/17/PDF/Coquand_Spiwack_-_2010_-_Constructively_Finite.pdf) by Thierry Coquand and Arnaud Spiwack for a detailed discussion of finiteness. The lesson is that finiteness is far from obvious constructively.

> **Comments:**
> **username_0**: 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.  
> **username_2**: 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.  
> **username_3**: 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.  

---

