The main difference with this formal theory is that it depends in an essential manner on a defined notion of class, set, and set membership ∈ , rather than the usual appraoch of leaving them undefined.
This theory is an extension of Atomic General Extensional Mereology with Bottom AGEM+BottomAGEM+Bottom, by adding a primitive binary relation L standing for labeling, so kLxis read as "k labels x", or can be read as "k is a label of x". The axioms about Labeling are:
Labels: aLx→atom(a)
All labels are atoms
Labeling: aLx∧aLy→x=y
No label labels two distinct objects
Empty: ∀ atom a(∄x(aLx)⟺a=∅)
Where ∅ is the Bottom atom.
There is only one non-labeling atom which is the
Bottom object.
Define: class(x)⟺∀a∀b∀y(aPx∧aLy∧bLy→bPx)class(x)⟺∀a∀b∀y(aPx∧aLy∧bLy→bPx)
A class is a fusion of equivalence totalities of labels under equal labeling
Define: y∈x⟺class(x)∧∃aPx:aLy
An element is what's labeled by an atom of a class.
Define: set(x)⟺class(x)∧∃y:x∈y
A set is a class that is an element of a class.
Define: pure(x)⟺class(x)∧∀aPx∀b∀y(aLy∧bLy→a=b)
A pure class is a class of unique labels.
From the above we get the following aesthetic Lemma:
Lemma: ∀x(pure(x)⟺∀y(yPx⟺y⊆x))
Where y⊆x⟺∀z∈y(z∈x)
That is, pure classes are those whose parts are their subclasses and vice verse.
I call such classes as Lewisian, after David Lewis, who introduced those classes in his Parts of Classes.
Define: pureset(x)⟺pure(x)∧∃!a:aLx
So a pureset is not just a pure class that is a set, in addition to that it must be uniquely labeled! Those I also call as "Lewisian sets".
Reflection: if ϕϕ is a formula of the language of set theory, whose parameters are among w1,..,wnw1,..,wn
n=0,1,2,...∀puresetsw1,..,wn:∀x(ϕ→pure(x))→∀x(ϕ→∃!a:aLx)
Where the langauge of set theory includes formulations only using ∈;= as predicates. (Note that when n=0 , the axiom becomes parameterless).
In English: All predicates definable in the language of set theory from pureset parameters if they only hold of pure classes, then all of those classes are pure sets
The suprising thing to me is that this attempt have a simply stated single schema on top of the axioms of Labeled Mereology, that can interpet all of Ackermann's set theory and therefore interpret ZFC. Simply take Ackermann's mystereous set predicate to be hereditarily pureset and all axioms of his set theory would be go through under that interpretation.
The motivation for this axiom is maximally turning pure classes into pure sets, and thereby constructing a strong buildup that is made from pure sets that enables strong kinds of comprehension over them. Now I'm not sure how much this is justified philosophically, but definitely it inspires strong technical developments in set theory, that enabled having a theory as strong as ZFC, and yet opens the door wide for it to be extended by setting axioms for the rest of kinds of sets.
The point here is that this axiom does depend in an essential manner on the defined notions of sets, classes and their membership; it essentially depends on the internal make-up of sets, I mean in Mereological terms! That is, what they are composed of. So it features Ackermann's sub-world V as the world of the most precious kind of sets, the most pure form that a set can be of, i.e. those sets which were described by Lewis. On the other hand, proper classes are classes that are not Lewisian-sets. This is a tempting explanation of Ackermann's set world.