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
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 (
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>>>
ABCis just a suggestive notational abbreviation for A(BC) ABCDis just a suggestive notational abbreviation for A(B(CD))
We could have done something similar instead, such as grouping the tuple components through the other position, i.e., letting
Indeed, the obvious conversion between left-nested and right-nested triples is exploited to prove this theorem:
Amusingly, by combining this purely structural fact with
Thm* a,b:. (ab) ~ (ab)
Thm* a,b:. (a ~ b) a = b
one can show