[pmoriarty]

"In this sense all three have ontological force; they codify what is, not how to describe what is already given to us."

What's the difference between "what is" and "what is already given to us"? What's the difference between codifying and describing it?

[danharaj]

20th century mathematics takes first order classical logic and set theory as foundational. All other mathematics then becomes the analysis of sets via proofs in first order classical logic. The ugliness of this definition is that it is unnatural. Mathematicians don't always think in sets, they think directly about mathematical objects intuitively. No one cares which set encodes the number e, for example, but foundationally speaking the number e must be a set, and the properties of e are the properties of that set. This is unsatisfactory from both an aesthetic and practical point of view: the Set foundations of modern mathematics obscure the fundamental, recurring themes of mathematics.

This is true even in computer science. Turing machines are sets too! I know, ridiculous.

Harper is saying that the correspondence between logic, language, and category is a suitable foundation for mathematical/logical/computational activity and they're all the same thing. This is not merely in the sense that the objects we work with are given beforehand by some more fundamental theory and we are merely analyzing them, but in the sense that logic/language/category is the appropriate setting in which to define our objects, to do synthetic as well as analytical reasoning. That is what makes a particular theory foundational.

[AnimalMuppet]

> All other mathematics then becomes the analysis of sets via proofs in first order classical logic.

That's like saying that home construction becomes an exercise in atomic physics. Yes, in some sense it's true, but it's so far removed from what's actually going on that it's completely uninteresting.

Take the person working on differentiable manifolds. Do they care about that as problems in set theory? Not at all. Change it to problems in logic/language/category theory? They still don't care. Axiomatize mathematics how you will, they won't care, because they're as many layers away from it as the home construction people are from atomic physics.

[danharaj]

https://ncatlab.org/nlab/show/motivation+for+higher+differen...

Without category theory, certain generalizations of differential geometry would be virtually impossible to describe in any useful matter. These generalizations are extremely important for applications to physics and elucidate a lot of the fundamental structure of the classical theory. Furthermore, you get a much nicer theory when you consider higher geometric structures.

The power of category theory as foundations is that it lets you efficiently study the structure of a theory and how to modify that structure in principled ways.

Sure, the mathematician who is doing hard analysis probably does not care too much about category theory, but every mathematician being educated today knows at least a little category theory because it is the natural setting for certain key mathematical ideas, like cohomology.

In contrast, Set Theory is powerful but it doesn't organize mathematics the way logic/languagecategory theory does.