Let $``\mathcal T x. \phi"$stands for the totality of all objects $x$ satisfying $\phi$. So it is a term of the language as long as $\phi$ has $x$ free and never occur as bound. It cannot be quantified upon, so $\exists \mathcal Tx. \phi, \forall \mathcal Tx. \phi$ are not expressions of the language. Also existential generalization doesn't hold over $\mathcal T$ terms, so we do NOT generally have $(\vdash \phi(\mathcal Ty.\phi)) \implies \vdash \exists x \, (\phi(x))$. Accordingly universal instantiation does not work as well, so we also do NOT generally have: $(\vdash \forall x (\phi(x))) \implies \vdash \phi(\mathcal Ty. \phi)$. Consider the $\mathcal T$ terms to be objects of a sort other than that of the quantified objects (sets). Other than these two exceptions, all the rest of rules of first order logic with equality are maintanied.
Axioms:
- Sets: $\forall x \, ( x= \mathcal T y. (y \in x))$
Sets are totalities of their elements.
- Extensionality: $\mathcal Tx. \phi = \mathcal Tx. \varphi \iff \forall x (\phi \Leftrightarrow \varphi)$
Totalities of objects satisfying equivalent formulas are identical.
- Comprhension: $\forall y \, (y \in \mathcal Tx.\phi \iff \phi(y|x))$;
if $y$ does not occur in $\phi$, $x$ only occurs free in $\phi$, and $\phi(y|x)$ obtained by replacing all occurrences $x$ in $\phi$ by $y$.
An object is an element of the totality of objects satisfying some formula, if and only if, it satisfies that formula.
- Subsets: $\forall a \, \exists b \, (\cal Tx. (x\in a \land \phi)=b) $
The totality of all elements of a set satisfying a formula, is a set.
Define $``V_\alpha"$ recusively along the usual lines.
- Hierarchy: $\forall x \exists \alpha (\lim \, \alpha \land x \in V_\alpha)$
Every set is an element of some stage of the cumulative hierarchy indexed by a limit ordinal.
- Size: $\forall \alpha \, ( \bigcup \mathcal Tx. (x=f(\beta) \land \beta \in \alpha) \neq \mathcal Tx. \top )$
Where $\top$ is any true sentence; and $\bigcup \mathcal Tx. \phi = \mathcal Ty. \exists x \, (\phi(x) \land y \in x ) $
The universe is not the union of the image of a set under some function.
- Choice: $\forall x \, \exists \text { ordinal } \alpha \, \exists f: x \hookrightarrow \alpha$
Where $``\hookrightarrow"$ signify "injective function".
Every set is injective to some ordinal.
Can this theory prove all axioms of $\sf ZFC$?
The question is in particular about if this theory can prove all instances of Replacement? Since the other axioms of $\sf ZFC$ are easily provable in this theory.