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 $\mathrm{\exists }Y(X\in Y)$.
$Atom(X)$ is short for $\mathrm{\neg }Cl(X)\wedge Memb(X)$.

Then:

Axioms of $\mathsf{ASC}$:
(COMP) $\mathrm{\exists }X[Cl(X)\wedge \mathrm{\forall }Y(Y\in X\leftrightarrow (Memb(Y)\wedge \varphi (Y))].$
(EXT) $Cl(X)\wedge Cl(Y)\to (\mathrm{\forall }Z(Z\in X\leftrightarrow Z\in Y)\to X=Y).$
(ATOM) $Atom(X)\to \mathrm{\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:

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

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

(COMP) $\mathrm{\exists }X(Cl(X)\wedge \mathrm{\forall }y(y\in X\leftrightarrow \varphi (y)))$.

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

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

with the usual meaning (i.e., the class of all members $x$ such that $\varphi (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$
$C{l}^{\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.