infinitesimal analysis w/o AC

[Mikhail Katz]

Dear FoMers,

Karel Hrbacek and I just posted an article at
https://arxiv.org/abs/2009.04980 entitled "Infinitesimal analysis
without the Axiom of Choice" with the following abstract.

"It is often claimed that analysis with infinitesimals requires more
substantial use of the Axiom of Choice than traditional elementary
analysis. The claim is based on the observation that the hyperreals
entail the existence of nonprincipal ultrafilters over N, a strong
version of the Axiom of Choice, while the real numbers can be
constructed in ZF. The axiomatic approach to nonstandard methods
refutes this objection. We formulate a theory SPOT in the
$\st$-$\in$-language which suffices to carry out infinitesimal
arguments, and prove that SPOT is a conservative extension of ZF. Thus
the methods of Calculus with infinitesimals are just as effective as
those of traditional Calculus. This result and conclusion extend to
large parts of ordinary mathematics and beyond. We also develop a
stronger axiomatic system SCOT, conservative over ZF+ADC, which is
suitable for handling such features as an infinitesimal approach to
the Lebesgue measure.  Proofs of the conservativity results combine
and extend the methods of forcing developed by Enayat and Spector."

Historically, the Calculus of Newton and Leibniz was first made
rigorous by Dedekind, Weierstrass and Cantor in the 19th century using
the epsilon-delta approach.  It was eventually axiomatized in the
$\in$-language as ZFC.  After Robinson's development of nonstandard
analysis it was realized that Calculus with infinitesimals also admits
a rigorous formulation, closer to the ideas of Leibniz, Bernoulli,
Euler. and Cauchy.  It can be axiomatized in a set theory using the
$\st$-$\in$-language.  The primitive predicate $\st$ can be thought of
as a formalization of the Leibnizian distinction between assignable
and inassignable quantities.  Such theories are obtained from ZFC by
adding suitable versions of Transfer, Idealization and
Standardization.

Now that it has been established that the infinitesimal methods do not
carry a heavier foundational burden than their traditional
counterparts, one can ask the following question.  Which foundational
framework constitutes a more faithful formalization of the techniques
of the 17-19 century masters?  For all the achievements of Cantor,
Dedekind and Weierstrass in streamlining analysis, built into the
transformation they effected was a failure to provide a theory of
infinitesimals which were the bread and butter of 17-19 century
analysis, until Weierstrass.  By the yardstick of success in
formalization of classical analysis, arguably SPOT, SCOT and other
theories developed in the present text are more successful than ZF and
ZF+ADC.

Mikhail Katz