Re: Ordered pairs

[Andrzej Trybulec <trybulec@wwwserve.cs.shinshu-u.ac.jp>]

William Faris wrote:
> 
...
> 
> One reason might be that it generalizes in a natural
> way to ordered triples, etc. For instance, one could have
> 
>            [x, y, z] = { {x,y,z}, { x,y }, { x } }.
> 

I like the argument, unfortunately it does not work:

     [x, y, y] = {{x,y,y},{x,y},{x}} .= {{x,y},{x}}
     [x, y, x] = {{x,y,x},{x,y},{x}} .= {{x,y},{x}}

The definition may be used if all elements are different. Let us put
indices, to distinguish them. I.e. instead of x,y,z we use
 [x,1], [y,2], [z,3]. Then it works, but then
      { [x,1], [y,2], [z,3] }
is quite good triple  (in Mizar notation it is <*x,y,z*>, a finite
sequence)).

I believe that we should use finite sequence rather than triples defined
as [[x,y],z]. Even <*x,y*> instead of [x,y]. Still we need Kuratowski's
definition to start. With one reservation: finite sequences should start
with 0, not with 1. So I would use "finite T-sequence" instead
(finite transfinite sequences :-).

I intend to propose the following revision of MML:

- to restrict the use of [x,y] when it is absolutely necessary
  (the definition of binary relations and unary functions)
  even the binary Cartesian product will be defined as
    product <*A,B*> 
  i.e. { <*a,b*> : a in A & b in B }
  and not { [a,b] : a in A & b in B }

- to remove from MML definitions (mostly Cartesian product of various
  structures) that then will become special cases of (usually  
introduced later, but quite often in the same article) the general    
Cartesian products.

Andrzej Trybulec