FW: Bourbaki and foundations

[Kreinovich, Vladik]

An interesting constructive-related comment on the foundations of math mailing list

-----Original Message-----
From: FOM [mailto:fom-b...@cs.nyu.edu] On Behalf Of Sam Sanders
Sent: Friday, May 20, 2022 3:00 AM
To: tc...@alum.mit.edu; Foundations of Mathematics <f...@cs.nyu.edu>
Subject: Re: Bourbaki and foundations

Dear FOM,

Chow made the following remark, which I elaborate upon.

> to emphasize again that what's being debated is not whether traditional foundations *can* do the job, but whether an alternative approach is easier or more elegant or more enlightening. It should not be surprising that such questions are a matter of opinion and are up for debate and discussion.

The issue of developing foundations close to mathematical practise is a difficult one. I think one can do this only “locally”: a given foundational paradigm may be good at developing subfields X, Y, Z while close to the practise of X, Y, Z, but will fail to do so for other subfields W, V, U.
There cannot be a foundational paradigm that develops all of mathematics close to mathematical practise.

Related to this topic, I repeat the following relevant observation: the first chapters of Bishop’s book on constructive analysis have been formalised. It was noted that all results (except two exercises) are optimal as follows: if you weaken the assumptions or strengthen the conclusion of any given theorem, it becomes non-constructive (in that Brouwerian counterexamples exist). Bishop reportedly also stood out for being able to produce Brouwerian counterexamples “on the spot”.

My point is the following: it seems that developing a coherent framework for constructive analysis requires one to step outside of constructive analysis. In particular, one has to painstakingly verify that all the definitions and theorems fit together as a constructive whole, developing lots and lots of Brouwerian counterexamples, which Bishop claimed were only supposed to be sidenotes in constructive math.

This is not a criticism of Bishop (or anyone): I merely wish to point out that “just doing mathematics with intuitionistic logic” is unlikely to yield the edifice Bishop has produced: one has to step outside of that mindset and into a “more foundational” one, which is what Bishop seems to have done via Brouwerian counterexamples.

I believe this observation has some universality to it: developing the foundations of a subject, even if the goal is to stay close
to the practice of that subject, is bound to take you (far) outside of it.

Best,

Sam

[Steve Vickers]

> This is not a criticism of Bishop (or anyone): I merely wish to point out that “just doing mathematics with intuitionistic logic” is unlikely to yield the edifice Bishop has produced: one has to step outside of that mindset and into a “more foundational” one, which is what Bishop seems to have done via Brouwerian counterexamples.

As we know, “just doing mathematics with intuitionistic logic” is seldom as simple as that. Each classical formula can have a range of non-equivalent constructive formulations, and we have to examine the possibilities and how they fit together - hours of fun, but it seems more than “just doing mathematics”.

However, when it comes to topology and analysis there’s a much deeper issue of formulation. One of the bigger messages from topos theory is it makes a huge difference if one approaches topology point-free instead of point-set. For example, Tychonoff and Heine-Borel become true. The basic reason for the improvement is really one of topology, not logic. Internally in sheaves over a space X, objects correspond to local homeomorphisms over X, whereas point-free spaces correspond to more more general bundles (maps to X). Thus to take the “set of points” (discrete coreflection) of a point-free space in the internal, intuitionistic logic, is to approximate a general bundle by a local homeomorphism, and this cannot always be done adequately.

A simple example is to take X to be Sierpinski $ and consider its closed point as a map 1 -> $. Its discrete coreflection, as local homeomorphism to $, is easily calculated to be that of the empty set, the initial sheaf.

In fact examples in sheaves over $ are common, and it seems to me they often play the role of Brouwerian counterexamples. Instead of considering some explicit unknown proposition, you just use the generic proposition in sheaves over $ and calculate there.

By the way, Palmgren in “A constructive and functorial embedding of locally compact metric spaces into locales” showed how Bishop’s apparently ad hoc point-set formulations correspond to more natural ones point-free.

All the best,

Steve.

> On 24 May 2022, at 03:23, Kreinovich, Vladik <vla...@utep.edu> wrote:
>
> An interesting constructive-related comment on the foundations of math mailing list

> --
> You received this message because you are subscribed to the Google Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/constructivenews/ef69d4bacdee46a9b849e6e28409713f%40ITDSRVMBX011.utep.edu.