How strong is this set theory?

Question

In the spirit of this related question, consider a set theory with the following axioms:

Axiom of extension: $$ \forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y) $$

Axiom schema of comprehension: $$ \exists x \forall y (y \in x \leftrightarrow (\phi y \land C y)) $$

Axiom of construction: $$ \forall x (\forall y (y \in x \rightarrow C y) \leftrightarrow C x) $$

where $C$ is a new symbol like $\in$ that intuitively represents a kind of "constructibility". Some properties I've deduced are

1. Every hereditarily finite set exists and is constructible (in particular, the empty set $\varnothing$ exists and is constructible, as are all the finite ordinals).

2. The quasi-universal set $U$ with $\phi y \equiv \top$ exists, is constructible, and contains itself.

3. The quasi-Russell set $R$ with $\phi y \equiv y \not\in y$ exists, is not constructible (since that yields the Russell contradiction), and does not contain itself.

4. The quasi-co-Russell set $R^\ast$ with $\phi y \equiv y \in y$ exists and is constructible iff it contains itself, which seems to be independent of the theory.

5. Let $y^+ \equiv y \cup \{y\}$ and let $\textsf{inductive } x \equiv \varnothing \in x \land \forall y (y \in x \rightarrow y^+ \in x)$ denote that a set is inductive. $C \varnothing$ and $C y \rightarrow C y^+$, so $\textsf{inductive } U$.

6. Let $\textsf{natural } x \equiv \forall y (\textsf{inductive } y \rightarrow x \in y)$ denote that a set belongs to every inductive set (i.e. is a natural number). Since $\textsf{inductive } U$, $\textsf{natural } x \rightarrow x \in U$. But $x \in U \rightarrow C x$. Thus $\textsf{natural } x \rightarrow C x$. Instantiate the axiom schema of comprehension with $\phi \equiv \textsf{natural}$. Then $\exists x \forall y (y \in x \leftrightarrow \textsf{natural } y)$. That is, the set of natural numbers $\mathbb{N}$ exists, and moreover is constructible.

My question is this: How strong is this set theory compared to ZFC or other alternative set theories?

Edit: In light of the contradiction pointed out below, one might consider restricting the formulas allowed in the axiom schema of comprehension. For example, we might consider restricting to positive formulas, as in positive set theory.

Edit 2: An interesting alternative system is presented here.

Answer 1

Even if $φ$ is restricted to not use $C$, the theory is inconsistent! Here is the simple 2-line proof.

Let $R$ be such that $∀x\ ( x∈R ⇔ C(x) ∧ x∉x )$ by Comprehension.

Then $C(R)$ by Construction. Thus $R∈R ⇔ R∉R$. Contradiction.

Answer 2

Suppose first that $\phi$ in the comprehension schema is allowed to use the symbol $C$. Then I claim your theory is inconsistent. Indeed, suppose we had a model $M$ of this theory, and let $M'$ be the submodel consisting of the elements of $M$ that satisfy the predicate $C$ in $M$. Then every definable-in-$M'$ family of elements of $M'$ is also definable in $M$ (by a formula that may need $C$ to restrict quantifiers) and therefore, according to comprehension, given by an element $x$ of $M$. By the axiom of construction, $x$ satisfies $C$ in $M$ and is therefore in $M'$. Thus $M'$ satisfies unrestricted comprehension, which is impossible by Russell's paradox.

Now suppose the $\phi$ in comprehension is not allowed to use $C$, so it's a formula in the language of ZF. That causes a problem in the preceding paragraph, because a definable-in-$M'$ family of elements of $M'$ might not be definable in $M$ without using $C$. Specifically, if the definition in $M'$ involved a quantifier, the corresponding definition in $M$ would need to refer to $C$ in order to make the quantification range only over $M'$ and not all of $M$. Fortunately, that doesn't matter, simply because the formula involved in Russell's paradox doesn't contain any quantifiers.

So even with the weaker, $C$-less-$\phi$ version of comprehension, the theory is inconsistent.

Answer 3

Regarding the latter suggestion to restrict $\phi$ to positive formulas. The resulting theory would be consistent relative to positive set theory, but it would be just a redundant re-exposition of a fragment of it. Simply take $C$ to be the predicate of being "equal to itself" i.e.:

$C(x) \leftrightarrow x=x$,

and comprehension would just be positive comprehension, and axiom of construction would be trivially true! Same would apply if for example we've restricted $\phi$ to stratified formulas, we'd only get Quine's New foundations set theory.

Actually that argument would hold for any kind of a theory that has a naive like comprehension axiom with only syntactical restrictions on the defining formula.

I think the only reasonable adjustments to salvage your approach are those you've had with your original theory, the one you raised this theory in connection with, which I think is as strong as $PA$, if you want to strengthen it, you add an axiom of infinity, or even a more risky approach is to add a universal class of all $C$ objects but with changing the bound on parameters in comprehension (the schema of construction) for all of them to be elements of that universal class. But I don't know if those are consistent, and what would be their consistency strength?