[btilly]

Yeah, yeah. My comment was my reaction 30 years ago.

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.