[taejo]

> The problem with this is that it is wrong.

> You can translate between different logical theories by building a model of one in another, so it's not like you loose anything. But it's cooky to insist that we should start with ZFC of all things.

I don't see how these two are consistent. Almost everything most mathematicians do can be done both in ZFC and your favourite non-kooky axiom system. Certain Powers That Be seem to have decided that ZFC is the foundation of mathematics, so they say that what they're doing follows from ZFC even if they have a very hazy idea of what it is, but why does it matter? Most mathematics probably won't be formalized in their lifetime anyway, so whether it ends up being formalized on top of ZFC or something else doesn't affect them.

[btilly]

Almost everything most mathematicians do can be done both in ZFC and your favourite non-kooky axiom system.

You would be amazed at how many uniqueness and existence theorems in how many areas of mathematics require Zorn's Lemma. Which is, of course, equivalent to the axiom of choice. For example, "Every vector space has a (possibly infinite) basis." Or, "Every Hilbert space has a (possibly infinite) orthonormal basis."

It is rare for mathematicians to think much about choice. But it underpins key results in a surprising number of fields.

[fmap]

Slightly tongue in cheek, but the analogy to programming is this:

> "Almost everything most programmers do can be done both in x86 assembly and your favorite non-kooky programming language. Certain Powers That Be seem to have decided that x86 is the foundation of computer science. [...] Why does it matter?"

The problem is that it is difficult to translate results in a theory built in ZFC to other "architectures". In mathematics, the architectures in question are not different axiom systems, they are different branches of mathematics.

Let me give you an example. There is a large body of work on differential geometry with many useful constructions. Classical differential geometry works directly in a model where manifolds are certain subspaces of (countable products of) R^n. These constructions have been successfully imported into many different areas of mathematics. In most cases people just had to tweak the definitions slightly and adapt the proofs by keeping the basic strategy and changing all the details.

What is happening here is that the underlying ideas of differential geometry are not specific to this particular model.

When faced with such a concrete model, our first instinct should be to abstract from it and ask which assumptions are required. This is difficult in ZFC, because in the end you have to encode everything into sets. It's not possible to reason about "abstract datatypes" directly, without literally building a notion of logic (generalized algebraic theory) and models of it within ZFC. Even then, the existence of choice means that you usually have to exclude unwanted models of your theory.

Coming back to differential geometry: You can generalize a lot of it by working in a differentially cohesive (infinity-)topos. This is terribly indirect (in my opinion) and looses a lot of the intuitions. A topos is literally a model of a certain logic. Alternatively you can work directly in this logic (the "internal language" of the topos), where the differential geometric structure is available in the form of additional logical connectives. You are now talking in a language where it makes sense to talk about two points being "infinitesimally close" and where you can separate the topological from the infinitesimal structure.

At the same time you reap the benefits that there are many more models of differential cohesion than there are models of "R^n modeled in classical set theory". You can easily identify new applications, which might in turn suggest looking into different aspects of your theory. It's a virtuous cycle. :)

This approach is deeply unnatural when working in set theory or arithmetic. You have to encode everything into sets or numbers and then these sets or numbers become the thing you are studying.

[taejo]

I only studied mathematics, never actually been a professional mathematician, and I feel like a big difference might be in what we see as "most mathematicians" (if you're working in this area you're probably more right than I am! but it's also possible your view is focussed on people working in areas related to yours).

I'd make the following alternative analogy: I code in Python on an x86, because that happens to be the machine on my desk. If you told me I should be using POWER instead of x86, I'd probably just shrug: I could do that - my work is portable - but it's also completely irrelevant to my work. I think this would be how most people in say analysis, algorithms or combinatorics feel, for example.