Axiom of non-choice

The axiom of non-choice, also called axiom of unique choice, axiom of function choice or function comprehension principle is a function existence postulate. The difference to the axiom of choice is that in the antecedent, the existence of $y$ is already granted to be unique for each $x$.

The principle is important but as an axiom it is of interest merely for theories that have weak comprehension and the capability to encode functions. This is the case, for example, in some weak constructive set theories or some higher-order arithmetics.

Formal statement

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

$\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 $\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 ${\mathrm {AC} }!$. It may also only be adopted for functions from the naturals to the naturals, then called ${\mathrm {AC} _{00}}!$. When the function values are sequences, it may be called ${\mathrm {AC} _{01}}!$. Set theoretically, the existence of a particular codomain may be part of the formulation.

Discussion

Arithmetic and computability

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

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

$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 ${\mathsf {ZF}}$ does not adopt the axiom of choice.

In intuitionistic Zermelo–Fraenkel set theory ${\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

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

Category theory

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.

Links

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

External links

• Michael J. Beeson, Foundations of Constructive Mathematics, Springer, 1985
• Beeson, Michael J. (1988). "Towards a computation system based on set theory". Theoretical Computer Science. 60 (3): 297–340. doi:10.1016/0304-3975(88)90115-6.