While I was thinking about NBG and MK I had the idea for two alternative axioms. As usual $V$ is the class of sets.
The first one:
For a boolean function $f : \{T,F\}^n \to \{T,F\}$ let $\varphi_f(x_1,\dots,x_n)$ be a formal representation of $f$. That means for $a_1,\dots, a_n \in \{T,F\}$ we have $f(a_1,\dots,a_n) = T \ \Leftrightarrow\ \models\varphi_f(a_1,\dots,a_n)$. (I'm identifying T, F with $\top$, $\bot$). So for example if $f$ is the AND-function we have $\varphi_f = (x_1 \wedge x_n)$.
Axiom 1 (scheme):
For all boolean functions $f : \{T,F\}^n \to \{T,F\}$ and all $R_1, \dots, R_n \in \{=,\in,\subseteq\}$:
For all $b_1,\dots, b_n \in V$ we have
$\{x; \varphi_f(x R_1 b_1, \dots, x R_n b_n)\} \in V \quad \Leftrightarrow \quad \neg\varphi_f(\bot, \dots, \bot)$ $\ $ (or semantically $f(F,\dots,F) = F$)
This axiom implies
- EmptySet $\quad$ (choose $n=0$ and $f(\langle\rangle) = F$; $\ \langle\rangle \in \{T,F\}^0$ is the empty sequence)
- Pairing $\quad$ (choose $n=2$, "$f = AND$" and $R_1,R_2 =\; =$)
- Powerset $\quad$ (choose $n=1$, "$f = $ identity" and $R_1 =\; \subseteq$)
- SmallUnion $\quad$ (choose $n=2$, "$f = OR$" and $R_1, R_2 =\; \in$)
and others... (Let $a \in^2 b :\Leftrightarrow \exists c (a \in c \wedge c \in b)$. If we allow the $R_i$ to be $\in^2$ we have Union too. )
Further: the axiom states that many classes are proper (without the help of other axioms).
And I'm quite sure that this axiom follows from NBG/MK.
If we choose Extensionality, (Foundation), Class Comprehension, Limitation of Size, Infinity and our Axiom 1 we have a version of NBG resp. MK which is easy to remember. What do you think?
The second:
Axiom 2:
If $X$ is a class of non-empty disjoint sets, then $X$ is a set iff there is a choice set for $X$.
(I think the formalisation is clear)
This axiom is a fusion of choice and (at least) a part of replacement. So for example if we have a class function $f: A \to B$ and $A$ is a set that contains no pairs, we could build the class $X = \{ \{x, \langle x, f(x)\rangle\}; x \in A\}$ and use our axiom to conclude that $X$ is a set (since $A$ is obviously a choice set of $X$). With Union and Separation we get that the image of $f$ is a set too.
My first question:
Is Axiom 2 equivalent to choice and replacement (modulo other standard axioms)?
My second question: Are similar axioms studied somewhere?
I found an answer to the first question: Yes
Let $f : A \to B$ be a class function and $A$ a set
(i) If $f$ is injective we define $C := \{a \in A; f(a) \notin A\}$. With separation it is a set. Now we build the class $X = \{ \{a,f(a)\}; a \in C \}$. Since $C$ is a choice set of $X$ (and $X$ is a class of non-empty disjoint sets) we get with Axiom 2 that $X$ is a set. If we have small union, union and separation this implies, that $\operatorname{im} f = f(C) \cup (A \cap \operatorname{im} f)$ is a set.
(ii) Now consider an arbitrary class function $f$. $f$ defines an equivalence relation $a \sim b :\Leftrightarrow f(a) = f(b)$ on $A$. With powerset and separation we get, that the class of equivalence classes $A/{\sim} := \{ [a]_\sim; a \in A\}$ is a set. Since $f_{\sim}: A/{\sim} \to B,\ [a]_{\sim} \mapsto f(a)$ is injective, we can use (i) to show that $\operatorname{im} f = \operatorname{im} f_{\sim}$ is a set.
So Axiom 2 implies replacement.