Say we have DCλ where λ is some inaccessible cardinal. Is that enough to develop all of ordinary mathematics? If not, is there a strengthening that is but that nevertheless does not assume full choice high up in the universe of sets?

2$\begingroup$ Related: What can be preserved in mathematics if all constructions are carried out in ZF? $\endgroup$– Timothy ChowAug 11 at 11:17

$\begingroup$ In "ordinary" linear algebra do we want: "every vector space has a (Hamel) basis" ?? And isn't that equivalent to the full AC? $\endgroup$– Gerald EdgarAug 12 at 7:15

1$\begingroup$ I'd really like every ideal of a ring with unit to be contained in a maximal ideal. I can probably get away with elaborate periphrastic circumlocutions, but I hate it when that happens. $\endgroup$– Dave BensonAug 13 at 21:30

1$\begingroup$ Is "elaborate periphrastic circumlocutions" an elaborate periphrastic circumlocution? $\endgroup$– Gerry MyersonAug 13 at 23:19

1$\begingroup$ @GerryMyerson It's a repetitive redundancy. $\endgroup$– Elizabeth HenningAug 14 at 1:06
4 Answers
Your hypothesis is in a sense stronger than just assuming ZFC outright.
Namely, if we have $\lambda$DC for some inaccessible cardinal $\lambda$, and ZF in the background, then in particular, we will have the full axiom of choice inside the universe $V_\lambda$, consisting of all sets of rank less than $\lambda$, since $\lambda$DC implies choice for all families of size less than $\lambda$. So $V_\lambda$ will be a model of full ZFC.
Therefore, by simply jumping inside this universe $V_\lambda$, we recover full ZFC for all the purposes of "ordinary mathematics." If all ordinary mathematics would take place inside such a universe, then the answer would be yes.
But let me note that it is somewhat subtle to define what one means by inaccessible cardinal in the absence of the axiom of choice, since the usual definition would be that $\lambda$ is an uncountable regular strong limit, but being a strong limit should mean that if $\kappa<\lambda$ then $P(\kappa)<\lambda$ as well, and so in particular, $P(\kappa)$ is wellorderable. But in this case it follows by definition that if $\lambda$ is inaccessible, then the axiom of choice holds in $V_\lambda$ just as a consequence of inaccessibility.
In other words, we get ZFC in $V_\lambda$ even without your $\lambda$DC assumption. In this sense, the power of your hypothesis for ordinary mathematics consists of your having an inaccessible cardinal in the first place, rather than in your having $\lambda$DC.
Controversial counterpoint. Meanwhile, let me also say that my view also is that we would make a fundamental disservice to mathematics and to ourselves by attempting to limit our mathematical conceptions to those ideas that have proved productive in the past, limiting ourselves to the ideas used in "ordinary" realms of mathematics. Set theory has discovered a vast new tranfinite realm of mathematical reality and fundamental principles that govern it, such as the axiom of choice but also large cardinals and many new strong principles with transformative global effects. In my view, the fact that those principles do not apply as much to the older "ordinary" questions do not show the impotence of the new ideas, as much as they show the impotence of the old ideas in capturing the vast new lands before us.

3$\begingroup$ Joel, regarding your controversial counterpoint, if I said, say, that we should be platonists about countable DC but formalists about stronger forms of choice  would I be doing a fundamental disservice to mathematics? I ask because you talk about "limiting ourselves to the ideas used in `ordinary' mathematics", which sounds like someone wants to somehow forbid nonordinary mathematics. Maybe there are such people, but it sounds like a pretty fringe position. $\endgroup$ Aug 11 at 17:10

5$\begingroup$ ... I was once accused by Harvey Friedman of wanting to "BAN" (his all caps) some mathematical fields. When I pressed him to indicate where I had ever said that, his response was something to the effect of "by saying that certain kinds of math lack a clear philosophical justification, and therefore we should be formalists about them, I was discouraging people from pursuing those directions, and, in effect, attempting to BAN them". So I have become sensitized to words like "limiting" which seem a little strawmanish. $\endgroup$ Aug 11 at 17:14

1

4$\begingroup$ By the way, much the same discussion can be had about excluded middle and constructive mathematics, which is not just frugal, it's downright ascetic. The old school proceeded from philosophical positions, but I would say the new generation, especially people close to computer science, are in the first place pragmatic (although still speak fanatically at times). Personally, I am just fascinated by how rich mathematics gets once we drop excluded middle – one can get all sorts of things that are classically unthinkable. $\endgroup$ Aug 13 at 17:50

3$\begingroup$ I don't mean to place myself in any camp, but when I was referring to the RH possibly lacking a "definite truth value" I meant in the sense of, say, S. Feferman's paper "Is the Continuum Hypothesis a definite mathematical problem?" (Incidentally, I think CH is a good example showing how the kind of evidence I mentioned above  namely, the work of Gödel and Cohen  could convince someone that a proposition they previously have thought of as a perfectly "normal" mathematical statement might lack a truth value.) $\endgroup$ Aug 13 at 18:16
It depends on what you mean by "ordinary" mathematics. The reverse mathematics school has shown that you can do virtually all, arguably entirely all, of what is usually meant by "ordinary" using only countable dependent choice.
You can say things like "Tychonoff's theorem requires the full axiom of choice", but actual uses of Tychonoff's theorem in mainstream, non settheoretic fields rarely need more than countable products. I'm not aware of any applications that require Tychonoff for uncountable products that I would consider "ordinary" mathematics. I don't think I've ever used the HahnBanach theorem on a nonseparable Banach space, and on separable Banach spaces it doesn't require any choice. Nor have I ever used Alaoglu's theorem in the dual of a nonseparable space. So from my point of view all essential uses of forms of choice stronger than countable DC are somewhat exotic.

3$\begingroup$ We use much more AC than (countable) DC in commutative algebra and algebraic geometry. Many important rings, especially those have something to do with analytic geometry, such as valuation rings, are nonNoetherian. $\endgroup$– Z. MAug 11 at 3:43

5$\begingroup$ @Z.M Can you elaborate on your comment? Just because one is studying nonNoetherian rings doesn't automatically mean that AC is needed. $\endgroup$ Aug 11 at 11:12

2$\begingroup$ @newaccount Some uses of ultrafilters could "in principle" be eliminated by generically adjoining a suitable ultrafilter to the universe, proving the desired theorem in that forcing extension, and then returning to the original universe by some absoluteness result. Of course you might need a set theorist to design a notion of forcing to produce your "suitable" ultrafilter. $\endgroup$ Aug 11 at 18:23

1$\begingroup$ @TimothyChow There are many situations where AC (or at least, the ultrafilter lemma) is necessary for the current framework to work. For example, Krull's existence of maximal ideals needs the full generality of AC for nonNoetherian rings. We also need the abundance of valuation rings (and that they are stable under ultraproducts) to work with vtopology and arctopology, where we need at least the ultrafilter lemma. NonNoetherian rings appear naturally: even if you start with a variety, modern techniques such as perfectoid spaces will quickly lead you to nonNoetherians. $\endgroup$– Z. MAug 11 at 18:42

1$\begingroup$ @TimothyChow I do not understand your trick. If I understand correctly, one point is Deligne's completeness theorem (equivalent to the ultrafilter lemma): the Zariski locale (or some valuative locale) has enough points, thus we can reduce to stalks, i.e. local rings (or valuation rings), somehow sort of "stalklocal global principle". I do not mean that AC or the ultrafilter lemma is uneliminable (some partial progress was made by Lombardi–Quitté and so on), but that current mathematics build on them, and it is nontrivial to eliminate. $\endgroup$– Z. MAug 12 at 15:48
Some of the other answers seem to be based on the assumption that in ordinary mathematics, one needs (at least) two separate consequences of the full AC: (1) dependent choice (ADC); and (2) existence of nonprincipal ultrafilters.
As is well known, avoidance of choice as much as possible is motivated by its unintuitive consequences, as detailed here. In this context, some of our recent work suggests that ingredient (2) above may be reducible to (1). Namely, we constructed a conservative extension of ZF+ADC where infinitesimals are found within $\mathbb R$, eschewing any need for nonprincipal ultrafilters (in the sense of conservativity just mentioned). We showed, for example, that the Lebesgue measure admits an infinitesimal construction (via counting measures), and that Peano existence theorem similarly admits an intuitive infinitesimal proof.
It would be interesting to explore other areas of mathematics where ultrafilters are used, to determine whether analogous conservative extensions can be constructed that would enable one to bypass the dependence on the existence of ultrafilters.
The moral one draws from this is that the two goals of the revolution of 1870: (a) elimination of infinitesimals, and (b) increased rigor via formalisation of foundations, are actually entirely unrelated, contrary to much flak in the historical literature. To put it another way, the reason it is so hard to put infinitesimals back into mathematics is because they were taken out to begin with when the foundations were formalized. Notably, one shortcoming of ZF was its failure to formalize the Leibnizian distinction between assignable and inassignable quantities, which had been the source of infinitesimals in analysis for centuries before they were eliminated from the foundations.

2$\begingroup$ One should perhaps mention Nelson's "radically elementary probability theory", which is based on very modest means (as opposed to the treatment not involving infinitesimals). $\endgroup$ Aug 13 at 14:08

1$\begingroup$ @SamSanders, Nelson's REPT turns out to be a subsystem of SCOT, which is conservative over ZF+ADC. $\endgroup$ Aug 13 at 14:11

$\begingroup$ Ultrafilters and ultraproducts appear frequently in algebraic geometry, cf. §3.2 of Bhatt–Mathew. $\endgroup$– Z. MAug 13 at 22:06

$\begingroup$ @Z.M : I tried reading BhattMathew but found the terminology rather inaccessible. Could you perhaps point out a basic problem in algebraic geometry that is usually solved using ultraproducts, without using hifalutin' language? I could then try to check whether this can also be done without ultrafilters along the lines of Blass's comment. $\endgroup$ Aug 15 at 13:35

1$\begingroup$ I am not technically equipped to extract a concrete "basic" problem, but if I understand correctly, it is basically used to reduce general rings to valuation rings (e.g. ultraproducts of valuation rings are still valuation rings). It is analogous to reducing general manifolds to open subsets of $\mathbb R^d$ in differential geometry. Hansen–Scholze gives a construction of perverse $t$structure using these techniques. $\endgroup$– Z. MAug 15 at 16:07
Each of the following is, at the very least, convenient for usual mathematics, but probably to a large extent unnecessary.
Countable/dependent choice. With them analysis and measure theory can be developed smoothly. But actually most of analysis is essentially countable, and can be done in fragments of secondorder arithmetic, as is shown by results in reverse mathematics. See for example Timothy's link.
Existence of nonprincipal ultrafilters. This is sometimes useful in functional analysis and geometric group theory where people take ultraproducts of metric spaces. Again, if you analyze the proof closely, you can probably eliminate the use of ultrafilter. In fact reverse mathematicians have proved that ultrafilters are indeed unnecessary in many cases: there was work by Kreuzer showing that roughly speaking, for a significant class of statements in secondorder arithmetic, if you can prove them with ultrafilters then you can prove them without ultrafilters; then Montalban and Shore showed that you can even assume the ultrafilters have extra nice properties.
Zorn's lemma. Of course this is equivalent to choice under $\mathsf{ZF}$, but I have in mind the usual applications like existence of enough prime/maximal ideals. According to nLab such uses can sometimes be eliminated by considering the entire partial order, or the collection of all chains, etc. Even if a working algebraic geometer wants to use Zorn's lemma for convenience, they don't need it to prove something like "$\mathbb{C}_p$ and $\mathbb{C}$ are isomorphic as fields". However, I'm quite ignorant in algebra and I don't really know which fields do people want to have algebraic closures of.
To summarize, countable/dependent choice, ultrafilters and Zorn's lemma are not strictly necessary, but nevertheless convenient, for usual mathematics. And $\mathsf{AC}$ happens to imply all three of them, and hence itself convenient. Moreover $\mathsf{AC}$ arguably seems more obvious than Zorn's lemma. I think that makes a good case for accepting $\mathsf{AC}$ as an axiom, instead of the conjunction of countable/dependent choice, existence of nonprincipal ultrafilters and whatever instances of Zorn's lemma an algebraic geometer needs. Of course if you feel adventurous, you are welcome to prove everything (like FLT) in $\mathrm{EFA}$ to test Friedman's grand conjecture.