SPOT as a conservative extension of Zermelo–Fraenkel

Question

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?

Answer 1

In plain terms, the conservativity of SPOT over ZF means that if a particular statement S in the language of ZF is provable in SPOT, then ZF can already prove S (with a possibly different proof). Note that ZF does not include the axiom of choice.

More formally, the conservativity of SPOT over ZF is a statement about formal proofs; it asserts that for every proof $\pi$ of a statement S from the axioms of SPOT, there is a proof $\pi'$ of S from the axioms of ZF.

A much older conservativity proof was noted by Georg Kreisel in 1956. Kreisel observed (on the basis of Gödel's work on the constructible universe) that if S is an arithmetical statement (i.e., a first order sentence formulated in the usual language of Peano Arithmetic), and S is provable in ZFC + GCH (where ZFC is ZF plus the axiom of choice, and GCH is the general form of the continuum hypothesis) then S is already provable in ZF alone.

So, by Kreisel's observation, if one manages to prove an arithmetical statement (e.g., Goldbach's conjecture) using a "fancy" proof that uses the axiom of choice and/or the continuum hypothesis, there is another "spartan" proof in ZF alone of the same statement. This FOM post of mine provides more detail (and further links).

A vast generalization of Kreisel's observation was proved by Shoenfield in 1961, it is known as the Shoenfield absoluteness theorem, and it is one of the cornerstones of modern set theory.

Answer 2

Ali's answer contains all the required technical explanation. My answer is more "sociological background " in nature:

For various reasons, there have been rather strong negative reactions to Nonstandard Analysis. Bishop and Connes come to mind as good examples, as discussed at length in papers by M. Katz and his co-authors.

By the usual standard of mathematics, the negative responses to Nonstandard Analysis can only be called "fierce" and "highly emotional". To dress up this semi-religious war with intellectual arguments, one often hears that

"Nonstandard Analysis more heavily makes use of the Axiom of Choice (than usual mathematics)."

The point of SPOT is to show that this commonplace is actually false.