Is there a contradiction hiding in this alternative set theory with 3 axioms?

Let us take as a vocabulary the $\in$ relation (is an element of), and a single unary predicate $C$, where $Cx$ is read "$x$ is constructible" or "$x$ is a constructible set" (I'm making this up, but the term seems appropriate). We may then write down an alterative set theory with three intuitive axioms (one of them an axiom schema):

1. Extensionality: $$\forall X \,\forall X'\;:\; (\forall x\; x \in X \longleftrightarrow x \in X') \to X = X'.$$

(I.e.: Objects with the same elements are equal.)

2. Schema of construction: For any formula $\varphi$ which does not contain C, if $\varphi$ has free variables $x$ and $\overline{y} = (y_1, y_2, \ldots, y_k)$, IF $$\forall \overline{y} \, \forall x \;:\; (Cy_1 \land \cdots \land Cy_k \land \varphi(x,\overline{y})) \to Cx$$ THEN $$\forall \overline{y} \, \exists X \, \forall x \; :\;x \in X \longleftrightarrow \varphi(x,\overline{y}).$$ In other words, if it is possible to deduce that $x$ is constructible from only the fact that $y_i$ are constructible and $\varphi(x,\overline{y})$, then the set $X = \{x \mid \varphi(x,\overline{y})\}$ exists.

3. Constructible sets are those with constructible elements:

$$\forall X \; : \; CX \longleftrightarrow (\forall x \;:\; x \in X \to Cx).$$

It seems to me I can deduce many of the axioms of ZF from these: at least, pairing, union, power set, and specification.* So I am thinking there must be a contradiction lurking somewhere. The question:

(i) Is there an (obvious) contradiction in these three axoims?

For instance, we could try to encode Russell's paradox. It can't translate directly, since if we just assume "$x \in x$", it doesn't follow that $Cx$. And one cannot play tricks with "the set of all constructible sets that don't contain themselves" because $C$ is not allowed in $\varphi$ in the comprehension schema.

However, there does seem to be something fishy going on: in ZFC, well-founded induction is a theorem, and well-founded induction cannot be true here or else we could prove that all sets are constructible (using axiom 3). At that point, (2) reduces to unrestricted comprehension and the theory becomes inconsistent.

I would also like to know:

(ii). Is this theory similar to any existing alternative set theories?

When I wrote down these axioms this afternoon, I was trying to formalize the intuitive justification for the axioms of ZFC, namely, that every axiom constructs bigger sets out of smaller sets which have already been defined.

*For pairing, if $A$ and $B$ are constructible, and $x = A$ or $x = B$ then $x$ is constructible. The other axioms I mentioned (union, power set, and specification) use axiom (3): For union, if $A$ is constructible and $x \in a$, $a \in A$, $x$ is constructible. For power set, if $A$ is constructible and $B \subseteq A$, then every $x \in B$ is constructible so $B$ is constructible. For specification, if $x \in A$ and$\varphi(x)$, and $A$ is constructible, then in particular $x \in A$ so $x$ is constructible.

• What does "constructible" mean here? – DanielWainfleet Nov 1 '17 at 2:09
• @DanielWainfleet You mean intuitively? Intuitively I mean something like "well-founded" -- it is built from "smaller" sets which have already been constructed. – 6005 Nov 1 '17 at 2:18
• Comprehension is usually the name for a different Schema. What you call Comprehension is a modification of the Schema that's usually called Replacement. It would be better if you changed the words. Your Q is, I think. whether it is consistent with ZF that there exists a transitive set or proper class $C=\{x:Cx\}$ that satisfies the relativizations to C of Extensionality and "unlimited Replacement", (transitivity of C is your Axiom (3): Members of C are subsets of C.) – DanielWainfleet Nov 1 '17 at 2:47
• @DanielV $a \land b \to c$ means $(a \land b) \to c$. I thought this was standard but I'll edit to add parens. – 6005 Nov 1 '17 at 19:19
• You may be interested in George Boolos' axiomatization of the iterative conception of sets, published in his well-known (and aptly titled) "The Iterative Conception of Set" (it was reprinted in his Logic, Logic, and Logic). He not only axiomatizes the notion, but shows how to derive most of Z's axioms from it (he also argues that Replacement and Choice are not derivable from this conception). – Nagase Nov 3 '17 at 0:29

You have two problems with $2$. One is the term "does not contain $C$". In the simpleminded approach that you can't have $C$ on the right we can avoid that with a two-step that doesn't reference $C$ directly. Just define some urelement $x$ that is a member of some sets and not of some others. You have two classes of sets, those that include $x$ and those that do not. Now you can reformulate Russell's paradox in two steps going between sets that include $x$ and those that do not.
• I guess that empty set arise from application of ex falso to the hypothesis of axiom $(2)$ – Tancredi Nov 1 '17 at 2:31
• Thanks, Ross. Tancredi is right about the empty set. Can you give more detail about the construction to bypass $C$? So I guess by urelement you might mean an $x$ such that $\lnot Cx$. But I don't follow how we can then get the Russell contradiction. With the finite sentences I'm not sure about that either. Even numbers can get defined in ZFC -- probably as a subset of the naturals by specification, but maybe replacement is necessary first to define addition (not too familiar with this). – 6005 Nov 1 '17 at 9:31