It probably comes as something of a surprise that we have got this far through a book on foundations of mathematics  especially a book which stresses constructivity  without discussing finiteness. Emphasis on finite enumeration was a reaction to the excesses of classical set theory, and clearly any set which is given by picking its elements must be finite in order to be represented in a machine.
The reason why we have played down finiteness is that mathematical and computational objects are normally handled according to their structure, with no need for explicit enumeration. Besides, enumerative processes are very slow: one does not have to go to a very high order of functions over a twoelement base type to exhaust the memory of a computer, or indeed of the Universe. We can nevertheless handle higher order functions very easily with the lcalculus, and prove certain properties of all numbers by induction without examining each one.
Arguments in combinatorics usually do make essential use of finite sets. Unfortunately it is for these that the type theory and logic tend to be the most difficult to mechanise (although the combinatorial aspects can be handled directly), whereas Section 1.6 showed that variables, the connectives and the quantifiers can be translated very fluently between the vernacular and formal language. When a proof does need finite sets, considerable bureaucratic manipulation of lists must be added to the level of detail that a (human) mathematician would regard as sound and precise. Even this section elides many such details, since we have already said as much about lists as we intend to say.
When we have spoken of finite sets in this book, notably in the definition of algebraic theories and the crucial result about quotients of algebras, we have usually had in mind particular numbers, such as 3. It is said that ``hard cases make bad law'': each instance of finiteness is familiar, but it is very difficult to identify the abstract notion.
Adam of Balsham (1132) observed that the difference between finite and infinite sets is that the latter admit proper selfinclusions, such as n® 2n ( cf Exercises 1.1 and 2.47). But, without Choice, only special infinite sets have this property, so the rest are inappropriately called ``finite.''
As with the exactness properties of Set (Section 5.8), progress was made only after similar concepts had been identified in algebra and topology. In these disciplines, many familiar objects, despite having infinitely many elements, are ``bounded'' in some sense which may be used to investigate their properties. For example [0,1] Ì R is compact (if it is contained in any directed union of open sets then just one of them suffices), whence any continuous function on it is bounded and attains its bounds.
EXAMPLE 6.6.1 A commutative ring R is said to be Noetherian if every directed set of ideals is eventually constant. Assuming excluded middle and Dependent Choice, every element a Î R of such a ring can be expressed as a product of irreducibles ( cf Example 2.1.3(b) for prime factorisation).
PROOF: If a is reducible then a = bc, where the ideals they generate satisfy (a)\subsetneqq (b)\subsetneqq R. Repeating this process, we get either a product as required or, by Dependent Choice (Definition 1.8.9), a properly increasing sequence of principal ideals, which is forbidden by hypothesis. []
Emmy Noether was the pioneer of conceptual mathematics ( begriffliche Mathematik), but this notion is no mere piece of abstract nonsense. Since it is inherited by quotients, polynomial rings and even formal power series rings, it replaced the ``jungle of formulae'' (as she described her own doctoral thesis) which had characterised nineteenth century algebra ( cf Exercise 6.49).
Three definitions by counting Of course a set is finite iff there is a listing of its elements, and we know from Section 2.7 what a list is. Classically (more precisely, when equality is decidable), any repetition in such a list may be eliminated, but anyone who has tried to maintain a moderately large database will be aware that this is not a trivial problem in practice. Depending on the amount of control we have over repetition, there are three useful definitions.
DEFINITION 6.6.2 A set X is said to be
It does not seem to be an appropriate property to require of a notion of finiteness that any subset of a finite set be finite (but cf Remark 9.6.5). As with the connectives of logic and type theory, we shall take natural deduction for finite sets (rather than the prejudices of classical logic) as our guide, and this matches the definitions we have given.
REMARK 6.6.4 There are similar (and in fact prior) notions in algebra. The first corresponds to Fn, the free algebra on n generators (such as a finite dimensional vector space), which replaces the set n in the others. This analogy is a conceptual one, and is only tenuously related to the size of the carrier sets. The algebraic definitions are also distinguishable even in classical logic.
Any algebra with finitely enumerated carrier for a theory with finitely many operationsymbols is finitely presented as an algebra: for laws we just list the instances of the operations ( cf the ambiguity in the usage of this word mentioned in Definition 1.2.2). However, there is no other implication. We shall compare and contrast these definitions further in Proposition 6.6.13ff.
The ability to count We have usually avoided discussing the external interpretation of logic, but it is important to understand the meaning of the existential quantifier (``able'') in these definitions.
REMARK 6.6.5 Recall from Remark 5.8.5 that G\vdash$y: Y.f[y] means that !:{y: Yf[y]}® G is epi. Thus an object X is finitely enumer able or gener able iff

["m:N."x,y: X. m,x,m,y Î pÞ x = y] Ù["m.m < nÛ ($x.m,x Î p)] Ù["x.$(!)m.m,x Î p],
in which we read $! in the case of enumeration and $ for generation.
The left projection D® N, an element n Î N^{D} , may be regarded as a ``variable number,'' viz the generic length of a way of listing the set. For i < n, ie i Î N^{D} with "d.i(d) < n(d), we have x_{i}(d) = p(i(n,p)) Î X where d = (n,p) Î D. In other words, we may write

Now consider the introduction and elimination rules for the quantifier.

COROLLARY 6.6.6 If a set is finite in either sense then we may assume that it has a listing (with or without repetition). []
This means that we do not need to mention the set D when working in the internal logic, nor are we making a choice of listing (Remark 1.6.7). But this box, like all others, must be properly nested. So if the set X depends on parameters, the ($E ) box which encloses the choice of listing must be closed before any surrounding box which quantifies the parameters.
However, there are problems with counting even when we seem to be able to identify a specific number of distinct things.
EXAMPLES 6.6.7 The set X of square roots of a generic number
To sum up, we are not at liberty to regard the listing of a dependent finite set X[y], or even the number of elements needed to cover a Kuratowski finite set, as a function of y.
Counting is unique But if a set can be finitely enumerated then the length of such an enumeration is an invariant. Although this must have been known as a fact before any other human intellectual achievement, the realisation that there is (a) a powerful theorem, and (b) something to prove, takes a degree of mathematical sophistication.
Bo Peep's Theorem (Exercise 1.1) amounts to saying that any injection n\hookrightarrow n is a bijection. The pigeonhole principle is a stronger result: if f:n® m with m < n then f(i) = f(j) for some i ¹ j Î n.
These properties fail, of course, for big sets like N, but finiteness is also about granularity. This is the reason for only allowing decidable subsets of finite sets to be called finite. For example, if I give you some wool, and some more wool, and a third quantity, and then take some back, and some more, and some more again, you may or may not still be holding some of what I gave you.
Besides its usefulness in agriculture, the power of counting is illustrated by the Sylow theorems in group theory.
FACT 6.6.8 Let G be a group with p^{k}m elements, where p is a prime not dividing m. Then there is a subgroup H Ì G of order p^{k}. Moreover the number n of such subgroups (which are conjugate to each other in G) divides m, and n º 1modp. If n = 1 then H is normal. []
By counting Sylow subgroups and elements of particular orders we may easily identify the simple group of order 168 and show that there is no simple group of small nonprime odd order (105 is the first tricky case).
Finite subsets Now let us look more closely at Kuratowski finiteness, which is apparently an exception to the rule that the poset version of a concept is simpler and older than the categorical analogue. This is the one which is usually relevant for subsets, since the other requires equality of elements to be decidable before we may form the subset {a,b}.
Although the induction scheme is the main feature to which we want to draw attention, we shall continue the discussion based on lists instead of developing the theory from the closure conditions as we did for the transitive closure in Definition 3.8.6ff ( cf Exercises 3.60 and 6.43).
There are rules for adding elements and subsets, corresponding to cons and append for lists. P_{f}(X) is the free semilattice on a set X, just as List(X) is the free monoid (Corollary 2.7.11).
DEFINITION 6.6.9 The finite powerset is the image



PROOF: Many of the parts are immediate corollaries of one another.
PROPOSITION 6.6.11 P_{f}(X) is the free semilattice on X.
PROOF: Let f:X® Q be a function to another semilattice, in which (by Proposition 3.2.11) the operations may be taken to be ^ and Ú. By Kuratowski induction, (Q, £ ) has joins of all finitely generable sets, but if U Ì X is finitely generable then so is its image p(U) = \fred_{!}(U) Ì Q, so it has a join. Hence there is a semilattice homomorphism P_{f}(X)® Q extending f; it is unique because the equaliser of any two such is a subalgebra, but there is no proper such. See also Exercise 6.45(a). []
The empty set Corresponding to List(X) º {*} +XxList(X), an element of the free semilattice can be parsed as empty or inhabited.
COROLLARY 6.6.12 P_{f}(X) is the disjoint union of {Æ} and P^{ ¹ 0}_{f}(X), the set of inhabited finitely generable subsets; the latter is the free algebra for binary join alone. In other words, it is decidable whether a finitely generable subset is empty or has an element, cf Example 6.6.3(f).
PROOF: {^,T} is a semilattice; the unique homomorphism taking all singletons to T maps everything else there except Æ. []
Finiteness and Scottcontinuity Theorem 3.9.4 established a link between the (Kuratowski)finite arities of Horn theories and preservation of directed joins. We should therefore look for a categorical analogue involving finite presentability. To recap,
PROPOSITION 6.6.13 The following are equivalent for a set X:
Moreover every set is the directed union of its finitely generated subsets.
PROOF: [b] is a special case of (c), and the last part is Lemma 6.6.10(e), whence [bÞ a]. [a Þ c] Any function f:{x_{1},¼,x_{n}}® È_{i} \typeV_{i} factors through some \typeV_{i}. []
It can also be shown that a set is finitely presentable iff ()^{X} preserves filtered colimits (Example 7.3.2(j)), and conversely that every set can be expressed as a filtered colimit of finitely presentable sets. This suggests a generalisation, since, for Set, the exponential ()^{X} is the same as the homset Set(X,).
DEFINITION 6.6.14 Let X be an object of a category S with finite limits and pullback stable filtered colimits.
The algebraic notions of finiteness (Remark 6.6.4) can be shown to be equivalent to the external ones for S = Mod(L), where L is a finitary algebraic theory. Mod(L) is locally externally finitely presentable; Peter Gabriel and Friedrich Ulmer [GU71] showed that every locally externally finitely presentable category which also has all small colimits is of this form, for some essentially algebraic theory in the sense of Remark 5.2.9. The term LFP is traditionally applied only to such categories, in contrast to algebraic dcpos, Definition 3.4.11.
EXAMPLES 6.6.15 To make the distinction clearer, let S = Set^{N} be the category of presheaves on N. Then X Î obS is finitely presentable
The terminal object \terminalobj_{S} = ln.{*} is internally but not externally finite. Nor need finitely enumerable presheaves (finite sets dependent on n Î N) be expressible externally as coproducts of copies of the constant set 1.
This, and the fact that emptiness or habitation of a Kuratowskifinite set is decidable, illustrate that singletons are rather big subsets. In this case how is it that every set is the directed union of its finitely generable subsets? If it only consists of partial singletons, the nodes of the diagram (other than Æ) are themselves partial.
Finiteness, therefore, is not a prerequisite to constructive mathematics, nor is it ``obvious'' what it means. On the other hand, it is amenable to logical and categorical study.