Ytukyg

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 modelsvarphi_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 function $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 negvarphi_f(bot, dots, bot)$ $ $ (or semantically $f(F,dots,F) = F$)

This axiom implies

• EmptySet $quad$ (choose $n=0$ and $f(langlerangle) = F$; $ langlerangle 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.