FOM: ordered pair: Bourbaki

[Kanovei]

From: Vedasystem at aol.com
Date: Sun, 2 May 1999 19:18:32 EDT

***
 The Bourbaki's approach to introducing notation
for ordered pair is preferable because one cannot prove
silly theorems like (x,y) U {x} =  (x,y).
The Bourbaki's approach is related to abstract data types --
the most fundamental concept on which the modern programming
languages like Java, C++, Eiffel are based.
***

Could you please explain how the rotten set theoretic 
pair definition <x,y>={{x},{x,y}}, possibly even with 
silly theorems like your favourite one above, 
can make any harm to *the modern programming
languages like Java, C++, Eiffel* ? 

The point is that the definition <x,y>={{x},{x,y}} 
was given not in order to irritate someone with 
something like (x,y) U {x} =  (x,y), and far not 
to please or displease any Java programmist: in reality 
the goal was to reduce the set theoretic foundations 
to real primitives, however fully satisfactory to 
ground the whole of mathematics, which exactly has 
been achieved. 

After this has been established, anything like 
ZFC + (Bourbaki's pair) + (natural numbers as primitives) + ... 
can be used, if convenient, as soon as it remains 
a conservative extension of ZFC. Since the conservativity 
is trivial here, hardly there is any foundational issue 
in the "paired" ZFC vs the "pairless" one. 

V.Kanovei