Bourbaki and foundations

[Lawrence Paulson]

Especially since joining Twitter, I see so much nonsense about sets, types and categories that it drives me to despair. Some of it seems to be connected with ideas from univalent foundations: the idea that a foundation of mathematics must be a formal system. Therefore set theory is a formal system and indeed mathematics as a whole is just a formal system.

Types were always just syntactic restrictions imposed on formalisms, but now people assert that types are bona fide mathematical objects. People seem unable to say what these objects are, except that they are definitely not sets. Others seem unwilling altogether to utter the S-word.

I wrote a blog post a while back trying to clarify some of these points, in particular my view that a foundation has only one real purpose, namely to justify how mathematics is done:

https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html

In my own building, students have posted memes mocking the axiom of choice and even ex falso quodlibet. Seriously, it looks like a cult.

Larry Paulson
On 13 May 2022, 01:26 +0100, Timothy Y. Chow <tchow at math.princeton.edu>, wrote:
On Mon, 9 May 2022, JOSEPH SHIPMAN wrote:
So far I have not seen anyone give an explanation that makes sense of
what is WRONG with set theory.
[...]
WHO is forcing anyone to use set theory in a way that requires any
significant and unnecessary effort?

To be clear, I don't think there's anything "wrong with set theory" in any
absolute sense. When Aczel speaks of "myriad problems and inadequacies"
and a "flawed system," I think he's overstating the case for the sake of
telling a good story.

On the other hand, I think I understand what's behind the complaints. If
you are a practitioner of some subfield of mathematics, then one thing you
typically want from a "foundation" is an axiomatization that accurately
captures the fundamental nature of the structures you are studying.
Faced with various logically equivalent alternatives, you are going to
pick the one that you feel best reflects the "essence" of the
subject---without any artificial or extraneous features---and that lets
you develop the basic theory with ease and elegance. From this point of
view, what's "wrong" with sets is that defining objects in terms of sets
often comes across as an artificial encoding procedure.

Here's an analogy that may help. If I'm studying sorting algorithms, I
will probably want to write my algorithms in some high-level programming
language. I don't want to have to program a Turing machine. What's
"wrong" with the Turing machine is that the process of encoding an
algorithm for a Turing machine comes with a lot of extraneous baggage that
obscures the essential differences between the sorting algorithms.

I don't think that any of the critics of set theory are saying that you
*can't* use sets as a foundation, nor are they denying that set theory is
well suited for certain tasks. What they're objecting to is the
suggestion that the only viable way---or at least the uniquely best
way---to develop a foundation is by means of set theory, even if what you
are seeking is Essential Guidance and not Risk Assessment or Generous
Arena.

Tim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220513/bcb07931/attachment-0001.html>