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., Golbach'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.

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.

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 Gerog 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., Golbach'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.

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., Golbach'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.