The principle states that for all domains ${\displaystyle A}$ , if for each element ${\displaystyle x\in A}$  there is exactly one ${\displaystyle y}$  such that some property holds, then there exists a function ${\displaystyle f}$  on ${\displaystyle A}$  that maps each element ${\displaystyle x\in A}$  to a ${\displaystyle f(x)}$  such that the given property holds accordingly. Formally, this may be stated as follows:

${\displaystyle \forall x\in A\;\exists !y\;\psi (x,y)\;\to \;\exists f\;{\Big (}\operatorname {Function} (f)\land {\big (}\operatorname {Domain} (f)=A{\big )}\land \forall x\in A\;\psi {\big (}x,f(x){\big )}{\Big )}}$ 

When ${\displaystyle \psi }$  is taken to be any predicate, this is an axiom schema. Restrictions to the complexity of the predicate may be considered, for example only quantifier-free formulas may be allowed.

The axiom may be denoted ${\displaystyle {\mathrm {AC} }!}$ . It may also only be adopted for functions from the naturals to the naturals, then called ${\displaystyle {\mathrm {AC} _{00}}!}$ . When the function values are sequences, it may be called ${\displaystyle {\mathrm {AC} _{01}}!}$ . Set theoretically, the existence of a particular codomain may be part of the formulation.

Arithmetic and computability edit

In arithmetic frameworks, the functions can be taken to be sequences of numbers. If a proof calculus includes the principle of excluded middle, then the notion of function predicate is a liberal one as well, and then the function comprehension principle grants existence of function objects incompatible with the constructive Church's thesis. So this triple of principles (excluded middle, function comprehension, and Church's thesis) is inconsistent. Adoption of the first two characterizes common classical higher order theories, adoption of the last two characterizes strictly recursive mathematics, while not adopting function comprehension may also be relevant in a classical study of computability. Indeed, the countable function comprehension principle need not be validated in computable models of weak, even classical arithmetic theories.

Set theory edit

In set theory, functions are identified with their function graphs. Using set builder notation, a collection of pairs may be characterized,

${\displaystyle f:={\big \{}\langle x,y\rangle \mid x\in A\land \psi (x,y){\big \}}.}$ 

The axiom of replacement in Zermelo–Fraenkel set theory implies that this is actually a set and a function in the above sense. Unique choice is thus a theorem. Note that ${\displaystyle {\mathsf {ZF}}}$  does not adopt the axiom of choice.

In intuitionistic Zermelo–Fraenkel set theory ${\displaystyle {\mathsf {IZF}}}$  and some weaker theories, unique choice is also derivable. As in the case with theories of arithmetic, this then means that certain constructive axioms are strictly constructive (anti-classical) in those theories.

Type theory edit

The axiom may also play a role in type theory, in particular when the theory is modeling a set theory.

Category theory edit

Arrow-theoretic variants of unique choice can fail, for example, in locally Cartesian closed categories with good finite limit and limit properties but with only a weakened notion of a subobject classifier.

• Axiom of choice
• Axiom of countable choice
• Axiom of replacement
• History of the function concept

• Michael J. Beeson, Foundations of Constructive Mathematics, Springer, 1985