# SPOT as a conservative extension of Zermelo–Fraenkel

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?

• OK this helps slightly, but set theory and logic are not my subjects so this contains a lot of jargon for me. Aug 4, 2021 at 11:51

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.

• Further similar extensions appear in MR0256872 (41 #1528) Platek, Richard A. Eliminating the continuum hypothesis. J. Symbolic Logic 34 (1969), 219–225. Notably, if a projective statement about the reals is provable using CH, then it is provable without this assumption. Aug 5, 2021 at 21:13
• @AndrésE.Caicedo Yes indeed, the (transitive closure) of the FOM link included in my answer includes a link that briefly discusses Platek's result; see cs.nyu.edu/pipermail/fom/2013-April/017209.html Aug 6, 2021 at 17:18
• Here's a direct link for Platek's paper in JSL: doi.org/10.2307/2271098 Aug 9, 2021 at 5:16

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.

• I would also describe Bishop's reaction as "grounded in a coherent position far from the mainstream" and "allied with numerical analysis and applied math instead of the pure math of the nonstandard analysts" -- I agree about the fierceness and emotional valence, but I see charitable descriptions too.
– user44143
Aug 6, 2021 at 21:57