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

[Frank Waaldijk]

Harvey Friedman wrote:

In any case, it would be even more valuable if there was a short piece
> of the kind I was describing concerning foundations of intuitionistic
> logic or intuitionism or constructivity, where we are with it, and in
> particular the role of the Creating Subject, and so forth.
> Intuitionism seems tp be remarkably stable under many
> "interpretations" even if they are rather rough/vague, and that seems
> to make it very likely to me that there is a lot more to be discovered
> concerning its foundations.
>

Allow me to give an overview on a personal note, since precisely this
subject cropped up recently on the constructive-news forum (
https://groups.google.com/forum/#!topic/constructivenews/e3JfKk_W2jI). 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.

Intuitionistic mathematics (INT) has sharp and precise foundations,
allowing for a continuing development of all fields of mathematics within a
stable and elegant framework. The same holds for constructive recursion
theory RUSS (intuitionistically valid if MP is left out; but my position as
an intuitionist is that MP is valid in INT as well).

This stability and coherence is in contrast with other contemporary
constructive approaches.

BISH (Bishop-style mathematics) has proven too vague in its foundational
definitions and coherence. Both its original definition of `continuous
function' and an alternative (1979) can be shown to have the desired
properties if and only if the Fan Theorem holds (the very FT that Bishop
called `mystic' and unnecessary). Basically because the desired properties
include uniform continuity on compact subspaces. Other than what Bishop
thought, this cannot be solved by adding this property to the definition of
`continuous'. In my eyes, also already the definition of a `function' in
BISH is already far to vague.

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. (To draw some more discussion)
I hope you'll grant me to comment biasedly on some of these ways.

I see

* Formal topology as a complicated affair, using transfinite inductive
machinery that is in essence Brouwer's Bar Induction. The main use of the
transfinite induction seems to be to salvage uniform continuity and related
compactness properties (but I'm no expert). It seems rather unsuitable in
my eyes for analysis. 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. I
suspect that the definition of `subspace' has not been really tested, and I
also am still unconvinced that the continuous-function definitional problem
has been resolved.

* that in analysis, Douglas Bridges and Luminiţa Simona Vîţă have changed
BISH-continuity, dropping the `uniform continuous on compact subspaces'
requirement. They also are working on a form of `apartness topology' which
to me seems more complicated and less effective than the apartness topology
that is in essence Brouwer's (but which was first explicitly defined in my
PhD thesis). I cannot find any explicit position that earlier BISH theorems
are now `no longer valid' or something similar, and I am also unaware of
any interest to locate conflicts between the two earlier definitions (the
1967 and the 1979 versions).

* that Homotopy type theory (HoTT) claims to be the answer also to
constructive math's foundational problems. But the chapter on constructive
math is in my eyes just a stub. Foundational compatibility, elegance and
ease of practice (analysis, topology, ...) to me look terrae non
consideratae.

* other `core' initiatives that address constructive mathematics gather
less steam. Abstract Stone Duality (ASD) is unfortunately still over my
head, but seems to address the right questions. Natural Topology (NToP)
basically translates Brouwer's topological concepts to BISH (and also to
classical topology), through an idea of Wim Couwenberg.

* model-theoretic, category-theoretic, proof-theoretic, topos-theoretic,
... developments, in which I have a hard time to understand what precisely
is the constructive content, and what precisely is relevant to someone like
me who would like to prove say the Michael Selection Theorem in
topology/analysis, or other `low-level' stuff.

(* also constructive and intuitionistic reverse mathematics developing)

Therefore my personal conclusion is:

The only foundationally precise, mathematically elegant and comprehensive
constructive theories today are INT and RUSS. These theories are accessible
for non-specialists, have been thoroughly vetted and are stable in the
sense that theorems proved 50 years ago can be used unaltered, since
definitions nor axioms have changed.

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.

Hoping to have contributed something,
best wishes,

Frank Waaldijk
www.fwaaldijk.nl/mathematics.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161218/d877828b/attachment.html>