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