Counting Indirectly - tuples

This can only happen if the classes from which the first and second components are drawn overlap. That couldn't happen for the modern chessboard notation of Counting Ordered Pairs because letters fill the first place and numbers fill the second. But of course that was not necessary -- the designers of the chess notation could have decided to use numbers from {1...8} instead of letters, and simply required that the first number indicates the file and the second the rank; that would be harder to read though, and people might have trouble remembering the order of rank and file.
So (<1,2> = <2,1>), and <2,2>  .

We won't go into it here, but to emphasize the distinction, and to portend subtle issues of how to distinguish objects to be counted, consider a buffet that, for a fixed price, allows you to have two servings of a topping on rice, your choice. While you might order chicken before you order tofu, or tofu before chicken, these would normally be understood as two ways to order the same meal.
The order you place might be considered an ordered pair of toppings, but the meal you choose would not. So our methods so far tell us how many ways we may place an order, but not how many meals we have to choose from. (My experience in these businesses is that you are permitted to have two of the same topping, so you cannot just say there are two ways of specifying each meal.)

Back to ordered pairs. Suppose we want to consider ordered triples. Do we need to redevelop the machinery for counting pairs from the start, and then again for 4-tuples, etc? Well, we certainly could add triples to our precise mathematical language. If we were to add triples we would soon start trying to adapt our facts about pairs by recognizing that you can "think" of a triple (x,y,z) as a pair <x,<y,z>>, whose first component is the first of the triple, but whose second component is itself a pair <y,z>, built of the second and third components of the triple. Not only can you "think" of triples that way, but you could define a bijection between A(BC) and the corresponding "triple-product". Naturally, once you do this you're ready to iterate the method to 4-tuples and so forth.

In fact, using the iterated pairs to simulate tuples has proven to be so convenient and simple that it is normal for mathematical systems to stop at the pairs and binary products and consider the higher tuples as informal concepts, or perhaps as themselves being "defined" as iterated pairs. We will do this, too.

<x,y,z> is just a suggestive notational abbreviation for <x,<y,z>>
<u,x,y,z> is just a suggestive notational abbreviation for <u,<x,<y,z>>>
etc.

ABC is just a suggestive notational abbreviation for A(BC)
ABCD is just a suggestive notational abbreviation for A(B(CD))
etc.

We could have done something similar instead, such as grouping the tuple components through the other position, i.e., letting <<x,y>,z> be our encoding of the triple (x,y,z), but these pairs are different objects and so we ought to stick to a convention.

Indeed, the obvious conversion between left-nested and right-nested triples is exploited to prove this theorem: Thm*  (ABC) ~ ((AB)C) Remark

Amusingly, by combining this purely structural fact with

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

one can show Thm*  a,b,c:. a(bc) = (ab)c .

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