nLab
finite set

Finite sets

Definition

A finite set is a set AA for which there exists a bijection between AA and the set [n]{kN|k<n}[n] \coloneqq \{k\in N | k\lt n\} for some nNn\in N, where NN is the natural numbers.

Classically, the finite sets are the finitely presentable objects in Set. Constructively, the same is true if finitely presented is properly interpreted, see there for details.

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:

  • A set is finite (for emphasis Bishop-finite or BB-finite) if (as above) it admits a bijection with [n][n] for some natural number nn.

  • A set is subfinite (or B˜\tilde{B}-finite) if it admits an injection into some finite set [n][n]; that is, it is a subset of a finite set.

  • A set is finitely indexed (or Kuratowski-finite, KK-finite, or even sometimes, confusingly, subfinite) if it admits a surjection from some finite set [n][n]; that is, it is a quotient set of a finite set.

  • A set is subfinitely indexed (or Kuratowski-subfinite or K˜\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 XX is Dedekind-finite if it satisfies one of the following:

    • any injection XXX\hookrightarrow X must be a bijection.
    • for any function f:Xf\colon \mathbb{N} \to X from the natural numbers, there exist n,mn,m with nmn \ne m such that f(n)=f(m)f(n) = f(m).

    In contrast to the previous three notions, Dedekind-finite infinite sets can coexist with PEM, although countable choice suffices to banish them. The above two versions of Dedekind-finiteness are equivalent under PEM, but constructively they may differ.

In constructive mathematics, one is usually interested in the finite sets, although the finitely indexed sets are also sometimes useful, as are the Dedekind-finite sets in the second sense.

Properties and relationships

Of course, we have

finitelyindexed finite subfinitelyindexed subfinite \array{ & & finitely\;indexed\\ & \neArrow & & \seArrow\\ finite & & & & subfinitely\;indexed\\ & \seArrow & & \neArrow\\ & & subfinite }

Moreover:

  • Finite and subfinite sets have decidable equality. Conversely, any complemented subset of a finite set is finite.

  • Finite sets are closed under finite limits and colimits.

  • A finitely indexed set with decidable equality must actually be finite. For it is then the quotient of a decidable equivalence relation, hence a coequalizer of finite sets. In particular, a set which is both finitely indexed and subfinite must be finite, i.e. the above “commutative square” of implications is also a “pullback”.

  • Finite sets are always projective; that is, the “finite axiom of choice” always holds.

  • However, if a finite set with 22 elements (or any set, finite or not, with at least 22 distinct elements) is choice, or if every finitely-indexed set (or even any 22-indexed set) is projective, then the logic must be classical (see excluded middle for a proof).

  • Finite sets are also Dedekind-finite (in either sense).

  • If filtered category means admitting cocones of every Bishop-finite diagram, then a set is Bishop-finite iff it is a finitely presented object in Set and it is Kuratowski-finite iff it is a finitely generated object in Set.

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 SS) the concept of ‘collection of subsets of SS 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 SS is finite if and only if it is an element of all such collections. Namely, for any set SS we define the following subsets of the power set P(S)P(S).

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

Challenge: Finiteness predicatively without infinity

Can you think of a way to define these notions of finite without power objects and without a natural numbers object? More specifically (and generously), can you define them in an arbitrary locally cartesian closed pretopos with enough projectives?

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.

Properties

The category FinSet of finite sets is equivalent to that of finite Boolean algebras by the power set-functor. See at FinSet – Opposite category for details and see at Stone duality for more.

Revised on July 20, 2014 23:58:34 by Urs Schreiber (82.113.106.220)