Counting indirectly - dependent ordered pairs

Suppose you want to determine the number of pairs of persons (from a given group) where the second person must be younger than the first? Or suppose you want to count the number of ordered pairs from this group where the person in the second position must simply be someone other than the one in the first. (There's nothing physical intended about these "positions". Maybe there's only one cupcake and one cookie left, and you want to count the number of ways to dole them out.
Then we may stipulate that the first "position" is getting the cookie, and the second is getting the cake.)

This way of limiting a class of pair constructions is denoted "x:AB(x)".

<a,b>  x:AB(x) just when a  A and b  B(a).

The "x" of "x:AB(x)" is a binding variable that binds in "B(x)", just like the quantifier notations "x:A. B(x)" and "x:A. B(x)".
The position of the B(x) in x:AB(x) should be occupied by an expression that stands for a class, no matter what expression of type A is put for x. The collection from which the second component b is chosen may DEPEND on the VALUE of the first component a. Examples:

*	(x:G{y:G| age(y)<age(x) }) is the collection of age-restricted pairs of persons described above where G is the collection of relevant persons.
*	(x:G{y:G| x = y }) is the collection of no-duplicate pairs of persons described above.
*	(x:Gy:G{z:G| x = y & y = z & z = x }) is the collection of no-duplicate triples, construing triples as nested pairs. (ala Counting Tuples)
*	(i:i) is the collection of pairs of natural numbers where the second is less than the first. There is no <0,k>  i:i since 0 is empty.

The standard notation for this operation on classes is "x:A. B(x)". The similarity to the standard notation for summing a numeric function over a range of values, such as " i:{k..m}. f(i)" , is again no accident. Here the two concepts are related:

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

The numeric sum notation " i:k. f(i)" is just an abbreviation for " i:{0..k}. f(i)".
The notational similarity could be either confusing or helpful. The two notations could not logically be used in the same contexts since they take different kind of arguments and have different kinds of values:

The value of a numeric summation expression " i:{a..b}. f(i)" is numeric, and the functional argument f(i) is numeric.

The value of a dependent-pair type expression "x:AB(x)" is a class whose members are pairs, and the functional argument B(x) stands for a family of classes, one for each member of class A.

The priniciple above very nearly tells us that if we assign to each member of a finite class, another finite class, then we can count the pairs of the dependent-pair-type by simply adding up the sizes of all the classes in the family of classes.

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