Could not include mathematicscontents
A finite set is a set for which there exists a bijection between and the set for some , where is the natural numbers.
A set is subfinitely indexed (or Kuratowski-subfinite or -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 it satisfies one of the following:
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.
Of course, we have
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”.
However, if a finite set with elements (or any set, finite or not, with at least distinct elements) is choice, or if every finitely-indexed set (or even any -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.
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 ) the concept of ‘collection of subsets of 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 is finite if and only if it is an element of all such collections. Namely, for any set we define the following subsets of the power set .
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?
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.