Is this simple class theory equi-interpretable with ZFC?

he 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!

• 1) You need to give the details of your definition of von Neumann ordinal. 2) You haven't provided any substitute for the axiom of replacement, so $V_{\omega+\omega}$ would be a model of your system. – Rob Arthan Jun 5 at 9:59
• Sorry, I misread your comprehension axiom: it probably is as strong as or stronger than replacement, so you probably shouldn't call it comprehension. – Rob Arthan Jun 5 at 10:08
• @RobArthan, I'll define the von Neumann's. Regarding the second point zermelo set theory does prove induction, and so by induction all elements of finite iterative powers of zero are sets, and so the set of all of them is the set HF of all hereditarily finite sets, by the same argument you get the set of all finite iterative powers of HF, which is a model of Zermelo and of course you clearly get $V_{\omega+\omega}$ being a set by separation. – Zuhair Jun 5 at 10:08
• @RobArthan, well anyway the original comprehension axiom of Naive set theory is indeed stronger than replacement, since its inconsistent. Anyhow I'm not really sure if it is stronger than replacement, since it forbids "set" from being used, so the quantifiers cannot be bounded by the predicate "set", and so this might limit replacements. – Zuhair Jun 5 at 10:12
• I think the most dangerous feature of this theory is that it doesn't limit its parameters to being sets, and I think an inconsistency would lie there! of course this is remediable easily by requiring parameter to be sets. – Zuhair Jun 5 at 10:18