[AnimalMuppet]

The foundations have real implications on very little of the mathematics. Say I'm working in differential equations in vector spaces. I really do not care whether the axiom of choice is true or false. I'm not building up my functions of multiple real parameters out of sets.

You say you have a foundation where that is in fact what I am doing? Great, if that floats your boat. I don't care. That's several layers of abstraction away from what I'm doing. I pretty much only care about stuff at my layer, and maybe one layer above or below.

[black_knight]

Very little of mathematics, like analysis? I am sure the analyst will care about all functions on the reals suddenly turning continuous. (Or rather losing the discontinuous ones)

Or what of commutative algebra and their beloved existence of maximal ideals!

[adgjlsfhk1]

you're kind of coming at this backwards. it's not that someone doing analysis doesn't care about whether all functions on reals is continuous, it's that if you hand them a foundation where that's true, they'll disagree with whether your foundation is correctly modeling functions/real numbers.

[black_knight]

At which point we would have an interesting debate! I could tell them all about how this foundation will give them a more nuanced view on continuity!

[johngossman]

I suggest you go meet some PhD mathematicians and have that discussion.

[black_knight]

Having a PhD in mathematics myself, I have been surrounded by such and had this discussion a few times. Some even like the ideas suggested!

I would say the most common counter argument is cultural: Classical mathematics is the norm in the field, hence one must use it to participate in research in this field.

But that seems to me a rather intellectually unsatisfying argument, if one cares about the meaning of the work.

[romangarnett]

Do you not care if your vector space has a basis?

[qbit42]

It is nicer to state theorems that hold for all vector spaces, so mathematicians like to invoke AoC. However, in any applications that are practically relevant, you can obtain a basis without invoking AoC.