Calculus Made Easy by Silvanus P. Thompson (1910)

The good news is that we don't!

Only model-theoretic approaches, which justify the infinitesimal methods by constructing a hyperreal field, require (a weak form of) the axiom of choice [2].

However, there are axioms for nonstandard analysis which are conservative over the usual choice-free set theory ZF. The three axioms of Hrbacek and Katz presented in the article "Infinitesimal analysis without the Axiom of Choice" [1] are the best recent example: these axioms allow you to do everything that is done in Keisler's book and more (including defining the derivative), and you never need to invoke the axiom of choice to justify them.

[1] https://arxiv.org/abs/2009.04980

[2] Essentially, the set of properties satisfied by a fixed nonstandard hypernatural gives rise to a non-principal ultrafilter over the naturals. The axiom of choice is necessary to prove the existence of non-principal ultrafilters in (choice-free) set theory, but the existence of non-principal ultrafilters is not sufficient to prove the axiom of choice.

_Make: Calculus: Build models to learn, visualize, and explore_ by Joan Horvath and Rich Cameron

https://www.goodreads.com/book/show/61739368-make

It's part of a series with matching books on Geometry and Trigonometry.

I find it a mildly interesting intellectual exercise that you can do NSA with weaker axioms than choice. But for all cases I care about, I can already prove it with NSA without ANY additional axioms!

How is this possible? From Shoenfield's absoluteness theorem, you can prove that all statements that an be made in the Peano Axioms that can be proven in ZFC, are also true in ZF. (Note, they must be statable in PA, but not necessarily provable there.) But PA can encode any statement we can make about computation. So take any calculation we can talk about that can be approximated on a computer. We can rewrite it in PA. We can prove it using NSA. We then know that it is true in ZF. And we know that it is true without any additional axioms beyond ZF!

That which we can actually calculate in any useful way can all be calculated on a computer. And therefore NSA can prove anything about Calculus that I care about without needing any axiom beyond ZF.

But in the end this is using a mathematical sledgehammer to drive in a thumb tack. Many approaches to Calculus do not require assertions about the existence of sets that we cannot construct, even in principle. Even though I understand how NSA works, I'd prefer to use any of those.