Is the existence of arbitrary definable partial functions bounded by a set equivalent to the axiom of choice?

Question

Is the axiom of choice (125) equivalent to the following axiom (120)? If we take (120) and the companion axioms (180) and (190), can we demote specification (140) and replacement (160) to theorems?

Free variables are represented with uppercase letters. Bound variables are represented with lowercase letters. $\varphi[M := \chi]$ is a capture avoiding substitution replacing the free variable $M$ with $\chi$ in $\varphi$.

Let $P(X)$ be an orthographic abbreviation for the following:

$$ P(X) \iff \forall w \mathop. \exists_{\le 1} v \mathop. \{\{w\}, \{w, v\}\} \in X \tag{110} $$

$P$ holds if and only if $X$ is a set that looks like a partial function and assigns at most one distinct output for every input.

The following candidate for an axiom schema promises us a set that looks like a partial function associated with every well-formed formula $\varphi$.

$$ \exists c \mathop. P(c) \land \\ (\forall x \in A \mathop. (\exists z \mathop. \{x, \{x, z\}\} \in c) \leftrightarrow (\exists y \mathop. \varphi[X:=x, Y:=y])) \land \\ (\forall x \forall y \mathop. \{\{x\},\{x, y\}\} \in c \to \varphi[X:=x, Y := y]) \tag{120} $$

For every set $A$ and well-formed formula $\varphi$, the formula above interprets $\varphi$ as a relation from its free variable $X$ to its free variable $Y$ and arbitrarily picks a partial function $c$ that is compatible with $\varphi$ when $\varphi$ is restricted to the set $A$. In addition, we prevent the resulting set $c$ from simply being empty by requiring it to be defined whenever possible (when thought of as a partial function).

For concreteness, here is the axiom of choice. It promises us a choice function for every set of nonempty sets.

$$ \forall x \mathop. (\varnothing \not\in x \to \exists f : x \to \cup x \mathop. \forall a \in x \mathop. f(a) \in a) \tag{125} $$

---

Here is the axiom schema of specification from Wikipedia

$$ \forall w_1 \cdots w_n \mathop. \forall a \mathop. \exists b \mathop. \forall x \mathop. (x \in b \leftrightarrow (x \in a \land \varphi(x, w_1 \cdots w_n, a))) \tag{130} $$

Here it is rephrased in slightly different notation.

$$ \exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in A \land \varphi[X:=x]) \tag{140} $$

Here's the axiom schema of replacement from Wikipedia

$$ \forall w_1 \cdots w_n \mathop. \forall a \mathop. ((\forall x \in a \mathop. \exists! y \varphi(x, y, w_1\cdots w_n, a)) \to (\exists b \mathop. \forall y \mathop. y \in b \leftrightarrow \exists x \in a \mathop. \varphi(x, y, w_1 \cdots w_n, a))) \tag{150} $$

Here it is rephrased in slightly different notation.

$$ (\forall x \in A \mathop. \exists! y \mathop. \varphi[X:=x, Y := y]) \to (\exists b \mathop. \forall y \mathop. y \in b \leftrightarrow \exists z \in A \mathop. \varphi[X:=z, Y:=y]) \tag{160} $$

In prose, this says that if $\varphi$ looks like a function from $X$ to $Y$ across all the sets, then we can apply it in some sense to a set we already have and get back a new set.

I noticed that both of these axioms promise us the existence of a set that's smaller than or equipotent to the set we started out with, so I wondered whether we can replace these two axiom schemas with a single axiom schema that promises us partial functions and two additional axioms promising us the pseudodomain (set of all places where the partial function is defined) and range of partial functions.

The notation $\{ \cdots \}$ for finite sets can be defined using the axiom of union, the axiom of pairing, and the axiom of extensionality.

$$ \exists c \mathop. \forall x \forall y \mathop. \{\{x\}, \{x, y\}\} \in c \leftrightarrow (x \in A \land \varphi[X := x, Y := y] \land \exists! v \mathop. \varphi[X:=x, Y := v]) \tag{170} $$

This says that given an initial set $A$ and a well-formed formula $\varphi$ thought of as a relation from $X$ to $Y$, we can construct a set that is equivalent to the graph of the partial function from $X$ to $Y$ that's associated with $\varphi$. We construct this mapping by leaving in $\{\{x\}, \{x,y\}\}$ in places where $\varphi$ would be single-valued as a function and removing an edge in cases where $\varphi$ does not send $x$ anywhere or sends $x$ to more than one place.

I'm not sure it's really necessary, but let's also throw in the following axioms so that we can extract the pseudodomain and range of any partial function.

Existence of pseudodomain

$$ \exists c \mathop. \forall x \mathop. x \in c \leftrightarrow (\exists y \mathop. \{\{x\}, \{x, y\}\} \in A) \tag{180} $$

Existence of range

$$ \exists c \mathop. \forall y \mathop. y \in c \leftrightarrow (\exists x \mathop. \{\{x\}, \{x, y\}\} \in A) \tag{190} $$

I claim that (170), (180), and (190) are equivalent to the axiom schemas of specification and replacement. Specification is analogous to applying (170) and taking the pseudodomain. Replacement is analogous to applying (170) and taking the range.

However, when I thought about this some more I noticed that the intuition behind the axiom of choice also gives us sets that are smaller than or equipotent to $A$, the set we started out with.

Then I started wondering whether we could recover choice by removing the $\exists! v \mathop. \varphi[\cdots]$ restriction in (170) and patching up the resulting axiom so that the resulting partial function $c$ makes an arbitrary choice when $\varphi$ is multivalued.

Does the construction (120) work as an equivalent for the axiom of choice? I'm pretty sure that it works, but isn't strong enough to be equivalent to the axiom of global choice because it doesn't give us a new function symbol or choice operator.

Answer 1

Yes, (120) is equivalent to Choice (over ZF), and (120) and (190) (no need for (180)) can be used to prove Separation and Replacement from the other axioms of ZF. The equivalence of (120) and Choice is pretty much trivial. Given a set $A$ of nonempty sets, apply (120) to $A$ and the formula $Y\in X$. This gives a $c$ which for each $x\in X$ contains the ordered pair $(x,y)$ for exactly one $y\in x$. With Separation you can then take the subset of $c$ consisting of only such pairs, and this is a choice function for $A$. Conversely, to prove (120) from Choice, let $B_x=\{y\in A:\varphi(x,y)\}$. Then if $f$ is a choice function for $\{B_x:x\in A\}$, the function $c$ on $A$ defined by $c(x)=f(B_x)$ witnesses (120).

To prove Replacement using (120) and (190), suppose $A$ is a set and $\varphi(x,y)$ is a formula (with parameters) that defines a function; we wish to prove the set $B=\{y:\exists x\in A\;\varphi(x,y)\}$ exists. Let $\varphi'(x,y)$ be the formula $\varphi(x,y)\wedge x\in A$. Applying (120) to $\varphi'$ and $A$, we get a $c$ such that contains the function defined by $\varphi$ on $A$ and no other ordered pairs (our modification of $\varphi$ to $\varphi'$ guarantees that the domain of $c$ can be no larger than $A$). Applying (190) to $c$ we then conclude that $B$ exists. Separation can then be deduced from Replacement. (Or more directly, you can apply (120) to the formula $\varphi$ that defines the identity function on the subset you are trying to construct.)

Let me further remark that if you strengthen (120) to require that every element of $c$ is an ordered pair, then (120) alone suffices to prove all of Separation, Replacement, and Choice (no need form (190)). Indeed, in the case that $\varphi$ actually defines a function whose domain is contained in $A$, this strengthened version of (120) just says that this function exists. In particular, the identity function on any subclass of $A$ exists. But if $f$ is a function, then $\bigcup\bigcup f$ is the union of its domain and its image. Applying this to identity functions on subclasses of sets then proves Separation. Applying it to arbitrary functions defined on sets then says that the union of the domain and image of the function exists, and then you can use Separation to get just the image, proving Replacement.