[FOM] Adventures in Formalization 6

[Freek Wiedijk]

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