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