Can we introduce complements on top of the standard set theory $\text{ZF}$ and have some comprehension axioms about them, like in defining a "small set" as an element of a stage of the Cumulative Hierarchy as:


$\text {Define:} \ \ small (s) \longleftrightarrow \exists f \ \exists d \ (Ord(d) \wedge dom(f)=d \\ \wedge \forall i,a,j,b \ (\langle i,a \rangle \in f \wedge \langle j,b \rangle \in f \to [i=j \leftrightarrow a=b] \wedge [j=i+1 \to b=P(a)]) \ \wedge \forall l (l \in d \wedge \neg \exists k \in d (l=k+1) \to \forall c (\langle l,c \rangle \in f \rightarrow c=\bigcup (\{y| \exists i \in d (i < l \wedge \langle i,y \rangle \in f)\}))) \\ 
\wedge \exists i,v \ (\langle i,v \rangle \in f \wedge s \in v))$


where $``Ord(d)"$ means $d$ is a Von Neumann ordinal, and $``dom(f)"$ means the domain of $f$. 


Now we hold Extensionality over the whole domain of discourse, also we stipulate axioms of Pairing, Union, and Power over the whole domain of discourse. Now the only axioms that needs to be restricted are empty and Infinity to be small sets, and instances of the axiom schema of Replacement, which needs to be applied only to collections having 1-1 correspondence with a small set, i.e. the formula of the replacement would be:


$$[\forall x \ \exists z \ \forall y \ (\phi(x,y) \to y=z)] \to \forall A \ (small (A) \to \exists B \ \forall y \ (y \in x \leftrightarrow \exists x \in A \phi(x,y)))$$


Then we add complements over the whole domain of discourse, i.e.


$$\forall A \exists A' \forall y (y \in A' \leftrightarrow y \not \in A)$$


That appears to be safe, and I think we can even add small set choice to it.


My questions are: 


[1] Are there known attempts in that direction?


[2] Can the above approach be extended, provided that set Union be $$ \forall A \ \exists x \ \big{[}\forall small \ y \ \big{(}y \in x \leftrightarrow \exists z \in A \ (y \in z) \big{)} \wedge \big{(}small(A) \to small(x) \big{)} \big{]}$$ , as to involve not just axiomatizing 'complements', but also to axiomatize existence of any function that is a 1-1 correspondence relation? Formally this is:


If $\phi(r,s)$ is a formula in which only $``r",``s"$ appear free, then:


$$\forall x,y \ [\forall z \big{(}\phi(z,x) \leftrightarrow \phi(z,y) \big{)} \to x=y] \ \to 
 \forall A \ \exists x \ \forall y \ \big{(}y \in x \leftrightarrow \phi(y,A) \big{)} $$


is an axiom. 


[3] can the axiom schema in [2] be strengthened as to allow parameters?



Can we add set complements on top of ZF?
Church’s “Set Theory with a Universal Set” and its variants have complements, with Replacement restricted to sets equinumerous to a well-founded set:


* Alonzo Church 1974a. “Set Theory with a Universal Set,” *Proceedings of the Tarski Symposium, Proceedings of Symposia in Pure Mathematics XXV,* ed. Leon Henkin, American Mathematical Society, ISBN: 978-0821814253, pp. 297-308. (Delivered 24 June 1971.)
* Alonzo Church 1974b. “Notes on a Relative Consistency Proof of Axioms A– K of Church’s Set Theory with a Universal Set,” unpublished lecture notes, Church Archives, box 47, Folder 5.
* Emerson Mitchell 1976. *A Model of Set Theory with a Universal Set,* unpublished Ph.D. thesis, University of Wisconsin at Madison.
* “A Variant of Church’s Set Theory with a Universal Set in which the Singleton Function is a Set” (abridged), in *Logique et Analyse,* Vol 59, No 233 (2016) pp. 81–131, doi:10.2143/LEA.233.0.3149532. The full version is available at the Centre National de Recherches de Logique: <http://www.logic-center.be/Publications/Bibliotheque/SheridanVariantChurch.pdf>.
* “Fixing Frege’s Set Theory,” slides from a talk on Church’s and my set theories with a universal set, delivered remotely at the University of Oxford Mathematical Institute, October 2013, and at the Stanford Mathematics Department, April 2014: <http://www-logic.stanford.edu/seminar/1314/Sheridan_Fixing_Freges_Set_Theory.pdf>.


See also Arnold Oberschelp 1973. *Set Theory over Classes,* Dissertationes Mathematicæ (Rozprawy Mat.) 106. [Mathematical Reviews 42 #8300], but note that the crucial part of the consistency proof in both [Friedrichsdorf 1979] and [Oberschelp 1973] is merely a reference to [Oberschelp 1964a], which uses a significantly different formalism.


More generally (chiefly, but not exclusively, about Quine’s *New Foundations*), see <http://math.boisestate.edu/~holmes/holmes/setbiblio.html>, and also <https://en.wikipedia.org/wiki/Universal_set#Restricted_comprehension>.


