Finiteness

Definition: a collection, N is finite precisely if the reverse of any mapping (N|:N) is a mapping (N|:N). The crucial properties are that:

• if a mapping (N::N) doesn't accept some member of N, then it doesn't accept enough inputs to be able to produce all members of N as outputs, and
• if a mapping (N::N) maps two inputs to the same output, it's not got enough other inputs to cover all the remaining members of N as outputs.

Now, the reverse of a mapping (N|:N) is (in any case) a monic relation (N:|N). [A relation (X:g:Y) is monic iff distinct y in Y have disjoint (|g:{y}) iff each x in X has at most one member for ({x}:g|); dually, a relation (X:g:Y) is a mapping (from Y to X) iff distinct x in X have disjoint ({x}:g|) iff each y in Y has at most one member for (|g:{y}); in the latter case, that one member is known as g(y), so (|g:{y}) is {g(y)}, and g is said to map y to g(y). A relation (X|:Y) relates each member of X to at least some member of Y; a relation (X:|Y) relates, for each y in Y, at least one member of X to y.] Usually, we'll have constructed our mapping (N|:N) in such a way that it's no news to us that its reverse is also a mapping, but (at least in principle) it's allowed to be a relation, though it's bound to be monic. In any case, the definition just given can be rephrased as: a collection N is finite iff every monic (N:|N) is a mapping (N|:N); or, equivalently:

• N is finite iff {mapping (N|:N)} subsumes {monic (N:|N)}

and, although it suffices to prove subsumes, note that this implies {monic (N:|N)} = {mapping (N|:N)}, since: if {mapping (N|:N)} subsumes {monic (N:|N)}, then any mapping (N|f:N) is the reverse of monic (N:reverse(f)|N), which is a mapping (N|:N), so its reverse is monic (N:f|N), whence {monic (N:|N)} also subsumes {mapping (N|:N)}, so these two collections must be equal.

Any collection which is not finite is, conversely, described as infinite. To prove some collection, N, is infinite, it suffices to exhibit a mapping (N| g :N) with (:g|) not equal to N: in such proofs, g will typically be monic, if only to make it easier to see that (|g:) really is N despite (:g|)'s omission. Of course, exhibiting a monic (N:g|N) with (|g:) not equal to N is equivalent, e.g. ({naturals}: successor |{naturals}) is an easy witness that {naturals} is infinite.

For any finite collection, N, and any value i, we can construct a collection S = N&unite;{i}. If i is in N, this is just N, hence finite. Otherwise, consider any monic (S: f |S). If ({i}:f|) is non-empty, it has exactly one member. If that is not i, it must be some n in N; in this case, construct the iso (S|g|S) which relates i to n, n to i and any other j in N to itself. If ({i}:f|) is empty or {i}, take g = S. Either way, we obtain monic (S:g&on;f|S) which relates i to nothing but, possibly, i; consequently, filtering out i as a left value loses no member of N as a right value, so (N:g&on;f|) subsumes N. Thus (N:g&on;f|N) is monic and N is finite, so (N|g&on;f:N) is a mapping: in particular, monic (S:g&on;f|S) relates no value of N to i, yet has i as a right value, therefore does map i to i; and does not relate i to anything but i, hence is a mapping (S|g&on;f:S). Now, g is a mapping and self-inverse, so (S|g|S)&on;(S|g&on;f:S) = (S|f:S) is also a mapping. Thus any monic (S:|S) is a mapping (S|:S), i.e. S is finite. Thus any union of a finite with a singleton is finite: in particular, the successor of any finite collection is always finite.

In general, for any mapping f we know that f&on;reverse(f) = (:x←x:f) = (|f:) is an identity and reverse(f)&on;f is an equivalence: if f is also monic, the latter is the collection (f:z←z:). Any composite of monics is monic, as is any composite of mappings. A composite of mappings is likewise a mapping. If an isoClean composite of mappings is monic, then each of the mappings is also monic.

For some finite N let S be some sub-collection of it and consider an arbitrary monic (S: f |S). We can define a relation (N: g |N) by uniting f with the identity on members of N which are not in S. Since the identity's outputs are none of them in S, and f's outputs are all in S, with f and the identity seperately monic, we find g monic (N:|N), consequently a mapping (N|g:N). Thus g yields all values in S as output, but (S: g :) = f, so f yields all members of S; and is subsumed by a mapping, hence (S|f:S) is a mapping. Thus, any sub-collection of a finite collection is finite.

That immediately tells us that any intersection of collections of which at least one is finite yields a finite collection. For contrast, it's quite easy to construct infinite unions of finite collections (eg the natural numbers): but only if you start out with infinitely many finite collections. I'll come back to that.

If we have a monic mapping (S|f|N), with N finite, we can use it to turn a monic (S:u|S) into a monic (N:g|N) = reverse(f)&on;u&on;f, which is consequently a mapping (N|g:N), whence u = f&on;g&on;reverse(f) is a mapping (S|u:S). Thus S is finite. Provided every monic (S|:N) subsumes a mapping (S|f:N), we can use (f:x←x:) in place of N, which subsumes it and is finite, so (f:x←x:) is finite, to show that the collection of outputs of a mapping from a finite set is always finite.

Assumption: every monic, (:|M), subsumes a mapping, (:|M). Likewise, viewing the reverse, any mapping (N|:) subsumes a monic (N|:). Note that anything a mapping subsumes is a mapping and anything a monic subsumes is monic. I may only need this assumption when N, M are finite, or when each ({n}:g|) or (|g:{m}) is finite; I may refine it or even, eventually, come back with a proof of it, but for now (Oct '98) I'm just assuming it.

Ordering and Size

What I've shown above suffices to define the natural numbers and prove that the union of any list of naturals is natural and, if the list was non-empty, an entry in the list: all other entries in the list are members of this union, which is hence a maximal element. Likewise, any non-empty collection of naturals has natural intersection and this is a member of the collection: furthermore, it is a member of all the others, making it a minimal element.

We can define a relation (which I'll then show to be an ordering) on collections as follows: m ≥ n precisely if there is some (m: monic |n), i.e. precisely if there is some (n| mapping :m); n<m precisely if m≥n and not(n≥m). This coincides with the natural ordering of the naturals by subsumes and in. Since any composite of monics (or mappings) is a monic (or mapping, respectively), ≥ is transitive. It is also reflexive because (n: identity |n) is always monic. We're going to be interested in its restriction to finite collections, which is particularly well behaved.

Being reflexive and transitive is enough to make the relation have the right kind of properties for an ordering: furthermore, I aim to show that it is the intuitively desirable ordering that goes with out expectation that some finite collections are of equal size and others are bigger or smaller than one another. In particular, successor(n) ≥ n for every n because the natural embedding of n in its successor is monic: and I'll want to prove that n isn't ≥ successor(n) when n is finite.

Suppose we have finite n, m with n≥m and m≥n. This means we have monic (m:f|n) and (n:g|m) hence monic (n: g&on;f |n) and (m: f&on;g |m) which are thus mappings (n|:n) and (m|:m) respectively, because n and m are finite. For (|g&on;f:n) to subsume n, (|g:) must subsume n; for (|f&on;g:m) to subsume m, (|f:) must subsume m. For g&on;f to be a mapping, when (|f:) = m subsumes (:g|), g must be a mapping; likewise f must be a mapping for f&on;g to be one. This makes f and g isomorphisms between n and m. Thus n≥m and m≥n imply that n and m are isomorphic, which makes some sense as a notion of same size. Eventually, I'll show that each finite collection is isomorphic to exactly one natural number, which will then be known as the size of the finite collection.

Theorem: there is a mapping ({naturals}|:N) iff N is infinite iff there is a monic (N:|{naturals}).

Proof: clearly the mapping and monic halves of this are equivalent under reversal, so it suffices to show either.

First suppose we have some monic (N: |{naturals}), let g be some mapping (N:|{naturals}) which it subsumes, let M be {i in N: i not in (|g:{naturals})}. Then ({naturals}|reverse(g):N) is a monic mapping also and we can construct s = M&unite;(N: g&on;successor&on;reverse(g) :N), which is monic on M because the other part of the union only accepts members of (|g:) and M is monic (M:|M); and on (|g:) it is a composite of monics, hence monic; so (N:s|N) is monic. However, it doesn't produce g(0) in N as one of its outputs, so isn't epic, hence N is infinite.

Conversely, consider some infinite N: that is, consider some monic mapping (N:g|N) and some n in N but not in (|g:). Define f = (: repeat(i,g,n) ←i |{naturals}), where repeat(0,g,n) is defined to be n while repeat(successor(m),g,n) is defined to be repeat(m,g,g(n)) = g(repeat(m,g,n)): all naturals are either 0 or successors, so this suffices to define f. Consider some natural m for which (:f:m) is monic - e.g. m = empty, of which this is certainly true: we will find (:f:successor(m)) monic precisely if f(m) isn't in (|f:m). Now, if m is empty, we have f(m) = n not in (|f:m) so this is easy: otherwise, m is successor(p) for some p in m, f(m) is g(f(p)) and (|f:m) is {n}&unite;(|g&on;f:p). In the latter case, we know f(m) in (|g:) isn't n and f(p) isn't in (|f:p) so, as g is monic, f(m)=g(f(p)) isn't in (|g&on;f:p); consequently, f(m) isn't in (|f:m) so (:f:successor(m)) is monic. Thus, by induction, every natural m has (:f:m) monic, and f is (N: |{naturals}). Now consider any naturals p, q with f(p) = f(q): the list [p,q] has a maximal element, m, and (:f:successor(m)) is monic with both p and q in successor(m), so f(p)=f(q) implies p = q. Thus f is monic (N: |{naturals}).

Theorem: there is a monic ({naturals}|:S) iff, for every natural n, there is a monic (|:S).

Proof: the forward implication is trivial: the restriction to n of any monic ({naturals}|:S) is a monic (n|:S), as {naturals} subsumes any natural, n. For the converse, we have a mapping ({naturals}| n-> g(n) :{monic (n|:S)}) from which to extract a monic ({naturals}|:S). I shall do this by showing that, given monic (N:f:S) with N natural, g(N) produces at least one value not in (N:f|), thus suitable for use as f(N) with (successor(N):f:) monic. This inductively lets us define f for every natural input, yielding a monic ({natural}| :S) as required.

It suffices to prove that, given natural N and a monic mapping (N:f:S), there is a member of (:g(successor(N))|) which isn't in (N:f|) so we can extend f as above. But g(successor(N)) is monic (successor(N)|:S), so call its reverse h and consider (N: h&on;f :successor(N)), which is monic but not epic, but h is epic, so (N:f|) doesn't subsume (|h), which is (: g(successor(N)) |), so the latter has a member not in (N:f|), as required.

Corollary: for any finite S, there is some natural N for which there isn't a monic (N|:S). This is just the negation of the above (and I may have used the law of the excluded middle somewhere, by now). Since N can be embedded in every natural which subsumes it, and this is monic, there must equally be no monics from naturals subsuming N to S. Thus every natural from which there is a monic to S is a member of N, the set of such naturals is a sub-collection of N, so may be written as a list and has a maximal element, which is the union of all such naturals. Consequently, for any finite S, there is a maximal natural from which there are monics to S: this is known as the size of S.

So, for finite S of size n, consider some monic (n|f:S), and we know that there are no monics (successor(n)| :S). Now, for any s in S, construct a relation (successor(n)| g :S) by g(n) = s, (n:g:) = f: this isn't monic, but f is, so we must have s in (n:f|). Thus (n:f|) subsumes S, and we also know the converse, so S = (n:f|). Reverse(f) is a mapping (S||n) and f is monic (n|f|S), so their composites are (n| f&on;reverse(f) |n) and (S| reverse(f)&on;f |S). The latter is the identity on S, because reverse(f) is a mapping: the former is likewise an equivalence on n. The identity on S is monic, so reverse(f)&on;f is monic. Since the composition here is isoClean, that is (:f|) = (|reverse(f):), this implies reverse(f) also monic, whence f is a mapping (and f&on;reverse(f) is the identity on n). Thus any monic (n|f:S) is a mapping (n:f|S). Since there are monics (n|:S), this also says there are monics (S|:n), so S≥n and n≥S.

Again, for finite S of size n, consider some monic (S|f:N) with N natural. Compose this after some monic (n|g:S) to get a monic (n|:N), so we know N subsumes n. We already know n=N arises, so intersect({natural N: {monic (S|f:N)} is non-empty}) = n and n is a member of any other natural to which there are monics from S. Thus n is the unique natural for which there are monics (n|:S) and (S|:n): furthermore, each monic of either kind is the reverse of some monic of the other kind, hence one-to-one, aka an isomorphism.

Thus, for every finite set there is a unique natural with which it is isomorphic (though there will be as many isomorphisms between them as there are permutations of either), known as its size. In particular the isomorphism, read the right way round, is a monic list of the members of the finite set.

It is now time to discuss arithmetic, exploiting the above, so as to construct finite sums of naturals and thus bound a finite union of finites to be finite in turn.

Suppose we have finite A, D with union U and some monic (U| f :U). Let N be the intersection of A and D and let B, E be the rest of A and D, respectively, so A is the union of B with N, B is disjoint from D, which is the union of E with N and E is disjoint from A. N, B and E are mutually disjoint and all finite. So it will suffice to show that the union of two disjoint finite collections is finite (B with D or A with E).

Consider reverse(f)&on;f, the equivalence relation f induces on its inputs: because f is monic, it's a mapping - the identity on U. Conversely, f&on;reverse(f) is an identity, (f|), subsumed by U.