Comment by ux266478

> Most foundations are in a sense equivalent. Therefore, "ZFC" is as good of an answer as any.

This doesn't follow. The sense in which they are equivalent is that they are equifinal, which doesn't mean isomorphism or even homomorphism. It's a meaningful thing in theory, but not in reality. Otherwise, Turing tarpits wouldn't be a thing.

Every foundation occupies a unique region of proof space. Your foundation, and everything that goes into it, doesn't just affect the shape of what's accessible to you in native semantics, it also effects the way you move through this space. This means by changing foundation, not only can we prove things that we otherwise couldn't in theory (in native semantics), it also means we can prove things we otherwise couldn't in practice (what embedding other foundations as object languages doesn't get you). You can recognize a little bit of this in that it makes some things seem easy, but that's an extremely trivial case of what this relationship implies.

It's all just tools in a toolbelt. Treating them like immutable, universal truths is worth tolerating merely out of human limitation, because it's a lot of work to build intuition for a foundation. If we're talking about philosophy of mathematics though? No, it would be a mistake to pretend like choice isn't meaningful. It is extremely meaningful, and there's a lot to be gained out of realizing they're actually just highly specialized tools. Something to grab when it's useful, and throw away when it's not.