[FOM] Adventures in Formalization 6 (reply to Paul Levy)

[Mario Carneiro]

Hi Paul,

On Fri, Oct 16, 2015 at 4:23 PM, Paul Blain Levy <P.B.Levy at cs.bham.ac.uk>
wrote:

> 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?
>

There is a general method for constructing such "disjointified sets".
Suppose sets A and B are given, and we want to construct a set isomorphic
to B and disjoint from A. If "ran A" is the set {y | exists x: <x,y> in A}
(also known as the range of A, which makes sense even if A is not a
relation), and f(A) is any mapping satisfying f(A) not in A (a simple
choice for this is f(A) = pow(union A), since if pow(union A) in A then
pow(union A) c= union A, contradicting Cantor's theorem), then we can
choose B' = B x {f(ran A)}. There is an obvious isomorphism from B to B'
sending x to <x,f(ran A)>, and given any y in B', it is of the form
<x,f(ran A)>, so if y is in A as well we have f(ran A) in ran A, a
contradiction.

It is easy to use this construction so that given a set A and an extension
B of A with a given injection f:A->B, we can output a modified version B'
of the extension and a bijection g:B->B' such that A is a subset of B' and
g(f(x)) = x (so that the mapped version of the original injection is the
identity function). This procedure can be carried out in any set theory
strong enough to produce ordered pairs and cartesian products.


> 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.
>

In the specific case of the construction of the reals, the reason this is a
problem is because both the original and new sets have their uses within
larger constructions: obviously the integers/reals just constructed are
needed, but the original natural number set also appears as a subset of the
ordinals. Thus there will be two copies of the natural numbers if the
"discrepancy" is not addressed by modifying the construction appropriately.
If this is considered an undesirable feature, one would have to extend the
abstract data type to include the specification that the canonical
injection from the natural numbers to the integers is in fact the identity,
and adjust the construction to satisfy this constraint.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151018/b6fb372d/attachment.html>