From lusk Fri Jun 17 14:35:16 1994
Received: from scapa.cs.ualberta.ca (scapa.cs.ualberta.ca [129.128.4.44]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id OAA22109 for <qed@mcs.anl.gov>; Fri, 17 Jun 1994 14:34:43 -0500
Received: from tees.cs.ualberta.ca by scapa.cs.ualberta.ca id <18491-2>; Fri, 17 Jun 1994 13:34:31 -0600
Subject: Examples
From: Andrzej Trybulec <andr@cs.ualberta.ca>
To: qed@mcs.anl.gov
Date: 	Fri, 17 Jun 1994 13:34:20 -0600
Cc: andr@cs.ualberta.ca (Andrzej Trybulec)
X-Mailer: ELM [version 2.4 PL23]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 2557      
Message-Id: <94Jun17.133431-0600.18491-2@scapa.cs.ualberta.ca>

Hi:

To continue the discussion on the examples for QED I would like to suggest
the Stone's theorem that every metrizable space is paracompact, 1948.

It is a bit of substantial methematics, and simultaneously sufficiently
simple to be a standard example.

This is somehow related to Ken Kunen and John Harrison discussion.
The proof that I remeber uses transfinite induction on ordinals but
the proof actually done in Mizar uses only well ordered sets.

I will try to formulate it in such a way that it fits the little theories 
approach (how I understand them).

1. We can use metric spaces instead of metrizable ones.

2. To say what is a metric space is we need a little theory of real
   numbers (elementary theory of real numbers will do).
   The first sort of objects that we need are Reals.

3. To get rid of the concept of metric space, let us treat it as
   a metathoretic locution. We need only new sort of objects: Points
   and the concept of distance between points that satisfies well
   known conditions:
     dist(x,x) >= 0
     dist(x,y) = 0 iff x = y
     dist(x,y) = dist(y,x)
     dist(x,y) + dist(y,z) >= dist(x,z)

4. The next sort of objects that we need are Subsets (of the metric
   space). We need a little theory of Subsets (I guess on the level
   of Boolean algebra). And two specific contructs:
   - an open ball (with the center x being a Point and the radius
     r being a Real)
      Ball(x,r) = { y, y being a Point: dist(x,y) < r }
   - on open Subset :
     X is open iff for every x in X there exist r > 0 such that
      Ball(x,r) is included in X

5. We need also Families of Subsets of our metric space. We may use
   a little theory of families of sets that must include two concepts

   F is a cover ( for every Point x there exists a Subset X
                  such that x belongs to X and X belongs to F)
   F is finer than G
                ( for every Subset X that belongs to F there exists
                   Subset Y that belongs to G and is included in Y)

   Now we are in a position to say what we want to prove:

   For every Family that is a cover and consists of open Subsets
 there exists a Family that is finer, still a cover and also
 consists of open Subsets and is locally finite.
 
 Locally finite means that for every point x there is a positive
 Real r such that Ball(x,r) has non empty intersection with
 only finite number of elements of the Family.
 
6. Hence we need a little theory of finiteness. 


I would like to see a proof of this theorem in some other system.


Andrzej Trybulec