Counting Indirectly - ordered pairs

For example, one can determine how many squares are on a chessboard by knowing that each square can be uniquely identified by a rank and a file, and that every rank of every file has a square. The modern convention for naming squares is to give a pair consisting of a letter from "a" to "h" and a number from 1 to 8. So, there is a one-one correspondence between squares and pairs <x,y>  AH{1...8}, if AH is the class of letters from"a" to "h". There are, of course, 64 squares, but let's proceed to probe the math.

Generally the "Cartesian product" AB is the class of pairs <x,y> such that x  A and y  B, and for finite A and B, the size of AB is the product of the sizes of A and B, or to be precise,

Thm*  a,b:. (A ~ a)  (B ~ b)  ((AB) ~ (ab))

It is no accident that the conventional notation "AB" for the Cartesion product of two classes resembles a standard notation for multiplication of numbers. This will happen with some other notations as well.

We can convey this relation between Cartesian product and numeric product more succinctly by resorting to our standard finite classes:

Thm*  a,b:. (ab) ~ (ab)

This is typical of how we shall express our core counting principles, and it is possible in this case because of the fact that

Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B'))

i.e., the product classes are in one-one correspondence if the respective component classes are, which means we can perform rewriting of class expressions preserving size.

To resume our chessboard problem, just as we shall not try to formally make the connection between chessboard structure, and the rank file pairs, leaving this claim only informally assumed, so we shall not here formalize the class of letters "a" to "h", and we shall assume that AH has 8 members, i.e., AH ~ 8.

So, we have informally "reduced" the problem of how many squares a chessboard has to how many members AH{1...8} has for arbitrary AH ~ 8.

The priniciples used in the proof that follows are these:

Thm*  a,b:. {a...b} ~ (1+b-a)
Thm*  a,b:. (ab) ~ (ab)
Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B'))
Thm*  (A ~ A')  (B ~ B')  ((A ~ B)  (A' ~ B'))
Thm*  A ~ A

These equivalences have been applied and assembled into a proof of

Thm*  (AH ~ 8)  ((AH{1...8}) ~ 64)

Please read it along with the Remark for this proof.

Here we have considered how to count pairs selected independently from two classes. This leads us to consider Counting Tuples and Counting Dependent Pairs, where the second element is drawn from a class selected by the choice of the first element.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html