Why is ZF favoured over NBG So why is ZF favoured over NBG? Is it historical, but I've read after Gödel's monograph was published, NBG was more prominent. Or is the reason that NBG gets the cold shoulder to do with forcing and all the extra work needed for NBG to handle forcing.  I've only studied forcing in ZF and have just been told that NGB doesn't deal with forcing well, so what are the major reasons why forcing is more work in NBG and how much harder is it in NBG?  As NBG doesn't really offer anything extra (besides being finitely axiomatizable), and as the NBG language can deal with proper classes and to me (and am sure most would agree) that the bulk of the theorems (elementary and advanced) are much more neater in NBG.  It also seems to me that NBG is much more neater to describe most mathematics especially model theory and related branches.  So any feedback greatly appreciated.
 A: You don't need to treat proper classes as objects in order to prove things in set theory.  ZF is simpler, so it's the preferred choice.  (EDIT: I can't speak to whether forcing is somehow simpler or more elegant in NBG, but this is admittedly the first time I've heard that claim.  Either way, a proof in NBG is a proof in ZF, if you follow, so you don't need to say that a particular proof is "an NBG proof".)
To facilitate discussion about things which concern proper classes (such as the class of all ordinals), we can prove in ZF that the objects of a proper class exist and that they have some property, and then discuss the proper class as though it were an object in ZF.  But it is understood that you could make this rigorous without the notion of "proper class" by referring to the property.  We also use facts about proper classes that we can prove in ZF (again, without an actual definition of a class as an object).  NBG just doesn't add anything useful to ZF that we can't abstract into a ZF discussion.
