[FOM] Uses of Replacement

[ali enayat]

In his posting of Feb 23, 2006, Friedman presented a number of significant 
examples of various results whose proofs heavily rely on Replacement.

Freidman concluded his posting with the following query:

>SUBSCRIBERS - do you know other examples where the uses of replacement 
>mayor may not be >necessary?

This prompted me to discuss the role of Replacement in the known proofs of 
the conservativity of ZF+GC (global choice) over ZFC.

It is known that every countable model M of ZFC can be expanded to a model 
(M,f), such that:

(1) f is a global choice function, i.e., for all nonempty x, f(x) is a 
member of x.
(2) (M,f) satisfies Replacement in the extended language {epsilon, f}.

This result was independently proved via a forcing argument by a number of 
people including Cohen, Solovay, Jensen, Kripke, and Felgner (whose proof 
was published in [Fund. Math., 1971]).

The conservativity of ZFGC over ZFC was also established by Gaifman without 
using forcing in [Israel J. Math, 1975]. However, both the forcing proof and 
Gaifman's proof rely on Replacement (in the forcing proof,  Replacement is 
invoked indirectly in the guise of the reflection theorem).

This raises the following apparently open foundational question regarding 
Replacement:

Question: Is Z + GC [Zermelo Set theory plus global choice] conservative 
over ZC [Zermelo set theory with local choice]?


Regards,

Ali Enayat