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 is already granted to be unique for each .

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[1] or some higher-order arithmetics.

Formal statement

edit

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

 

When   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  . It may also only be adopted for functions from the naturals to the naturals, then called  . When the function values are sequences, it may be called  . Set theoretically, the existence of a particular codomain may be part of the formulation.

Discussion

edit

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,

 

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   does not adopt the axiom of choice.

In intuitionistic Zermelo–Fraenkel set theory   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.

edit

References

edit
  1. ^ Myhill, John (1975). "Constructive Set Theory". The Journal of Symbolic Logic. 40 (3): 347–382. doi:10.2307/2272159. JSTOR 2272159.
edit
  • 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.