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

[Giovanni Sambin]

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.

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