# An axiom combining Choice and replacement

I am just finishing teaching a course in Set Theory, and was thinking about the ZFC axioms, when the following axiom occurred to me:

Axiom: Given a sentence $S$ with free variables among $x,y,A_1,\ldots,A_k$

$\forall X,A_1,\ldots,A_k$:

If

$\forall x\in X, \exists y$ such that $S(x,y,A_1,\ldots,A_k)$

then there exists a function $f$ with domain $X$ such that

$\forall x\in X, S(x,f(x),A_1,\ldots,A_k)$.

(I guess this is really an axiom schema.)

This seems to imply the axiom of choice: Take $k=1$, let $A_1$ be a family of nonempty sets and let $X$ be the indexing set of the family. Let $S$ be the sentence that says that $y$ is in the set indexed by $x$. Then the function guaranteed by the Axiom is a choice function for the family. This also seems to imply the Axiom of Replacement, too, and in fact the new Axiom seems to be equivalent to Replacement plus Choice.

I like the Axiom because it says something I find very intuitive: If you know that for all x there exists a y such that BLAH, you can find a function sending each x to a y such that BLAH.

This is probably not of great importance, but I thought I would ask, in case anyone is aware of an approach that combines the axioms like this.

• A function $f$ as in your schema is said to uniformize the relation $S$. As you say, requiring uniformizing functions for arbitrary definable relations is just equivalent to Replacement + Choice. Things become more interesting, however, if we require $f$ to be nice in some way. For example, descriptive set theory has many theorems saying that a relation of a given complexity can be uniformized by a function of the same complexity. – Miha Habič Apr 20 '16 at 18:49
• Thanks, this is the kind of thing I was curious about. – Nathan Reading Apr 21 '16 at 13:08

Taking the clause $\exists y\;[S(x,y,...)]$ and substituting $S'$ for $S$, where $S'$ is $S\land \forall z\;[S(x,z,...)\implies z=y]$ gives us Replacement.
When $S(x,y,...)$ is $(y\in x)\lor (x=y=\phi)$ we obtain a function $f:X\to \{\phi\}\cup (\cup X)$ such that $\forall x\in X\; (x\ne \phi \implies f(x)\in x)$, which is equivalent to AC.