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?