Classical set theory defines 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).
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.
A proof that a collection C is finite generally takes the form of showing that every mapping (C|:C) is necessarily also a monic (C:|C), or the converse of this – but I'll start with two easy examples that simply exhibit the two sets involved so as to prove them equal (then I'll prove a general result that'll make the first of these a consequence of the second). These simple results should be considered more as sanity checks of the definition: if empty and singleton sets don't qualify, the definition is wrong !
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 both 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 and any B that it subsumes, every mapping (A|:B) is a mapping (A|:A), as A subsumes B, hence given to be a monic (A:|A), hence a monic (A:|B), again because A subsumes B; thus {monic (A:|B)} subsumes {mappings (A|:B)}. So every finite collection pigeonholes each of its sub-collections.
Given, again, 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}).
For any finite collection m, consider the collection C = m&unite;{m}. If m is in m, this is just m itself, hence given to be finite. Otherwise, m is not in m: so consider any monic (C:r|C). It has m as a right value, so it relates some i in m to m; and it does not relate that i to any other value. When i is m, let s be the identity on C; otherwise, let s be the mapping that swaps i and m and acts on the rest of C as identity. In each case, we have a self-inverse monic mapping (C|s|C), a.k.a. a permutation of C, and its composite after r is necessarily monic (C:s&on;r|C). It relates m to m and is monic, so it relates m to nothing else, so restricting to its other left values loses us no right value other than m (it's yet not guaranteed to lose us m, for that matter); so (m:s&on;r:m) does in fact have every member of m as a right value, so is (m:s&on;r|m); and it's a sub-relation of a monic, s&on;r, so it's also monic. Since m is given to be finite, this implies that we actually have a mapping (m|s&on;r:m), so every member of m is in fact a left value of (:s&on;r:m), which is monic, hence s&on;r relates no member of m to m itself (or anything else that's not a member of m). Thus, when we restricted (m:s&on;r:m), all we lost was in fact m←m, which is a mapping and disjoint from the mapping (m|s&on;r:m), so their union s&on;r is a mapping and has m (from m←m) as well as every member of m among its right values, hence is a mapping (C|s&on;r:C). Now (C|s|C) is self-inverse and a mapping, so composing it after s&on;r makes r = (C|s&on;s&on;r:C) a mapping (C|r:C). We thus infer that the union of a finite set m with the singleton {m} is necessarily finite.
The above suffices to let us prove useful things about the naturals, which I shall assume in the next section. In particular, we are able to establish that successor = ({naturals}: {i}&unite;i ←i |{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.
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 function, 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 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.
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
); when collections are
considered modulo this equivalence, our partial order becomes a strict
order.
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. 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.
Given the natural numbers, one can use the partial order above to define a mapping on collections by:
Since each natural is subsumed by all later ones, the partial order above agrees with the natural ordering of the natural numbers, with the result that, for any collection C and natural n in the union that yields count(C), all of n's members are also in the union (but irrelevant since their union with n is still n); consequently, whenever count(C) is finite it is in fact the maximal natural ≤ C.
Suppose we are given a natural n for which: i in n implies that every mapping (C|:i), with C a collection, subsumes some iso (C||I); consider a mapping (C|f:n) for some collection C. Given (C|f:), each c in C has non-empty ({c}&on;f:i←i:) = {i in n: f(i) = c}, so let S = {c in C: ({c}&on;f:i←i:) is a singleton}; this is C precisely if f is monic. Let N be {i in n: i not in (S&on;f:i←i:)}; each i in N is either not a right value of f or not the only right value that f maps to f(i). If N is empty, then f is monic and (:f|n) hence iso (C|f|n); otherwise, as n subsumes non-empty N, n is a non-empty natural, hence 1+m for some natural m. Let i be the intersection of N's members, i.e. its least member; this is necessarily in N; consequently, it is redundant as an input to f. If i is m, let s be the identity on n; otherwise, let s be the mapping which swaps i and m while acting as the identity on all other members of n; in each case, (n|s|n) is self-inverse (and, in particular, iso). Now consider (C:f&on;s:m); if i was not a right value of f, this is equal to (C|f&on;s:n) because restricting (::m) only eliminated m which was not a right value of f&on;s anyway; otherwise there is some other j in n with f(j) = f(i), thus (as s is self-inverse) f&on;s relates f(i) to s(j) in m so f(s(m)) = f(i) is a left value of (:f&on;s:m); so every left value of (C|f&on;s:n) is in fact a left value of (C|f&on;s:m). As m is in n and (C|f&on;s:m) is a mapping, our initial hypothesis tells us it subsumes some iso (C|g|I); thus f = f&on;s&on;s subsumes (:f&on;s:m)&on;s which subsumes g&on;s; as g is iso and s is self-inverse, f thus subsumes (C|g&on;s|{s(i): i in I}). Thus, in each case, every mapping (C|f:n) subsumes some iso (C||I), which is exactly the property each of n's members needed to make it true for n. By strong induction we thus infer that every mapping (C|f:n), with n natural and C a collection, subsumes some iso (C||I); as n is finite and necessarily subsumes I, existence of this iso implies that C is finite. Consequently, every collection C which is ≤ any natural n is necessarily finite. Furthermore every natural ≤ C is then also ≤ n so n subsumes count(C), which is duly finite, hence count(C) is the maximal natural ≤ C.
Consider, now, a collection C ≤ {naturals} which is not ≥ {naturals}; there exists some mapping (C|:{naturals}) and there are no mappings ({naturals}|:C), hence no monics (C:|{naturals}). Given a mapping (C|f:{naturals}), consider the naturals n for which C≥n; for each such, there is a mapping (n|g(n):C) which we can compose after f to obtain a mapping (n|g(n)&on;f:{naturals}). Define a mapping ({naturals}:h:{naturals n: C≥1+n}) with f&on;h monic as follows: (:h|0) fatuously has (:f&on;h:0) monic; given (:h|n) with C ≥ 1+n and (:f&on;h:n) monic, (1+n|g(1+n)&on;f:{naturals}) has 1+n left values, while (:g(1+n)&on;f&on;h:n) is a mapping with n right values (inputs) so at most n left values (outputs); there must thus be at least one left value i of the former that isn't a left value of the latter. So let h(n) be the intersection of those right values of (1+n:g(1+n)&on;f:) that aren't left values of (:h:n); there must be some such right values, for g(1+n)&on;f to map to i; all such right values are naturals, so their intersection is the least of them; in particular it is one of them. As f(h(n)) is a right value of g(1+n), it is distinct from any g(h(i)), with i in n, that's not a right value of g(1+n); and g(1+n) maps f(h(n)) to a different output than any f(h(i)) that is a right value of g(1+n); hence f(h(n)) is distinct from the f(h(i)) with i in n, so (:f&on;h:1+n) is monic. So long as C ≥ 1+(h:i←i:), we can continue this process, growing h while keeping (C:f&on;h:{naturals}) monic. As there is no monic (C:|{naturals}), this process must terminate at some point; when it does, (h:i←i:) must be a natural n for which C≥n but C is not ≥ 1+n. Thus the set of naturals ≤C is finite and count(C) is the largest of them.
Written by Eddy.