Practical Foundations of Mathematics

Paul Taylor

6.6  Finiteness

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 two-element 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 l-calculus, 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 self-inclusions, 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

(a)

finitely enumerated if n Î N and p:n º X are given, where n is the set {m:N|m < n};

(b)

finitely presented if n,k Î N are given together with a coequaliser diagram k\rightrightarrows n\twoheadrightarrow X; the elements of k name laws (and also generate a finite equivalence relation);

(c)

finitely generated if n Î N and a surjection p:n\twoheadrightarrow X are given;

EXAMPLES 6.6.3

(a)

Theorem 5.6.9 requires that the positions in the arity of a general finitary operation must be distinguishable , because we want to put semantic values in them separately.

(b)

If an object is repeated in a family of which we are forming the coproduct, then we get multiple copies of it, which (in the case of Set, Section 5.5) are disjoint.

(c)

However, an element of a semilattice may be repeated arbitrarily in the formation of a join (Proposition 3.2.11 ).

(d)

Any closure condition may be repeated without changing its force.

(e)

An alias in a database specifies that two entries denote the same thing. If we are sure that all such coincidences have been recognised then the database is a finite presentation of its subject matter, otherwise it is a finite generation.

(f)

Any subsingleton {*|f} Ì 1 is finite in all three (``-able'') senses iff f is decidable (Exercise  6.41). More generally, a subset of a finite set is finite iff it is complemented.

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.

(a)

The free monoid on one generator is infinite.

(b)

Addition modulo m is finitely presented as a monoid (generated by one element subject to one law), but it is not free; of course the carrier set is finite.

(c)

The wreath product Z\wr Z is the group generated by symbols a and b subject to the relations that b^-nabⁿ commutes with b^-mab^m for all m,n Î Z. It has no finite presentation.

Any algebra with finitely enumerated carrier for a theory with finitely many operation-symbols 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: Y|f[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

(a)

in C is Kuratowski-finite, since zero has just one;

(b)

on the unit circle S¹ Ì C satisfies $p.p: 2 º X, where the existential quantifier ( cf Example 2.4.8) must be interpreted carefully as above: there is a cover D\twoheadrightarrow S¹ by open subsets each equipped with such an isomorphism, but there is no global one. The collection {p|2 º X}, as a sheaf on S¹, is called a torsor; as an algebraic structure, it retains the Mal'cev operation (u v^-1 w) of the automorphism group of X, but not the identity element (Example  9.2.12(d)).

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^km 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 non-prime 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

LEMMA 6.6.10

(a)

A subset U Ì X belongs to P_f(X) iff U is finitely generable; this property is, in particular, independent of the ambient set X.

(b)

P_f(X) is the smallest set of subsets closed under

Æ\triangleright Æ    and    {U}\triangleright UÈ{x}

(beware that these are elements of P_f(X) on the right of \triangleright ), so by Definition  3.7.8 it gives rise to the Kuratowski induction scheme in its unary form,

omitted prooftree environment

for predicates q on P_f(X), cf Peano induction for N, cons-induction for lists and the unary definition of transitive closure (Definitions 2.7.1, 2.7.3 and 3.8.6). Exercise  6.44 gives the binary induction scheme, corresponding to addition and the append operation.

(c)

The image of a finitely generable set is also finitely generable.

(d)

The coproduct or union of two finitely generable sets is also finitely generable.

(e)

P_f(X) is a semilattice, and hence directed (Definition  3.4.1); seen as a diagram in P(X), the join is X.

PROOF: Many of the parts are immediate corollaries of one another.

(a)

[[a]] ``U Î P<sub>f</sub>(X)'' and ``U is finitely generable'' are both existentially quantified statements. The latter is a surjection p:n\twoheadrightarrow U. In the former we have a list l:List(X), with a function p:n ® X where n = length(l) and p(i) = read(l ,i) (Exercise 2.48). We can show by list induction on l that \polly_!(n) = U.

(b)

[[b]] The second part is now an example of Proposition  6.2.4.

(c)

[[c]] The third follows from the definition of finite generability .

(d)

[[d]] [  ] lists Æ; if t lists U then cons(h,t) lists {h}ÈU; if l₁ and l₂ list \typeU₁ and \typeU₂ then l₁;l₂ lists both \typeU₁+ \typeU₂ and \typeU₁È\typeU₂.

(e)

[[e]] X is the join (within P(X)) of its singletons,  X Ì P_f(X). []

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 Scott-continuity   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:

(a)

X is finitely generable in the listing sense of Definition  6.6.2(c);

(b)

it is finitely generable in the sense of Definition  3.4.11, ie if X = \dirunion_{i Î I}\typeU_i then $i.\typeU_i = X;

(c)

the functor (-)^X preserves directed unions.

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₁,¼,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 hom-set Set(X,-).

DEFINITION 6.6.14 Let X be an object of a category S with finite limits and pullback- stable filtered colimits.

(a)

If the functor H^X º S(X,-):S ® Set preserves filtered colimits then we say that X is externally finitely presentable.

(b)

If S is cartesian closed and the functor (-)^X:S ® S preserves filtered colimits then X is internally finitely presentable.

(c)

If every object of S is a filtered colimit of finitely presentable objects then S is locally internally or externally finitely presentable.

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

(a)

internally iff each of the sets X(n) is finite, although they may grow without bound as a function of n;

(b)

externally iff å_nX(n) is finite, so $m. "n > m.X(n) = Æ.

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