[FOM] continuing problems with constructive continuity?
giovanni sambin
sambin at math.unipd.it
Tue Feb 12 04:43:26 EST 2008
Dear Frank Waaldijk,
I thank you for raising your problems. Unfortunately, I have no time
now to read your and Erik Palmgren's papers carefully to be able to
tell my opinion. I plan to do it as soon as I finish a book I am
writing (on the generalization of formal topology, which I call the
basic picture). Here I would like to call to your attention some of
the principles of formal topology, which seem to be closer to your
attitude than you seem to suspect.
The foundational system on which formal topology is based since its
beginning is very weak. Milly Maietti and I have recently been able
to formalize it properly, and are still working on it. We call it a
minimalist foundation, since
i. it allows to work as usual in mathematics (i.e. extensionally) and
still always know that you can have a computational interpretation
(i.e. formalization in a programming language), and
ii. all proposed foundations (CLASS, INT, RUSS, BISH, Martin-Loef's
type theory, Aczel's CZF,...) can be obtained by adding some kind of
assumptions. Very roughly speaking, it has an effective notion of set
(as in Martin-Loef's type theory), but also an ideal notion of
collection. Consistency of the two is due to the fact that they live
at two different levels of abstraction.
The minimalist foundation aims to providing a formal system i. can
be the common ground on which one can discuss with rigour all
foundational problems (and I suspect that the solution to your
specific problem is not purely mathematical and will pass through
some foundational clarifications), and ii. the mathematics one
develops on it can be understood by everybody.
Perhaps the minimalist foundation is complicated (since it faces the
complexity of all ingredients: sets, collections, recursive
functions,...), but the mathematics you do with it is very simple. I
am surprised to learn that you believe that the "nice idea" of formal
topology is "treated a little complicatedly". The central idea is
that the structure of open subsets (formal topology) can remain
effective also when that of points (formal space) is wholly ideal.
They are linked by the functor Pt producing formal points. This idea
is treated in a general form, which means it has an algebraic or
axiomatic flavour. Perhaps this is what makes it look "complicated"
to you, since the algebraic attitude is hardly present in Brouwer,
Bishop, etc.; to the contrary, to my taste, the algebraic language is
exactly what makes it so simple and perspicuous, since it allows you
to see the main ideas beyond the details of specific examples (and
without having to carry out all the time the computational
interpretation).
In the minimalist foundation, in which not even AC! is valid, the
notion of formal point can become a rigourous version of Brouwer's
notion of choice sequence. M. Maietti and I have recently proved that
Bar Induction BI (Brouwer's thesis) is compatible with CT (Church
Thesis).
Moreover, if you restrict to functions between formal spaces produced
by the functor Pt, they are all continuous. This gives a rigourous
meaning to Brouwer's continuity principle.
So you see that I personally have nothing against the use of
Brouwer's principles. But in the same time I offer a framework in
which you can see very well that you can do a lot without them. This
is also for the sake of communication with other views.
In conclusion, also after skimming through your paper, I believe that
you would like formal topology and the frame of mind around it, if
you find the energy to understand it a little more. For example, what
you call a genetic bar is nothing but a cover (which on a tree is
inductively defined). And BI is just the claim: every bar is
inductively defined. You find this discussed in the last section of
my first paper in 1987 (see
http://www.math.unipd.it/~sambin/txt/ifs87-97.pdf).
Also your general cultural attitude towards the various positions in
constructive mathematics is very congenial to mine. You find a
detailed discussion of my view in the third section of the paper
"Some points in formal topology" (see
http://www.math.unipd.it/~sambin/txt/SP.pdf), keeping in mind that
this was written 6 years ago, and I hope my ideas have improved since
then.
I hope somebody else can answer to your specific questions.
With my best wishes
Giovanni Sambin
More information about the FOM
mailing list