# Category talk:Zermelo-Fraenkel Class Theory

ZF Class theory? New one on me. I thought the extension to classes was due to Bernays, Godel and Von Neumann.

Once I'm through with my current exercise I'll see if I can dig out my Bernays and try to make sense of it in ProofWiki context. --prime mover 08:56, 7 August 2012 (UTC)

- I am trying to regularise what is on User talk:Asalmon; cf. also the new Definition:Class (Zermelo-Fraenkel). --Lord_Farin 08:58, 7 August 2012 (UTC)

- Ideally, later on, when NGB class theory is developed as well, all we will have to do is subpage the results on classes with a 'Proof in ZF Class Theory' and a 'Proof in NGB Class Theory'; when results don't hold in some axiom system, we could use 'Disproof in ...'. Finally, I can see some structural light in this uncharted, chaotic realm. --Lord_Farin 09:07, 7 August 2012 (UTC)

Kind of strange to have a class page for ZF, my understanding is that it's an informal concept (not a formal vehicle, as the article says) where classes are essentially predicates, so that $x \in P$ is just short for $P(x)$. So something like a class function $F:V \to V$ is really just a predicate where $F(x)=y$ denotes $F(\{x,y\})$. So you can sort of pretend that classes are objects in ZF but since you can't quantify over predicates, it's just pretend. I feel like this point should be emphasized more in the article with perhaps some examples, and that class theories like Bernays Godel and Morse Kelley should be mentioned as the formal analogs to this, where classes are actually formal vehicles. --TheoLaLeo (talk) 06:14, 22 November 2021 (UTC)