# Is the naive axiomatization of a sort of classes in ZFC, equiconsistent with ZFC?

Is the following extremely naive axiomatization of ZFC+Classes equiconsistent with ZFC?

If so, can my attempted proof be turned into a correct argument of this fact?

If not, I'm really curious why not. I deliberately chose the axioms so that interaction between the $$S$$ and $$C$$ sorts would be "unidirectional" and our new classes would not give us any new sets or tell us anything interesting about them.

I am working in multi-sorted first-order logic.

Let $$T$$ be the deductive closure of $$\mathsf{ZFC}$$; $$T$$ is a theory in the language with one sort $$S$$ and one relation symbol $$\in : S \times S \to 2$$.

Note that the theory $$T$$ in its axiom schemas is the same as ZFC, formulas in ZFC's comprehension axiom, for example, cannot refer to classes, nor can classes be used as parameters.

I want to, as naively as possible, axiomatize the notion of a class by introducing an additional sort $$C$$ as well as the relations $$=^o : S \times C \to 2$$ and $$\in^o : S \times C \to 2$$. I picked $${}^o$$ as the adornment because it looks cool.

I then insist on class extensionality with the following axiom:

1. $$[\forall x y : C]([\forall z : S](z \in^o x \leftrightarrow z \in^o y) \leftrightarrow x = y)$$

And I insist on sameness between classes and sets (via $$=^o$$) when they are extensionally equal.

1. $$[\forall x : S \forall y : C]([\forall z : S](z \in x \leftrightarrow z \in^o y) \leftrightarrow x =^o y)$$

And I insist on class comprehension with the following axiom schema:

1. $$[\forall \vec{x} \exists z:C \forall w : S](\varphi(\vec{x}, w) \leftrightarrow w \in^o C)$$ with $$\vec{x}$$ among both $$S$$ and $$C$$.

#### Beginnings of a proof attempt.

I have the following idea for an argument based on taking a model of $$ZFC$$ and stapling another sort to it. I'm not sure that it works though. The interaction between the sorts $$S$$ and $$C$$ given the new axioms is very weak, so I am confident that no new theorems are introduced for $$C$$-free sentences, but I don't know how to show it.

Assume that $$\mathsf{ZFC}$$ is consistent.

Let $$M$$ be a non-necessarily-standard model of $$\mathsf{ZFC}$$. I think I can get a standard model using some result, but I don't think I need it.

I will now augment $$M$$ with some additional stuff, namely an interpretation for the sort $$C$$ and the relations that involve it $$\in^o$$ and $$=^o$$. Ordinary $$=$$ is just true equality; I'm not using a weird formalism where $$=$$ is defined as some kind of congruence.

Let $$M'$$ be an expansion of the structure $$M$$.

Let $$C^{M'}$$ be the true powerset of $$M$$, $$2^M$$. It is not a problem if $$M \cap 2^M$$ because I am not insisting that different sorts map to disjoint domains.

Let $$(\in^o)^{M'}$$ hold of $$(x, y)$$ if and only if the interpretation of $$x$$ is an element of the interpretation of $$y$$.

Let $$(=^o)^{M'}$$ hold of $$(x, y)$$ if and only if the set $$\{ z : (z, x) \in (\in)^M \}$$ is equal to the interpretation of $$y$$.

This completes my construction of the augmented model.

Axiom 1 holds because $$C^M$$ is the true powerset of the interpretation of $$S$$. Therefore the notion of true equality lines up with extensional indistinguishability.

Axiom 2 holds because that's how we constructed an interpretation of $$=^o$$.

Axiom schema 3 holds because we used the true powerset of the interpretation of $$S$$, which is a superset of the definable powerset promised to us by the axiom schema.

This $$M'$$ is a model of the extended theory.

If ZFC with naively formalized classes is consistent, then it has a multi-sorted model. By taking a reduct and excising the interpretations for $$C$$, $$=^o$$ and $$\in^o$$, I get a model of ZFC.

• Your argument looks correct to me. In fact, it shows something stronger than equiconsistency, namely that your theory is a conservative extension of ZFC (I.e., that it proves no new theorems in the language of ZFC). This is basically exactly the usual proof that NBG set theory is a conservative extension of ZFC. Commented Jun 16 at 16:18