Slight Reformulation of ASC

This is a slightly different formulation of the theory of classes and atoms, $\mathsf{ASC}$ ("atoms, sets and classes") that I rather like, because of its generality (it permits urelemente/atoms and has impredicative comprehension) and its minimal restrictions. It is closely related to $\mathsf{MKA}$, Morse-Kelley class theory with atoms.

The official language $L$ of $\mathsf{ASC}$ is a 1-sorted first-order language, with variables

$X,Y,Z,X_1,X_2,\dots$ 

and three primitive predicates:

$X=Y$ for "$X$ is identical to $Y$"
$X\in Y$ for "$X$ is an element of $Y$"
$\mathsf{Class}(X)$ for "$X$ is a class"

We introduce explicit definitions:

$\mathsf{Memb}(X)$ is short for $\mathrm{\exists }Y(X\in Y)$.
$\mathsf{Set}(X)$ is short for $\mathsf{Class}(X)\wedge \mathsf{Memb}(X)$.
$\mathsf{Atom}(X)$ is short for $\mathrm{\neg }\mathsf{Class}(X)\wedge \mathsf{Memb}(X)$.
$X\equiv Y$ is short for $\mathrm{\forall }Z(Z\in X\leftrightarrow Z\in Y)$.

In quantifiers, it's convenient to use somewhat type-theoretic looking abbreviations:

$X:\mathsf{Class}$ for $\mathsf{Class}(X)$.
$X:\mathsf{Memb}$ for $\mathsf{Memb}(X)$.
$X:\mathsf{Atom}$ for $\mathsf{Atom}(X)$.

For quantification over members, one may introduce a new variable sort $x,y,z,\dots$ as follows:

$\mathrm{\forall }x\varphi (x)$ is short for $(\mathrm{\forall }X:\mathsf{Memb})\varphi (X))$

Then the axioms look a bit prettier:

Axioms of $\mathsf{ASC}$:
(COMP) $$ $(\mathrm{\exists }X:\mathsf{Class})\mathrm{\forall }y(y\in X\leftrightarrow \varphi (y)).$
(EXT) $$ $(\mathrm{\forall }X:\mathsf{Class})(\mathrm{\forall }Y:\mathsf{Class})(X\equiv Y\to X=Y).$
(ATOM) $$ $(\mathrm{\forall }X:\mathsf{Atom})\mathrm{\forall }Y(Y\notin X).$

These are impredicative class comprehension (restricted to members), extensionality (restricted to classes) and an axiom saying that atoms are empty. One may write down any formula $\varphi (y)$ for comprehension (with $X$ not free of course!). Consistency of comprehension (COMP) is ensured because the inner quantification only goes over members.

As mentioned before, this "second-order" theory $\mathsf{ASC}$ of classes is very weak. It has 1-element models. More generally, the models are related to power-set Boolean algebras, analogous to how models for $\mathsf{MK}$ can be understood as $\mathcal{P}(V_{\alpha })$, with $\alpha$ inaccessible.