While the language of ZFC set theory does not admit classes, this is not the case for NBG set theory. But the language of NBG does not allow quantification on symbols for classes, and it is known that NBG is conservative on ZFC for sets, meaning that every theorem concerning only sets provable in NBG is also provable in ZFC. But KelleyMorse (KM) set theory allows quantification on symbols for classes, and is known not to be conservative for sets on ZFC. Indeed, the language of KM admits more formulas for classes, so probably more classes, and among them more sets. My question is: "What are examples of theorems on sets provable in KM but not in ZFC set theory?" Gérard Lang

KM proves that for any class $X$, there are class club many cardinals $\delta$ that are fully $X$correct, meaning that $\langle V_\delta,{\in},X\cap V_\delta\rangle\prec\langle V,{\in},X\rangle$ (and furthermore, this elementarity is expressible in KM, unlike GBC or ZFC). The reason is that KM proves that there is a satisfaction class $S$ for $\langle V,{\in},X\rangle$, a truth predicate indicating which formulas are true at which points in this (limited) structure, and we may then apply the reflection theorem to $\langle V,{\in},S\rangle$, to find a club of $\delta$ which are $X$correct. This way of thinking produces many theorems purely about sets that are provable in KM, such as: Theorems. (KM)
Nevertheless, one should not think of the large cardinal strength of KM as being very great, since if $\kappa$ is an inaccessible cardinal, then $\langle V_\kappa,{\in},V_{\kappa+1}\rangle$ satisfies KM, and so we have a comparatively low upper bound on consistency strength. Meanwhile, I don't quite agree with your remarks about the syntactic difference between GBC and KM. One can view them both as formalized in the twosorted language, with variable symbols for sets and variable symbols for classes, and there are exactly the same formulas in the two theories. It is just that GBC does not allow the replacement and separation axioms for formulas using class quantifiers, while KM does allow them. But meanwhile, it is perfectly sensible to speak of GBC proving or refuting formulas that happen to have class quantifiers, or to speak of such formulas being independent of GBC. 

