[FOM] Troelstra's Paradox and Markov's Principle
sambin at math.unipd.it
Thu Dec 22 11:43:06 EST 2016
On 12/18/16 2:39 PM, Frank Waaldijk wrote:
> This overview will show my large ignorance in most areas, I know, but
>I would like to hear from others about their perspective on these matters.
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
> 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
Let me rectify one by one some of your mistaken claims:
>using transfinite inductive machinery that is in essence Brouwer's
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
>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
>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
Best wishes for 2017!
More information about the FOM