In E. Mendelson's book 'Introduction to Mathematical Logic' he develops NBG set theory. I believe it's well-known enough that a description here is not needed. Althought it could not hurt to summarise the main points:
- The objects of NBG are classes and sets are defined as classes which are members of another class,
- NBG is a conservative extension of ZF,
- NBG and ZF are equiconsistent.
When Mendelson formulates the axiom of regularity though he essentially states it as "Every class is well-founded". Why does he not formulate it as "Every set is well-founded"? They seem (unless I am mistaken) to be equivalent in $\mathbf{NBG}+\mathbf{AC}$ but I'm unsure otherwise.
Best Answer
You're right, they are equivalent. Using the axiom of choice (in particular, dependent choice), you can show that the axiom of regularity holds if and only if there are no infinite descending sequences under the $\in$ relation (I can provide a proof if desired). If regularity did not hold for classes, then we would have a sequence of classes $$\ldots x_2\in x_1\in x_0$$ However, by Mendelson's definition of a set, all but $x_0$ are sets, so we have the sequence of sets $$\ldots x_3\in x_2\in x_1$$ which means regularity does not hold for sets. Thus, if all sets are well-founded, then all classes must be well-founded. I'm guessing he formulated the axiom of regularity in terms of classes simply because the axioms are meant to establish the properties of classes, and consequently, sets as well.
Edit: My original claim that the axiom regularity for classes is equivalent to the assertion that there are no infinite descending sequences, while true, does not follow directly from the axiom of dependent choice like I thought since dependent choice only applies to sets. So, here is another argument. (As a bonus, this one does not require any axiom of choice.)
Suppose all sets are well-founded and let $C$ be a nonempty class. Let $x\in C$. If $x\cap C=\emptyset$, then $C$ is well-founded. If $x\cap C\neq\emptyset$, then $TC(x)\cap C\neq\emptyset$ where $TC(x)$ denotes the transitive closure of $x$ (the fact that the transitive closure of $x$ exists and is a set is true in NBG without the axiom of regularity, as can be seen in my proof here). Since $TC(x)\cap C\subset TC(x)$ and $TC(x)$ is a set, so is $TC(x)\cap C$. So by assumption, there exists $y\in TC(x)\cap C$ such that $y\cap TC(x)\cap C=\emptyset$. Assume $z\in y\cap C$. Then, since $z\in y\in TC(x)$ and $TC(x)$ is transitive, $z\in TC(x)$ so that $z\in y\cap TC(x)\cap C$, a contradiction. So, $y\cap C=\emptyset$ and hence, $C$ is well-founded. Thus, all classes are well-founded if and only if all sets are well-founded.