FOM: Predicativism, GR, ACA_0, Zorn's Lemma

[Kanovei]

>Matthew Frank <mfrank at mathlab13.uchicago.edu>  
>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?

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. 

Vladimir Kanovei