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.

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}).

... notational mess ... reversal being transformed, ← replacing -> ...

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.

Written by Eddy.