ASC: Atoms, Sets and Classes.

The following "second-order" axiom system is one I've been thinking about for a couple of years. It is called $\mathsf{ASC}$, which stands for "atoms, sets and classes". In a sense, it is the bottom level of Morse-Kelley class theory with atoms, $\mathsf{MKA}$. A set is defined to be a class which is a member of some class. Specific set existence axioms are then given in the usual second-order way.

The formulation of $\mathsf{ASC}$ is modelled partly on Mendelson's formulation of $\mathsf{NBG}$ set theory in

Mendelson, Introduction to Mathematical Logic, Chapter 4, "Axiomatic Set Theory".

except that (Impredicative) Class Comprehension is assumed as an axiom (scheme). 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$"
$Cl(X)$ for "$X$ is a class"

We introduce explicit definitions:

$Memb(X)$ is short for $\exists Y(X \in Y)$.
$Atom(X)$ is short for $\neg Cl(X) \wedge Memb(X)$.

Then:

Axioms of $\mathsf{ASC}$:
(COMP) $\exists X[Cl(X) \wedge \forall Y(Y \in X \leftrightarrow (Memb(Y) \wedge \phi(Y))].$
(EXT) $Cl(X) \wedge Cl(Y) \to (\forall Z(Z \in X \leftrightarrow Z \in Y) \to X = Y).$
(ATOM) $Atom(X) \to \forall Y(Y \notin X).$

These are restricted class comprehension, extensionality and an axiom saying that atoms are empty:

To simplify notation, one may introduce a new variable sort $x,y,z, \dots$ as follows:

$\forall x \phi(x)$ is short for $\forall X(Memb(X) \to \phi(X))$

So, that comprehension can be re-expressed in the more familiar "second-order" way:

(COMP) $\exists X(Cl(X) \wedge \forall y(y \in X \leftrightarrow \phi(y)))$.

Extensionality allows us to prove the uniqueness of any such class; and so we can form class abstracts:

$\{x \mid \phi(x)\}$

with the usual meaning (i.e., the class of all members $x$ such that $\phi(x)$), whose existence is guaranteed by (COMP).

This "second-order" theory $\mathsf{ASC}$ is very safe: it has 1-element models! For example, let the $L$-interpretation $\mathcal{A}$ be defined by:

$A = \{0\}$
$\in^{\mathcal{A}} = \varnothing$
$Cl^{\mathcal{A}} = \{0\}$

Then:

$\mathcal{A} \models \mathsf{ASC}$

A set is defined to be a class which is a member. That is,

$Set(X)$ is short for $Cl(X) \wedge Memb(X)$

The theory $\mathsf{ASC}$ proves the existence of the class $\varnothing$, but does not prove that $\varnothing$ is a set. Similarly, given $X,Y$, $\mathsf{ASC}$ proves the existence of the class $\{X,Y\}$, but does not prove that $\{X,Y\}$ is a set. One can remedy this with specific set-existence existence axioms, such as:

(Empty) $\varnothing$ is a set.
(Pair) If $x,y$ are members, then $\{x,y\}$ is a set.

And one can then continue to add one's favourite set existence axioms.