set-theory – How Strong is This Set Theory?

foundationslo.logicset-theory

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.

Best Answer

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.

Related Question