[FOM] FOM Digest, Vol 154, Issue 15

[Paul Blain Levy]

Dear Freek,

If your seven Mizar definitions were the only occasions when 
mathematicians want to embed a set inside another set, I suppose the 
awkwardness wouldn't matter.  But we encounter this situation again and 
again, e.g. embedding an arbitrary ring R inside the polynomial ring 
R[x], or an integral domain inside its field of fractions.  In each of 
these cases the embedding is often elided in informal discourse.  Are 
you saying that, in all such situations, the definer should contrive to 
make the bigger set disjoint from the original (smaller) one?

Another point: if, as you seem to be saying, you aim is merely to export 
abstract data types of natural numbers, integers, etc. to your users, 
what is wrong with defining an integer to be an equivalence class and 
then defining the natural numbers to be a subset of the integers?  These 
natural numbers, which you export, will not be the ones you used to 
implement integers, but the latter are unknown to your users so the 
discrepancy won't matter.

Paul


> Date: Thu, 15 Oct 2015 12:27:55 +0200
> From: Freek Wiedijk <freek at cs.ru.nl>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] Adventures in Formalization 6
> Message-ID: <20151015102755.GA23671 at wheezy.localdomain>
> Content-Type: text/plain; charset=us-ascii
> 
> Dear Paul,
> 
>> It must be stressed that this relies on int' - i[nat] being disjoint
>> from nat, which depends on the particular implementation of int' and
>> nat.  Evidently an equivalence class of Kuratowski pairs of von
>> Neumann naturals can't also be a von Neumann natural, as the former
>> is infinite and the latter finite, but it's hardly appealing to have
>> to rely on such "accidents".
> 
> Yes.  In the Mizar library I think that the rationals and
> the complex numbers are represented by two different kinds
> of pairs: one is Kuratowski pairs, the other sequences
> of two elements (which are implemented by functions from
> {0,1} _consisting_ of Kuratowski pairs, because functions
> are sets of Kuratowski pairs.)  And so the theorem had to
> proved that these are never are the same ZF set.
> 
> The definitions of some of the number sets are actually
> quite short.  I hope the FOM moderators will allow me to
> quote them here:
> 
>   func INT -> set equals
>     NAT \/ [:{0},NAT:] \ {[0,0]};
>   func RAT+ -> set equals
>     ({[i,j]: i,j are_coprime & j <> {}} \ the set of all [k,1]) \/ NAT;
>   func RAT -> set equals
>     RAT+ \/ [:{0},RAT+:] \ {[0,0]};
>   func DEDEKIND_CUTS -> Subset-Family of RAT+ equals
>     {A where A is Subset of RAT+ : r in A implies
>                    (for s st s <=' r holds s in A) & ex s st s in A & r 
> < s}
>       \ {RAT+};
>   func REAL+ -> set equals
>     RAT+ \/ DEDEKIND_CUTS \ {{s : s < t} : t <> {}};
>   func REAL -> set equals
>     REAL+ \/ [:{0},REAL+:] \ {[0,0]};
>   func COMPLEX -> set equals
>     Funcs({0,1},REAL) \ {x where x is Element of Funcs({0,1},REAL): x.1 
> = 0}
>       \/ REAL;
> 
> On the other hand, when _using_ these numbers the
> objection that they only fit together well because of
> "accidents" is completely irrelevant, because they're
> really used as "abstract data types".  Quoted from
> <https://en.wikipedia.org/wiki/Abstract_data_type>:
> "The user does not need any technical knowledge of how
> the implementation works to use the ADT.  In this way, the
> implementation may be complex but will be encapsulated in
> a simple interface when it is actually used."
> 
> Freek