Bourbaki and foundations

[Sam Sanders]

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