On 12/03/14 21:34, Thomas Streicher wrote:
> Dear Steve,
>
> I think we agree mathematically but disagree w.r.t.
>
> 1) what is simple and what isn't
> 2) the role of the ambient logic.
>
> Thanks for pointing out that Thierry's work not only constructivized
> existing topological arguments but that he also invented new such
> arguments. It hasn't been my intention to deny this.
I have (temporarily?) suspended my thoughts about locale theory/formal
topology, to focus on recent interests. (And also because very few
people in the world were/are interested in this (less than I have
fingers to count).)
But I would like to make a few comments.
From my *personal* point of view (and (published) experiences with the
subject), in this particular case, impredicative arguments are more
natural (for what I did do and tried to do).
Formal topology = locale theory developed predicatively.
Formal topology is too "syntactic" to my personal taste. This is fine
when the applications are to algebra, like in Thierry's work. But when
the applications are to analysis and to (point-free) topology regarded
as a generalization of analysis, more generally, the predicative
calculations are possible but do seem to become cumbersome (although
some people enjoy them).
> What really is the background of my complaints is that I don't see
> what is the intended application of formal topology and related
> approaches like yours.
Well, if you are looking for "applications", you already are aware of
some.
In programming language semantics, logics and verification, developed
*non constructively* (as is the tradition in theoretical computer
science), the locales are the "logic of observable properties", their
formal presentations are their algebraic treatment, and their
corresponding topological spaces give the official "intended"
semantics of programs (perhaps in the form of domain theory).
(BTW, it is a *myth*, as you know, that theoretical computer
scientists are constructively minded (alluded to by Fred
Richman). Most of them are not. Most of them don't understand what
constructive mathematics is (not). And don't care. And even dismiss
it. The idea is that if you already have written a computer program,
there is no point in working hard to prove constructively that it
works. A classical proof is regarded as perfectly sufficient.)
> Do you suggest to redo constructive analysis in a pointfree and
> prediactive way or do you reserves those methods for topology beyong
> Polish spaces. I can see the point of the latter but not of the
> former. Quite concretely, I think it is a nightmare to rewrite the
> first chapters of Bishop (and Bridges) in terms of formal topology.
I will wait to see what Steve has to say about this.
But here is my take: I would suggest that (constructive and
non-constructive) analysis can and should be done in a point-free way.
Regarding the nightmare: This is what Hilbert told Brouwer, and then
came Bishop, who transformed the nightmare into a dream (for some).
What is needed, again, is somebody to rewrite analysis in a compelling
pointfree way. Arguments in this mailing list won't be enough.
> Just think of introducing sine a cosine or logarithm in such formal
> terms. I wonder whether anyone seriously want's to do this.
Ah! I think this is not a problem at all, once the right
infrastructure is introduced.
Any version of real analysis will need to begin with some
infrastructure (even the HoTT people have proposed what this
infrastructure ought to be in HoTT, although the HoTT infrastructure
hasn't been "tested" yet).
The infrastructure will always (even in the classical case) be a bit
artificial and "logically looking". But once this is settled, I expect
point-free real analysis (when it is done properly) to look very much
like point-set analysis.
Martin