In a [recent article][1], Hrbacek and Katz have shown that it is possible to formulate an axiomatic theory which provides a formalisation of calculus procedures which make use of infinitesimals (known as SPOT, an acronym of its axioms).

Elsewhere I have read that SPOT is conservative over traditional Zermelo-Fraenkel set theory and so does not depend on the axiom of choice or on the existence of ultra-filters.  Can someone explain in terms more suitable for a non-expert what it means for SPOT to be ''conservative'' over ZF, and also why this implies no dependence on the axiom of choice?


  [1]: https://www.sciencedirect.com/science/article/abs/pii/S0168007221000178