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.

  • 2
    $\begingroup$ 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. $\endgroup$ Commented Jun 16 at 16:18


You must log in to answer this question.

Browse other questions tagged .