nLab
finite set

Definition

A finite set is a set $A$ for which there exists a bijection between $A$ and the set $\{k\in N\mid k<n\}$ for some $n\in N$, where $N$ is the natural numbers.

Classically, the finite sets are the finitely presentable objects in Set.

The category FinSet of finite sets and functions between them is essentially the subject matter of combinatorics?; it's fundamental in the subject of structure types.

Finiteness constructively and internally

In constructive mathematics, and internally to a topos, a number of classically equivalent notions of finiteness become distinguishable. In addition to the above notion (for which one generally reserves “finite”), we have the following.

• A set is subfinite if it admits an injection into some finite set.

• A set is finitely indexed (also called Kuratowski-finite, K-finite, or even sometimes, confusingly, subfinite) if it is a surjective image of some finite set.

• A set is subfinitely indexed (also called $\tilde{K}$-finite) if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set; that is, it is a subquotient set of a finite set.

• A set is Dedekind-finite if any injection from it to itself must be a bijection. In contrast to the previous three notions, Dedekind-finite infinite sets can coexist with PEM, although countable choice suffices to banish them.

In constructive mathematics, one is usually interested in the finite sets, although the finitely indexed sets are also sometimes useful. Note that a finitely indexed set with decidable equality must actually be finite.

Finite sets are always projective; that is, the “finite axiom of choice” always holds. However, if any finite set greater than 1 is choice, or if every 2-indexed set is projective, then the logic must be classical (see excluded middle for a proof).

Finiteness without infinity

The above definition of “finite,” and hence all the above definitions except for Dedekind-finiteness, only make sense given the set of natural numbers, i.e., given an axiom of infinity. However, they can all be rephrased to make sense even without an axiom of infinity (and thus in a topos without a natural numbers object). Basically, you define (for a given set $S$) the concept of ‘collection of subsets of $S$ that includes all of the finite subsets’ by requiring it to be closed under inductive operations appropriate for the sense of ‘finite’ that you want; then $S$ is finite if and only if it is an element of all such collections. Namely, for any set $S$ we define the following subsets of $P(S)$.

• $K(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A\mapsto A\cup B$ for $A$ a subset of $S$ and $B$ a singleton in $S$. Then $S$ is finitely-indexed iff $S\in K(S)$. Note that $K(S)$ is also the free semilattice generated by $S$.
• $\tilde{K}(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A\mapsto A\cup B$ for $A$ a subset of $S$ and $B$ a subsingleton in $S$. Then $S$ is subfinitely-indexed iff $S\in \tilde{K}(S)$.
• $F(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A\mapsto A\cup B$ for $A$ a subset of $S$ and $B$ a singleton in $S$ disjoint from $A$. Then $S$ is finite iff $S\in F(S)$.
• $\tilde{F}(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A\mapsto A\cup B$ for $A$ a subset of $S$ and $B$ a subsingleton in $S$ disjoint from $A$. Then $S$ is subfinite iff $S\in \tilde{F}(S)$.

Challenge: Finiteness predicatively without infinity

Toby: Can you think of a way to define these notions of finite without a set of truth values and without a natural numbers object? Equivalently, can you define them in an arbitrary locally cartesian closed pretopos? (Use the axiom of subobject collection if necessary.)

Finite objects in a topos

In a topos, there are both “external” and “internal” versions of all the above notions of finiteness, depending on whether we interpret their meaning “globally” or in the internal logic of the topos. See finite object.