# Untyped KM set theory

I'm writing a particular computational system that manipulates logical propositional statements. After starting with ZF and playing around and scrounging, I've arrived at roughly the NBG set theory as the foundation of this system, and from there read about KM. For various reasons, this is the foundation I wish to employ.

In most axiomatizations I've found, this is a typed theory: sets and classes are different classes of syntactic object. However, it would be very nice if this were not the case - again for various "practical" reasons. I'd like all terms to be a class (and maybe additionally a set), and not to have to worry - so far as the language goes - about if a term is a set representation or not.

Literally the only thing I could find online about this is a short mention that it is perhaps possible here: Variants of Kelley-Morse set theory | Victoria Gitman.

To proceed, I was planning on defining a Set predicate in the natural (in NBG) way - a class that is a member of another class is a set. Then, the axioms which are the same for sets and classes could be collapsed into a single axiom (for example, set-extensionality and class-extensionality become one axiom if there is only one type), and for the (ZF) axioms that apply only to sets, working the Set predicate directly into their statements to restrict them.

Now, I do not have a lot of background in logic. Is this sort of axiomatization possible/sane? Can someone refer me to some literature where something like this is done/defined, or explain why it might not be a good idea? Are there other semantics for KM where there is no need for type, and if so, what are they?

• Yes, the situation is exactly as you suppose. $KM$ is typed only for heuristic reasons of presentation. We can define the syntax for $KM$ as being only about class objects and whenever we want to make a statement about sets, we just use the definable predicate which picks out classes that are elements of some other class. There is very little current literature on $KM$, but I will try to find a reference for you (unless someone here does it first). – Victoria Gitman Nov 30 '15 at 21:05
• There is just such an axiomatization in "Forcing for the Impredicative Theory of Classes", which the author Rolando Chuaqui credits to Tarski. – Victoria Gitman Nov 30 '15 at 21:15
• Why are we calling this system $KM$ now? For years it has been known either as $MK$ (Morse, Kelley) or $MKM$ Mostowski, Kelley, Morse). – Rob Arthan Nov 30 '15 at 21:34
• Perfect, thanks Victoria! – BadZen Nov 30 '15 at 21:35
• A rather earlier and (to many) rather better known reference for MKM presented without types is in the Appendix to Kelley's book "General Topology" published in 1955. – Rob Arthan Nov 30 '15 at 21:55