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):
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.)
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.
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.