Is this simple class theory equi-interpretable with ZFC?

Question

The question here is about the consistency of a rather very simply presented theory and if it is equivalent to ZFC.

The theory is a first order theory of classes, so it has its primitives being equality and membership, with a new primitive one place predicate added that is "set" to denote "..is a set". Now the axioms are those of Extensionality written exactly as in ZFC. An axiom stating that every class is a set if and only if it is a class of sets. A comprehension axiom schema stating that whenever a formula holds strictly of sets without using the predicate "set", then it defines a set. The last axiom is that of infinity stating that every natural number is a set, where natural number is defined in the customary way as a finite von Neumann ordinal.

FORMAL EXPOSITION

To the language of set theory (first order logic with equality and membership) add a primitive one place predicate symbol $``set"$, denoting "is a set".

Axioms:

Extensionality: $\forall x \forall y [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$

Sethood: $\forall x [set(x) \leftrightarrow \forall y \in x (set(y))]$

Comprehension: if $\phi$ is a formula in the langauge of set theory (i.e. doesn't use the symbol $``set"$), in which the symbol $``x"$ is not free, then all closures of:$$ \forall y (\phi \to set(y)) \to \exists x \forall y \ (y \in x \leftrightarrow \phi)$$; are axioms.

Infinity: $\forall n \ [natural(n) \to set(n)]$

Where $natural$ is defined as finite von Neumann ordinal, like as "well founded transitive sets of transitive sets, that are successors and every non empty element of them is a successor"

Questions:

1. Is this theory consistent?

2. If it is consistent, is it interpretable in ZFC?

3. If 2, would it interpret ZFC?

This theory [if consistent] does interpret and prove the consistency of Zermelo set theory, over set $V_{\omega+\omega}$. I'd conjecture that it is equi-interpretable with ZFC also?! However, this theory might be inconsistent. Although this theory does prove existence of non-set classes, but it doesn't stipulate comprehension axioms about them. This is deliberately done here as to avoid set theoretic paradoxes since Sethood axiom is more powerful than the two completeness axioms of Ackermann's set theory, and also comprehension is not restricted to set parameters as it is the case with Ackermann's. So this theory is hazardous. It would be nice to see if it is consistent! and also it would be nice to see what its exact strength relative to Ackermann's and ZFC!

Answer 1

This theory is consistent and moreover its consistency strength is below that of ZFC.

Note that if any model of that theory is is necessary illfounded from the outside. To see this, take any $x_0$ that does not satisfy the $set$-predicate (this must exist). Then it has to contain an element $x_0\in x_1$ that does not satisfy the $set$-predicate as well and one can continue the chain indefinatley. This gives us a hint how we can find such a model.

Let us take any $\omega$-wellfounded, yet illfounded model $(M, E)$ of Zermelo Set theory plus the statment "the von-Neumann Hierachy exists (as sets) and exhausts the whole universe". Observe that ZFC proves such models to exist. Let $\operatorname{wfc}(M)$ denote the wellfounded part of $M$, i.e. all sets in $M$ that are not part of an infinite descending $\in$-chain (from the outside). We may assume that $(M, E)$ is solid in the sense that $\operatorname{wfc}(M)$ is transitive and that the $E$-relation agrees with the true $\in$-relation on $\operatorname{wfc}(M)$. I claim that the structure $\mathcal M=(M; E, set)$ satisfies your theory when we interpret $set$ as $\operatorname{wfc}(M)$.

The Extensionality axiom clearly holds true.

The Sethood axiom is true as any element $x_0$ of the illfounded part of $M$ has an element in the illfounded part of $M$, for example the $x_1$ of any infinite descending chain $x_0\ Ǝ\ x_1\ Ǝ\dots$.

The Infinity axiom holds true as we chose $M$ to be $\omega$-wellfounded, i.e. $\omega^M\subseteq\operatorname{wfc}(M)$.

Now finally lets see that your Comprehension scheme holds as well. Suppose $\varphi(y)$ is any $\in$-formula that has the property $$\mathcal M\models\forall y\ \varphi(y)\rightarrow set(y)$$ I claim that there is an ordinal $\alpha\in\operatorname{wfc}(M)$ such that any $y\in M$ satisfying $\varphi$ has $M$-rank $<\alpha$. Suppose not. Let $\delta=\operatorname{Ord}\cap\operatorname{wfc}(M)$. That means that $\{\operatorname{rank}(y)\mid \varphi(y)\}^M$ is contained and unbounded in $\delta$. Hence $\delta$ is definable over $M$ as the union over this class. But this is impossible: There would be an element $x$ of $M$ whose elements are exactly that of $\delta$. Then $x$ is an $M$-ordinal and furthermore it is in the wellfounded part of $M$, hence $x\in\operatorname{Ord}\cap\operatorname{wfc}(M)=\delta$ and so $x E x$, a contradiction. This is one manifestation of the overspill principle. Thus there is such an $\alpha$. But then $$\{y\mid\varphi(y)\}^M=\{y\in V_\alpha\mid \varphi(y)\}^M$$ and the latter class is a set in $M$ by seperation (here we use that our assumption that $V_\alpha$ is a set). Note that even the version of the comprehension scheme with parameters is true here as long as we require the parameters to fulfill the $set$-predicate(EDIT: Actually we dont need this restriction).