5
$\begingroup$

Amongst different foundations of mathematics, $ZF$ and $NF$ are talking about "sets" but $MK$ and $GB$ are talking about two sorts of objects "sets" and "classes".

What are benefits of studying the axiomatic systems with more than one sort of objects even if they are conservative relative to $ZF$? Is it just because theorems about proper classes have simpler forms in such systems in comparison with corresponding theorem schemas in $ZF$ or it is because we lose some useful information and power of the theorems on proper classes when we reduce them to $ZF$? If the last is true, what are the examples of such harmful reductions? Does the same phenomenon happen for sets as same as proper classes too? In the other words, do $GB$ or $MK$ in some sense tell us "more" about sets and proper classes than $ZF$?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

The premise of the question seems undercut by the fact that both GB and MK have formulations solely in terms of classes, that is, in terms of only one kind of object. In these formulations, one can define the sets simply to be those classes that are $\in$-related to another object.

Some set theorists finds these single-object-type presentations to be more elegant, but many other set theorists prefer the two-sorted presentations, simply because they are more naturally related to and extend the ZFC account.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ On the other hand one may view stratifications as in NF as introducing an infinite sequence of kinds of objects... This "arbitrariness" of one-manysortedness manifests itself most clearly in category-theoretic approach to type theory via the notion of idempotent splitting: one may turn a category with one object (a monoid) into one with several objects by declaring objects/types to be idempotents of the monoid. I believe this approach was first used by Scott in his "Data types as lattices" where he used it to model behavior of types in programming languages via his $\wp_\omega$ $\endgroup$
    – მამუკა ჯიბლაძე
    Feb 25, 2014 at 6:09
  • $\begingroup$ The point is that although these categories are not equivalent, their "sets" (i. e. set-valued functors on them) form equivalent categories $\endgroup$
    – მამუკა ჯიბლაძე
    Feb 25, 2014 at 6:11
  • $\begingroup$ One more thing - the gains/losses of one/many types approach are well illustrated by the drastic distinction between untyped and typed $\lambda$-calculus $\endgroup$
    – მამუკა ჯიბლაძე
    Feb 25, 2014 at 6:12
6
$\begingroup$

I would like to address the part of the question about whether allowing classes beyond those that are definable over the model adds to our understanding of the properties of sets/classes. For instance, the famous Kunen inconsistency showing that there cannot be an elementary embedding $j:V\to M$ is nearly trivial to prove if we assume that $j$ is definable. Kunen's sophisticated argument is required to show that there cannot be such a class embedding in any model of ${\rm GBC}$. The existence of classes beyond those that are definable can also be useful in model theoretic ultrapower constructions. If $M$ is a (set) model of ${\rm GBC}$, we can construct ultrapowers of $M$ by using an ultrafilter on its proper classes. In particular, this method allows us to build end-extensions of models of set theory. By controlling what types of classes exist in $M$, we can obtain end extensions with different desired properties.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.