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.