What’s ‘Function’ in Axiom of Choice?

Question

In ZF Axiom a function is defined by a formula $\phi$ i.e. $x \in A \leftrightarrow \phi (x)$. But what is the function in AC. Is it a particular set or a undefined notion like set, membership and equality in ZF Axiom

Answer 1

The choice function that the Axiom of Choice says exists is a function like any other function: (usually) a set of ordered pairs. The fact that we usually call it a "choice function" just reflects that it can't be any function, it has to fulfill certain requirements with regards to what its domain and codomain are, and how the function relates the two.

Answer 2

In set-theory for any set $A$ we define: $$\mathsf{Dom}A:=\{x\mid\exists y\; \langle x,y\rangle\in A\}\text{ and }\mathsf{Ran}A:=\{y\mid\exists x\; \langle x,y\rangle\in A\}$$

A set $R$ is a relation if all its elements are ordered pairs.

A set $f$ is a function if it is a relation with the following property:

$$\forall x\in\mathsf{Dom}f\;\exists!y\in\mathsf{Ran}(f)\;\langle x,y\rangle\in f$$

The uniqueness of $y$ invites us to write $y=f(x)$ in this context.

The axiom of choice states that for any set $X$ satisfying $\varnothing\notin X$a function $f$ exists with: $$\mathsf{Dom}(f)=X\text{ and }\forall x\in X\;f(x)\in x$$

A function $f$ with these properties is a so-called choice function.

So $\mathbf{AC}$ in words is: "For every set that only has non-empty elements a choice function exists".

Answer 3

Your mistake lies in the claim that functions are "defined by a formula". That is not true any more than it is true that every function on the real numbers is defined by a formula.

Functions are sets with certain properties. Once we decide on a way to encode functions as sets (e.g. sets of ordered pairs with a certain property, and also how we encode ordered pairs), then saying that "a function exists" is no different than saying that anything else exists. It simply means that there is a set with the property that it is a function.

So when we say that a choice function "exists", we simply mean that there is a set with certain properties that encodes a function, which itself has certain properties (that it satisfies the definition of a choice function).