Bourbaki and foundations
sasander at me.com
Fri May 20 04:59:38 EDT 2022
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.
More information about the FOM