[FOM] continuing problems with constructive continuity?

[giovanni sambin]

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