*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$"We introduce explicit definitions:

$X \in Y$ for "$X$ is an element of $Y$"

$\mathsf{Class}(X)$ for "$X$ is a class"

$\mathsf{Memb}(X)$ is short for $\exists Y(X \in Y)$.In quantifiers, it's convenient to use somewhat type-theoretic looking abbreviations:

$\mathsf{Set}(X)$ is short for $\mathsf{Class}(X) \wedge \mathsf{Memb}(X)$.

$\mathsf{Atom}(X)$ is short for $\neg \mathsf{Class}(X) \wedge \mathsf{Memb}(X)$.

$X \equiv Y$ is short for $\forall Z(Z \in X \leftrightarrow Z \in Y)$.

$X : \mathsf{Class}$ for $\mathsf{Class}(X)$.For quantification over

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

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

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

$\forall x \phi(x)$ is short for $(\forall X : \mathsf{Memb}) \phi(X))$Then the axioms look a bit prettier:

These are impredicative class comprehension (restricted toAxioms of$\mathsf{ASC}$:

(COMP) $\hspace{10mm}$ $(\exists X: \mathsf{Class})\forall y(y \in X \leftrightarrow \phi(y)).$

(EXT) $\hspace{13mm}$ $(\forall X : \mathsf{Class})(\forall Y : \mathsf{Class})

(X \equiv Y \to X = Y).$

(ATOM) $\hspace{10mm}$ $(\forall X: \mathsf{Atom})\forall Y(Y \notin X).$

*members*), extensionality (restricted to

*classes*) and an axiom saying that atoms are empty. One may write down

*any*formula $\phi(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.

## No comments:

## Post a Comment