  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. The
conclusion extends 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.
