Counting Indirectly - integer ranges.

k  

B ~ k

A ~ k

Thm*  (A ~ B)  (B ~ C)  (A ~ C)

Thus developing the skill of counting abstractly specified classes depends partly on developing a few basic forms that one knows how to count, and partly on developing the skill of "translating" new descriptions of classes into these forms one already knows how to count.

If you take a finite range of consecutive integers and add the same number to them all then you get a new collection with the same size as the old one.We will normally indicate such consecutive integer collections either with

Def  {i...j} == {k:| ik & kj }

or

Def  {i..j} == {k:| i  k < j }.

The notation {i..j}, which mentions the least member and the number after the largest member, turns out often to be more convenient to use than the more natural notation {i...j} which mentions both ends. (With both notations there are infinitely many ways of specifying the empty class, by picking ends in the "wrong" order, e.g., {4...3}, {1...-2}, {0..0}, or {0..(-3)}.)

We shall also adopt {0..k} as our "standard" finite class having k members, rather than the more every-day counting set {1...k}.
We tend to use this standard when precisely expressing facts about class size.
We shall abbreviate {0..k} as k, connoting "the first k members of ".

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

(corrolary of Thm*  (A ~ m)  (A ~ k)  m = k)

Here are some theorems about the sizes of these finite integer ranges.

Thm*  a,b:. {a..b} ~ (b-a)

Thm*  a,b:. {a...b} ~ (1+b-a)

Underlying these theorems is a lemma

Thm*  a,b,a',b':. b-a = b'-a'  ({a..b} ~ {a'..b'})

which is proved by explicitly giving the functions that map back and forth between {a..b} and {a'..b'}.
Recall that

Def  InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)

and that one way to give a one-one correspondence is to provide such a pair of inverse functions. The proof of {a..b} ~ {a'..b'} specifies

(x.x+a'-a)  {a..b}{a'..b'}
and
(x.x+a-a')  {a'..b'}{a..b}

then shows these functions to be inverses by simply computing

(x.x+a-a')((x.x+a'-a)(x)) down to x+a'-a+a-a', which is obviously equal to x, and

(x.x+a'-a)((x.x+a-a')(y)) down to y+a-a'+a'-a, which is obviously equal to y.

Another fundamental method is to reduce a counting problem to Counting Ordered Pairs.

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