Nuprl - Introduction to Counting

Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMathNuprl Section: DiscreteMath - Discrete Math Lessons Counting is finding a function of a certain kind.
When we count a class of objects, we generate an enumeration of them, which we may represent by a One-to-One Correspondence from a standard class having that many objects to the class being counted. Our standard class of n objects, for n

, will be

n, which is the class {k:

| 0

k < n } of natural numbers less than n. A more familiar choice of standard finite classes might have been {k:

| 1

n }, but there is also another tradition in math for using {k:

| 0

k < n }.

So, a class A has n members just when

f:(nA). Bij(n; A; f)

which may also be expressed as

(n ~ A)

since Thm* (f:(AB). Bij(A; B; f)) (A ~ B), or as

(A ~ n) since Thm* (A ~ B) (B ~ A).

Now, since counting means coming up with an enumeration, we may ask whether counting in different ways, i.e., coming up with different orders, will always result in the same number, as we assume. Of course, we know this is so, but there are different degrees of knowing. It is not necessary to simply accept this as an axiom; there is enough structure to the problem to make a non-trivial proof.

Thm* (A ~ m) (A ~ k) m = k
Gloss

This theorem is closely related to what is sometimes called the "pigeon-hole principle", which states the mathematical content of the fact that if you put some number objects into fewer pigeon-holes, then there must be at least two objects going into the same pigeon-hole. Number the pigeon-holes with the members of k, and the objects with the members of m; then a way of putting the objects into the holes is a function in mk: