FOM: ZFC over ZF

[Harvey Friedman]

Reply to Frank  Sat, 19 Feb 2000 04:38, and Kanovei Sat, 19 Feb 00 18:54.

Frank writes:

>>I suspect that ZFC is
>conservative over ZF for formulas of form "there exists a unique x such
>that phi", or for most such formulas--does anyone know of any results like
>this?

Kanovei responds:

>Take, as phi(x), the formula saying:
>"x is the set of all wellorderings of the continuum
>and x is a non-empty set" --
>this will be a counterexample for your thesis.
>Yet a lot of practically interesting formulas are
>really "absolute" w.r.t. the provability in the
>ZF/ZFC pair, by the Sigma^1_2 absoluteness theorem.

It is known from the sixties or possibly early seventies that every Pi-1-4
sentence provable in ZFC is provable in ZF, and this is false for Sigma-1-4
sentences. It then follows that if ZFC proves (therexists unique subset x
of omega)(A(x)) then ZF proves (therexists unique subset x of omega)(A(x)),
if A is Sigma-1-3. But what if A is Pi-1-3? Likely false using Pi-1-2
singleton technology.