In classical set theory, one can define finiteness of sets by what's known
as the pigeonhole principle

, which I can express as: a set S is finite
precisely if {monic (S:|S)} = {mappings (S|:S)}; i.e. for a mapping (relating
at most one left value to any given member of S, as right value –
a.k.a. input) to succeed in producing every member of S as an output (left
value), it must in fact accept every member of S as an input and can map at
most one member of S to any given output.

Given that my raw material is, in place of sets, relations: I reserve the right to generalise this principle to a definition which is applicable to a general relation; given that I chose to allow context to use an arbitrary equivalence relation as its notion of equality, any such generalisation needs to be quite carefully thought out if is to work well. For the present, however, my needs are amply met by the fore-going restatement of the pigeonhole principle, save that I apply it to collections rather than sets (since I don't define sets and collections are what takes their place in my work) and I'm rather more reticent, than classical set theory, about expecting facts about membership to be decidable.

I'll say that a collection A **pigeonholes** a collection B
precisely if {monic (A:|B)} subsumes {mappings (A|:B)}; i.e. every mapping
from within B to all of A does in fact use all of B and never repeats any
output. Reversing each member of the two derived collections, this implies
that {mappings (B|:A)} subsumes {monic (B:|A)}; so, if B also pigeonholes A,
then {mappings (B|:A)} = {monic (B:|A)}. A collection
is **finite** precisely if it pigeonholes itself; otherwise, it
is **infinite**.

First let's check the implications of that make sense for the simplest collections – the empty collection and singletons. Then we can go on to examine some more general results which (shall in fact imply these initial results, and) suffice to describe the natural numbers.

The empty relation (for which the question does it relate
this to that ?

*always* gets the answer no

) is
necessarily a collection (there are no *distinct* x, y for which it
relates x to y) and, for any collection A, the only relation (A::empty) is
empty itself, which is monic, a mapping and (A:|empty). Thus {monic
(A:|empty)} subsumes {relation (A::empty)}, which subsumes {mappings
(A|:empty)} as a matter of course; thus every collection pigeonholes
empty. In particular, empty is a finite collection.

Now consider a collection having exactly one member, {m}. Any relation (::{m}) is necessarily monic, since there is only one right value that any left value could possibly be related to. Consequently, every non-empty relation (::{m}) is monic (:|{m}). For any non-empty collection A, a mapping (A|:) is necessarily non-empty – as A has some members, each of which is a left value – so {monic (A:|{m})} subsumes {mappings (A|:{m})}. Thus every non-empty collection pigeonholes every singleton collection, all singleton collections pigeonhole one another and every singleton is finite. In particular, as {empty} is a singleton, there does exist at least one finite non-empty set.

Given a finite collection A that subsumes B, consider a mapping (B|f:B); uniting this with the identity on {a in A: a not in B} yields a mapping (A|:A) which is thus a monic (A:|A); and every sub-relation of a monic is monic, hence f is monic. Restricting to B, on either side, simply gives us back f without losing any (right or left) values in B (since it only eliminates the identity we united f with), so we also find that (B:f|B), so {monic (B:|B)} subsumes {mappings (B|:B)}. Thus every sub-collection of a finite collection is finite (and finiteness of empty can be inferred by virtue of it being a sub-collection of any singleton, e.g. {empty}).

Suppose A pigeonholes B which subsumes C. Consider any mapping (A|f:C); as B subsumes C, this is fatuously a mapping (A|f:B) hence, as A pigeonholes B, a monic (A:f|B); and B subsumes C so its restriction (::C) is monic (A:f|C); but its restriction to C is f itself, as f was specified (:f:C). So every mapping (A|f:C) is in fact a monic (A:f|C) and A pigeonholes C. Thus every collection pigeonholes everything subsumed by anything it pigeonholes; pigeonhole subsumes pigeonhole&on;subsume. In particular, a finite collection pigeonholes itself, hence everything it subsumes.

Suppose A subsumes B which pigeonholes C. Consider any mapping (A|f:C);
its (B::) restriction is still a mapping and, as A subsumes B, (B|f:C); thus,
as B pigeonholes C, this restriction is monic (B:f|C). As f is a mapping
(::C), each left value is f(c) for some c in C and there is only one such per
member of C; as each c in C *is* a right value of (B:f|C), hence has
f(c) in B, the restriction (B:f:) was in fact fatuous and (B:f|C) = f is
monic. Since A subsumes B, (A:f:) has every right value that (B:f:) has, so f
is in fact (A:f|C). So every mapping (A|f:C) is in fact monic (A:f|C) and A
pigeonholes C. Thus any collection pigeonholes everything that any of its
sub-collections pigeonholes; pigeonhole subsumes subsume&on;pigeonhole.

Define:

- successor = (: r&unite;{r} ←r :{relations})

In so far as context admits a relation r as a value, we have a
singleton collection {r}, the relation which relates r to r and nothing else;
and we can unite this with r to obtain successor(r), which relates x to y
precisely if either r relates x to y or x and y are both r. (The choice of
name has to do with the rôle this mapping plays in my formulation
of the naturals.) I refer to successor(r)
as the successor of

r. When r is a collection, its successor is
necessarily also a collection, since {r} is.

Given one collection, A, that pigeonholes another collection, B, and any a not in A, b not in B; consider a mapping (A&unite;{a}| f :B&unite;{b}). As a is a left value of f, it is f(i) for some i in B&unite;{b}; if i is b, let s be the identity on B&unite;{b}, otherwise let s be the iso that swaps i and b while acting as the identity on the rest of B; either way, s is self-inverse and iso. Composing before f gives us the mapping (A&unite;{a}| f&on;s :B&unite;{b}) with f(s(b)) = a; its (A::) restriction loses us all right values i with f(s(i)) = a, notably including b, but it's a mapping, so relates nothing else but a to any of these right values; it is thus a mapping (A|f&on;s:B) and, as A pigeonholes B, a monic (A:f&on;s|B). As it is a mapping and (A:|B), f(s(i)) is in fact in A for all i in B, so f&on;s relates a only to b; f&on;s is thus the union of (manifestly) monic ({a}: a←b :{b}) and monic (A:f&on;s|B), with a not in A, hence f&on;s is monic and (A&unite;{a}: f&on;s |B&unite;{b}). As s is self-inverse and iso, f&on;s&on;s = f is thus also monic (A&unite;{a}: f |B&unite;{b}). This being true for any (A&unite;{a}| f :B&unite;{b}), we see that A&unite;{a} pigeonholse B&unite;{b}. Thus adding a single new member to a collection yields one that pigeonholes every result of adding a single new member to any collection the original pigeonholes.

Now, had b been in B, B&unite;{b} would have been simply B; and
A&unite;{a} subsumes A (even if a is in A), which pigeonholes B, so
A&unite;{a} would still have pigeonholed B&unite;{b}. Thus, as long as either
a is not in A or b is in B, A&unite;{a} pigeonholes B&unite;{b}. In
particular, for any finite collection C with C in C

decidable, the
collection C&unite;{C} is also finite (as C pigeonholes C and either C not in C
or C in C meets the foregoing conditions with C as A, B, a and b).

Given collections A, B along with a not in A and b not in B, suppose we
know that A&unite;{a} pigeonholes B&unite;{b}; and consider a mapping
(A|f:B). We can extend it to a mapping (A&unite;{a}| :B&unite;{b}) by uniting
it with ({a}: a←b :{b}), as b is not in B (so this doesn't hurt its being
a mapping); and we know the result doesn't relate a to anything but b (so its
(A::) restriction is simply f). Our given pigeonholing now implies that this
extended mapping is in fact monic (A&unite;{a}: |B&unite;{b}), hence its (A::)
restriction, which is simply f, is monic (A:f|B). Thus A pigeonholes B and we
can cancel

an extra member as readily as we can add one.

The above suffice to let us prove useful things about the naturals, which I shall assume in some later sections. In particular, we are able to establish that ({naturals}: successor |{naturals}) is monic (and, by construction, a mapping) but is not ({naturals}| :{naturals}) since empty = 0 in {naturals} is not a left value of successor; thus {naturals} is infinite (and there does necessarily exist an infinite collection).

Before moving on, it's worth noticing that the existance of an
infinite set actually implies an endless supply of infinite sets, each of
which pigeonholes the previous (but none of them pigeonholes itself). For any
relation r, define P(r) = {relations s: r subsumes s} = ({r}&on;subsume:
s←s :). In classical set theory, when A is a set, P(A) is known as
its **power set**. We can define a mapping

- Cantor = (: (P(A): {a in A: a not in f(a)} ← f :{mappings (P(A)::A)}) ←A :{collections})

for which each Cantor(A, f) is in P(A) and not a left value of f
– each a in A is either in Cantor(A, f) or in f(a) but never in both (by
Cantor(A, f)'s specification) so serves as a witness that Cantor(A, f) is not
f(a). This being true for all mappings (P(A):f:A), we know that {mappings
(P(A)|:A)} is empty, thus subsumed by {monic (P(A):|A)}. So *every*
collection A is pigeonholed by P(A), hence by at least *some*
collection – even if A is infinite.

For any collection B, {mappings (empty|:B)} = {empty}; and empty (though monic) is only (:|B) if B is empty; so empty pigeonholes nothing but itself.

From the definition of pigeonholing, whenever any mapping (A|f:B) is not (A:f|B), even if it is monic, A does not pigeonhole B; in particular, given a mapping (A|f:B) and any b not in B, we can fatuously consider f to be (A:f:B&unite;{b}), ignoring b and retaining all its left values, hence (A|f:B&unite;{b}) but not (A:f|B&unite;{b}), since b is given to not be one of f's right values; so the collection of outputs of a mapping never pigeonholes the result of adding one extra member to the mapping's collection of inputs. In particular, no collection pigeonholes its union with any collection it doesn't subsume, and no collection is pigeonholed by any of its proper sub-collections.

Conversely, whenever one collection A does not pigeonhole some other, B,
the definition says this means there is some mapping (A|:B) which is not monic
(A:|B). If it is not monic, then there is some a in A which it relates to
more than one member of B, each of which it maps only to a; so omitting some
but not all of these right values from B, the restriction is still a mapping
(A|:B) and is not (A:|B). Consequently, whenever A does not pigeonhole B,
there is some mapping (A|:B) which is not (A:|B). In particular, and often
more usefully (as we'll see below), there *does exist* some mapping
(A|:B).

Given a monic, m, the composite reverse(m)&on;m is necessarily just m's collection of right values, for: if it relates x to z, it necessarily does so via some y which m relates to both x and z; but m is monic, so relates any given left value, y, to only one right value; hence x is z. Likewise, for a mapping, f, the composite f&on;reverse(f) is just f's collection of left values. Every iso (i.e. monic mapping) thus has its reverse as inverse, in either order.

An iso between the whole of each of two collections, (C|e|S), induces an iso ({(C::C)}| e&on;r&on;reverse(e) ←r |{(S::S)}) which, in particular, identifies {monic (C:|C)} with {monic (S:|S)} and {mapping (C|:C)} with {mapping (S|:S)}. As a result, each of C and S is finite precisely if the other is; any collection isomorphic to a finite one is also finite.

Suppose A pigeonholes B and we have isomorphisms (A|e|P) and (B|i|Q); consider any mapping (P|f:Q). The composite g = e&on;f&on;reverse(i) is necessarily a mapping and (A|:B), hence monic (A:g|B); and the composite f = reverse(e)&on;g&on;i is likewise monic and (P:|Q). Thus whenever one collection pigeonholes another, every collection iso to the former pigeonholes every collection iso to the latter.

From the above it should be clear, from how it interacts with subsume and
with addition of new elements, that pigeonholing serves as a kind of is
bigger than

comparison. Let's now look at how it relates to another kind
of size

comparison among collections, concerned with when
there *exist* (|:) mappings. A mapping (A|:B) is described as
a **surjection** to A, so we can think of this as a surjection
ordering of collections.

We can define a partial order on collections by: C ≥ S precisely if
there exists some mapping (S|:C). This is reflexive (C≥C for all C thanks
to the (C|:C) identity) and transitive (because a composite (S|:K)&on;(K|:C)
of mappings is an (S|:C) mapping). We can thus intersect it with its reverse
to obtain an equivalence, known as **cardinality**. Note, in
contrast, that pigeonholing is *not* reflexive (infinite collections
don't pigeonhole themselves), hence not a partial order. As negation of ≥,
define C < S precisely if there exists no mapping (S|:C); and let ≤
stand for the reverse of ≥, with > being the reverse of <. When one
collection, A, does not pigeonhole another, B, we have already seen that this
implies B≥A.

One may reasonably suppose that every mapping (S|f:C)
between collections subsumes some iso (S||N) for which C subsumes N, so that
finiteness of C shall imply finiteness of S and, conversely, infiniteness of S
shall imply infiniteness of C; and likewise, on reversing the monic, for
mappings; however, to prove that, we need the axiom of choice. For the case
where C is given to be finite, we only need finite choice, which we shall
infer below; but the infinite case requires the transfinite axiom of
choice. (I entertain the possibility that there may exist a mapping (N|f:S)
and some property Q that S's members may posses, that is commonly undecidable
for particular members of S, yet for which there is some way to prove that,
for each n in N, f *does* relate n to some member of S having property
Q; in such a case, showing that f's restriction (N|f:{s in S: Q(s)}) subsumes
some iso seems likely to be difficult.) So, while it is sensible to
understand cardinal equality of collections S and C as corresponding to the
existence of an iso (S||C), I merely define it to mean that there exist
mappings (S|:C) and (C|:S); I allow the possibility that isomorphism is a
proper sub-equivalence of cardinality.

Indeed, I see no obvious way to even prove that ≥'s union with its
reverse relates all collections to one another; i.e. that, for any collections S
and C, we necessarily know either S≥C or C≥S

, i.e. there
necessarily is at least one mapping either (S|:C) or (C|:S). Without that, ≥
isn't a full order; we can't even infer S≥C from S>C; but it does at least
give me a nice short-hand way to say whether there exist mappings (|:) between
collections.

When a collection, C, subsumes another, S, the latter – construed as an identity – is a mapping (S|:C), hence C ≥ S, so ≥ subsumes subsume; in particular, ≥ coincides with the usual ordering on the naturals (each of which subsumes each of its members).

Suppose we have collections A, B with A > B; i.e. there are no mappings
(A|:B). Fatuously, A pigeonholes B; every collection, including {monic
(A:|B)}, subsumes empty = {mappings (A|:B)}. For any b not in B, consider a
mapping (A|f:B&unite;{b}). Define a mapping ({iso (B&unite;{b}|
|B&unite;{b})}: t |B&unite;{b}) by: t(b) is the identity on B&unite;{b}; for
each i in B, t(i) swaps i and b while acting as the identity on all other
members of B. For each i in B&unite;{b}, we thus have a mapping (A| f&on;t(i)
:B&unite;{b}); and there are no mappings (A|:B), so some member of A is not a
left value of (A: f&on;t(i) :B). The restriction (A::) is fatuous, given f's
introduction as an (A|:) mapping, and the only omission caused by (::B) is to
eliminate b as a right value, along with any left values related to it; as
f&on;t(i) is a mapping, it relates at most one left value to b; and as
(:f&on;t(i):B) does in fact omit some of A, there must be some such left
value, namely f(t(i,b)) = f(i), hence i *is* a right value of
f. Furthermore, for f(i) to be missing from (:f&on;t(i):B)'s left values,
there must be no member of B that f&on;t(i) relates it to, hence i is
the *only* right value to which f relates f(i). Consequently, f is in
fact monic (A:f|B&unite;{b}) and A pigeonholes B&unite;{b}. So A>B implies
that A not only pigeonholes B but pigeonholes the result of adding at least
one member to it.

Conversely, suppose A pigeonholes B&unite;{b} for some b not in B. Thus
every mapping (A|f:B&unite;{b}) is in fact monic (A:f|B&unite;{b})
and *does* have b as a right value. Every mapping (A::B) can fatuously
be construed as one (A::B&unite;{b}); but one of these can only be (A|:) if it
in fact has b as a right value, hence it's not (A::B), so there are no mappings
(A|:B); thus A>B. Thus A pigeonholes B&unite;{b}, for any b not in B,
precisely if A>B; and A≤B precisely if A does not pigeonhole any
B&unite;{b} with b not in B.

Now suppose we are given collections A, B with A≥B, i.e. {mappings (B|:A)} is non-empty; and suppose B pigeonholes some collection C which subsumes A (whence B pigeonholes A). So consider a mapping (A|f:C); we can compose it with any mapping (B|g:A) to obtain a mapping (B|g&on;f:C) which must be monic (B:g&on;f|C) since B pigeonholes C; thus every member of C is a right value of f, so (A:f|C). Now suppose f relates some a in A to both c and z in C; each mapping (B|g:A) gives g(f(c)) = g(a) = g(f(z)) if a is a right value of g; as g&on;f is monic, this makes c and z equal; thus (g:f:) is monic. But (:g&on;f|C) implies (g:f|C); and f is a mapping, so every c in C has f(c) a right value of g so (g:f:) = f. Thus f is in fact monic (A:f|C) and A pigeonholes C which subsumes A. No collection pigeonholes any that strictly subsumes it, so this implies C = A. Thus A≥B implies that A is the only collection, that subsumes A, that B even might pigeonhole.

Conversely, given a collection A, if a collection B does not pigeonhole any collection, except possibly A, that subsumes A, then (in particular) B does not pigeonhole any A&unite;{a} with a not in A, so we can infer A≥B. Thus A≥B precisely if B does not pigeonhole any collection, except possibly A, that subsumes A.

Suppose one collection, B, does not pigeonhole another, A (hence we know A≥B). Since every collection pigeonholes empty, this tells us A is non-empty, hence A = {a}&unite;C for some a not in C. Every collection which subsumes C, aside from C itself, subsumes {c}&unite;C for some c not in C; and this is trivially iso to A, so B does not pigeonhole it, hence nor does B pigeonhole anything that subsumes it. Thus B pigeonholes no collection that subsumes C, except possibly C; hence C≥B and there exists a mapping (B|g:C). Now consider any mapping (A|f:B); we can compose it with g to get a mapping (A|f&on;g:C); and A subsumes C, so this is (A|f&on;g:A) but is not monic (A:|A), as a is not one of its right values; so either there is no mapping (A|f:B), i.e. A>B, or A is infinite.

Conversely, for any finite collection A, every collection either pigeonholes A or is <A. In the latter case, it is also ≤A (as it was ≤C, which A subsumes) and A pigeonholes it (and even the result of adding another member to it, since A> it). For a pair of collections, we thus have these possibilities:

- At least one of them is infinite,
- Each pigeonholes the other, or
- One pigeonholes the other, which is both < and ≤ the first.

We now have what we need to formalise counting,
the process by which we associate each finite set with a natural number that
has the same number of members

.