[FOM] Troelstra's Paradox and Markov's Principle

[Frank Waaldijk]

Dear Giovanni,

thank you for your thoughtful reply. To give credit also (and not only
criticize...) let me state clearly that I have learned a lot from Formal
Topology, and that I also really appreciate your philosophical-mathematical
views on constructive mathematics. Furthermore, your answer shows that you
take my remarks seriously, yet kindly even though I play the devil's
advocate. I appreciate your humanist and respectful style, and (less
important to me) it seems a more fruitful approach than ignoring such
remarks, because valid (meta)mathematical arguments have a tendency of not
going away.

I also appreciate that you share my wish for a common platform for
constructive mathematics. Would it be really such a bad idea to start
something like that as a program? It could start with an informal
conference, where free discussion and devil's advocacy are welcomed.

To play devil's advocate is not my favourite game, because I feel
mathematics is a collective endeavour, and I prefer to look for merits and
collaboration rather than for deficits and conflicts. There should actually
be no real conflicts in mathematics itself, just misunderstandings which
can be cleared up (in time, through much effort sometimes). My big
mathematical hero in this respect is not Brouwer (as some seem to think
simply because I advocate using Brouwer's topological methods in
constructive math), but Kleene.

Kleene stripped Brouwer's intuitionism of all the inessential (less
essential perhaps) embroiderings and paraphernalia, not out of disrespect
but to simplify. And this simplification stands today as clearly
intelligible as in 1965. Yet Kleene's work on intuitionism (FIM) is largely
neglected. My question whether Kleene actually constructively proved
Brouwer's axioms (through realizability methods, in 1969) has gone
unanswered so far here and on Mathoverflow.

It is my strong conviction that Bishop really didn't understand Brouwer
well enough, otherwise he would have taken Brouwer's Fan Theorem a lot more
seriously. Brouwer was a master topologist, and topology is the very
foundation for constructive mathematics. Brouwer, through his endless work
on Baire space, understood that FT is actually derived from transfinite
induction, and that one cannot really elegantly do constructive analysis
without some form of transfinite induction (or axioms) [I will come back to
this unjustified remark later, please bear with me].

But Brouwer went further: he analysed the way in which we could
constructively arrive at the secure knowledge: `for all \alpha in Baire
space there is an n in N such that \alpha*n* is in A' (where \alpha*n*
indicates the finite string of the first n values of \alpha). And he
concluded that the only constructive procedure to arrive at such knowledge
could be transfinite induction. In my opinion (so far unchallenged) Kleene
actually proved this, through his realizability methods, in 1969.

Brouwer however proceeded to formulate this in difficult language and
(meta)mathematical concepts, giving `proofs' which to me are complicated
metamathematical justifications [still, to me: valid, when corrected and
simplified]. After being treated not respectful at all by his
contemporaries he became more reclusive and `mystic' to many. Ever since it
seems that constructive mathematicians are eager to distance themselves
from Brouwer, mostly to their own cost if you ask me.

In my thesis (*modern intuitionistic topology*, 1996) I noted already
clearly that the Bishop definition of continuous function was deficient. I
could not get anybody interested in this. When I proved rigourously that to
repair this deficiency the Fan Theorem was necessary and sufficient,
ignoring it was no longer an option (see my 2005 paper *On the foundations
of constructive mathematics --- especially in relation to  the theory of
continuous functions*).

For almost 40 years Bishop's school maintained that FT was unnecessary. Now
people in Formal Topology have been stating for more than 10 years that
they will solve this problem without FT. You will understand that I am a
little sceptical, especially since no effort seems to have been made to
really develop analysis with Formal Topology methods. The fact that there
is no clear, non-changing, axiomatic and definitional framework for Formal
Topology doesn't help me lose this skepsis.

On the plus side: Formal Topology has pushed me to develop Brouwer's
constructive topology in a new way. The resulting 2011 book *Natural
Topology *
has been revised in 2012 and is available on arXiv. Its axiomatic basis is
a restriction of the BISH axioms (since the BISH choice axioms are to me
unacceptably vague), with the added axiom PGI: the Principle of Genetic
Induction.

In NToP, I prove the equivalence over Baire quotients of PGI with the much
more complicated PFI (Principle of Formal Induction, which I had to
formulate myself, since I could not find an axiomatic description of it,
which may be my fault of course) which is used (I believe!) in Formal
Topology.

Furthermore, in NToP I show that Brouwer's ideas suffice to do both
pointfree and pointwise topology, and analysis, at the same time. This
because points remain sequences, and therefore elements of Baire space. The
beauty of Brouwer's methods is that continuous functions themselves can
also be unambiguously coded as elements of Baire space. To do so elegantly
and efficiently is a prime aspect of NToP. A few weeks ago, I showed on the
constructive-news-forum how this can be used to eliminate the use of
countable choice in many constructive proofs.

NToP captures all Polish spaces, and more (also non-metrizable spaces),
since it covers all \Sigma_01-apartness quotients of Baire space.

>From NToP, I wrote an article on exact computation (*Exact computation over
topological spaces*, preprint 2013) which shows how NToP methods can be
used as an elegant and efficient interface between constructive theory and
computation. The review process is still ongoing...

So far, I have had no real reaction from the constructive community on
NToP. It may therefore be true that I am not well informed on Formal
Topology, yet it seems to me that this holds two ways.

Well, I said my piece, so let's end on the same positive note as on which
we started:

Hopefully this interchange will lead to more comments and reactions, with
the aim of uniting and simplifying constructive foundations and practice.

Best wishes for 2017 to all!

Frank Waaldijk

www.fwaaldijk.nl/mathematics.html


Dear Frank,
> I also feel I would like to know more on many topics, but have to accept
> my ignorance.  So I touch here only the issues you raise in which I really
> have something to say by direct working experience (that is why I do not
> touch: creating subject, apartness spaces, abstract Stone duality, model
> theory, HoTT, Natural Topology, etc.). The aim of my post is just to
> rectify some of your comments and in the same time offer some positive
> information.
>
> > This stability and coherence  [of INT and RUSS] is in contrast with
> > other contemporary constructive approaches.
>
> See below about MF.
>
> >A multitude of ways to deal with this are currently developed, but there
> >seems to be no accepted common framework that would also include
> >INT and RUSS, and/or validate earlier work in BISH.
>
> See below about MF.
>
> >I see Formal topology as a complicated affair,
>
> To be frank, your comments on formal topology show that it is indeed
> something mostly obscure to you. Formal topology is not difficult, but it
> takes some time to familiarize with its underlying intuition, which is new
> to mathematics, since it is totally predicative (and hence respects
> whatever computational content). Other constructivists have other
> intuitions, of course, and this is a source of richness.  I am very much in
> favour of pluralism in mathematics and its foundations. So I do not expect
> a "canonical" foundation or intuition, even if we restrict to
> constructivism.
>
> None of the issues you mention on formal topology is a real problem or
> obstacle.
> Let me rectify one by one some of your mistaken claims:
>
> >using transfinite inductive machinery that is in essence Brouwer's
> >Bar Induction.
>
> Formal topology uses transfinite induction, of a totally controlled kind
> (in particular, provably consistent), precisely to *avoid* assuming Bar
> Induction (this is clear since Per Martin-Löf's  thesis "Notes on
> constructive mathematics", 1970). It is used to extract the computational
> content (inductive and coinductive generation) of classical examples, such
> as Baire space, Cantor space, Dedekind and Cauchy style real numbers,
> Zarisky topology.
>
> >The main use of the transfinite induction seems to be to salvage
> >uniform continuity and related compactness properties (but I'm no expert).
>
> I am also not an expert on uniform continuity (thus I abstain from
> comments and refer to Erik Palmgren for a solution of the issue). But that
> is for sure not the main use of transfinite induction in formal topology.
>
> >It seems rather unsuitable in my eyes for analysis.
>
> I expect formal topology to be perfectly suitable for analysis. The fact
> that there is nothing comparable to the spectacular development of analysis
> in Bishop style does not mean it is unsuitable. I actually conjecture that
> one could even find some general metatheorems saying that one can do (most
> of) analysis informally in the style of Bishop and still keep all the
> advantages of the rigorous foundation and explicit computational content as
> in formal topology.
> The huge benefit of formal topology (developed over MF, see below) is to
> keep effective (pointfree topology) and ideal aspects (ideal points and
> ideal spaces) of mathematics in the same framework, and still clearly
> distinct (and provably consistent, that's understood). This should be
> extremely interesting  for instance for those who care, on one hand,  about
> exact real number computation and are interested, on the other hand, in
> keeping some geometric intuition.
>
> >There is a fair community, but I have not seen any book that
> >builds up the subject from the foundational ground level, and
> >shows its aptness, coherence and compatibility with other developments.
>
> You correctly ask for a book on formal topology (but recall Brouwer never
> wrote a book after his thesis), and I am a bit touchy on this point. You
> perhaps already know that I am writing an extensive book on constructive
> topology (I have over 400 pages ready) to be published by Oxford UP. I hope
> it is out in 2017. One of the reasons it has taken longer than planned is
> indeed that many interesting novelties have emerged while writing it,
> witnessing the potential of formal topology. Moreover, all its content is
> developed over the minimalist foundation MF (see below). Finally, I have
> been writing it in a way every master student can understand (I have
> already tested this several times).
> Before the book is out, if you are curious you perhaps can read with
> profit, as many other do, my survey paper "Some points in formal topology",
> see http://www.math.unipd.it/~sambin/txt/SP.pdf. There you find an
> introduction to the original formal topology developed with Per Martin-Löf,
> the main notions of my new variant which I now call Positive Topology, and
> an exposition of my views on foundations. In over a dozen years, there have
> been many further developments, both in constructive topology and in
> foundational views. They will all be in my book to appear.
>
> >I suspect that the definition of `subspace' has not been really tested,
>
> There are no signs supporting this suspect of yours. To the contrary, in
> our new approach (positive topology) the notion of subspace is even
> clearer, as well as other ways to construct spaces from given ones.
>
> >and I also am still unconvinced that the continuous-function
> >definitional problem has been resolved.
>
> I see absolutely no problem with the definition of continuous functions in
> formal topology. Actually, our approach gives a privileged perspective on
> Brouwer's continuity principle, making it clear with mathematical rigour in
> which sense it is true.
>
> >Therefore my personal conclusion is:
> >The only foundationally precise, mathematically elegant and
> >comprehensive constructive theories today are INT and RUSS.
>
> >In the past two decades I have infrequently raised this `common
> >platform' issue, but I am unaware of any systematic approach/development
> >in this area. There are of course many specialist publications that
> address
> >parts of these issues, but I have a hard time pasting these publications
> >together (if this is at all possible) to something that approaches such
> >a common stable platform.
>
> I also feel the "common platform" issue. In fact, together with Milly
> Maietti, in 2005 we have introduced what we call the Minimalist Foundation
> (MF). See http://www.math.unipd.it/~sambin/txt/MaiettiSambin-rev2.pdf. It
> has several primitive concepts (set, collection, proposition and their
> variant depending on arguments,  thus providing the notions of operation,
> subset, relation, function) and essentially no assumption about them. It
> aims  to maximize the capacity of concept resolution by minimizing
> assumptions. I like it because it corresponds faithfully to the  intuition
> that every abstract concept must refer in a clear, although indirect way to
> something concrete.
> MF can act as the common ground you are looking for. In fact, all
> foundations I know of (classical or not, type theoretic or not) can be seen
> as extensions of MF. Since it is very simple, I expect it to remain stable.
>
> Best wishes for 2017!
> Giovanni Sambin
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161229/9e6d8049/attachment-0001.html>