In Infinitesimal analysis without the Axiom of Choice, 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 in another somewhat related article by Katz 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?