Axiom of non-choice

Last updated April 23, 2023

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$ .

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 is inconsistent. Adoption of the first two characterizes common classical higher order theories, adoption of the latter 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

Related Research Articles

In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that a Cartesian product of a collection of non-empty sets is non-empty. Informally put, the axiom of choice says that given any collection of sets, each containing at least one element, it is possible to construct a new set by arbitrarily choosing one element from each set, even if the collection is infinite. Formally, it states that for every indexed family $of nonempty sets, there exists an indexed set such that for every . The axiom of choice was formulated in 1904 by Ernst Zermelo in order to formalize his proof of the well-ordering theorem.$

In mathematical logic, Russell's paradox is a set-theoretic paradox published by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains an unrestricted comprehension principle leads to contradictions. The paradox had already been discovered independently in 1899 by the German mathematician Ernst Zermelo. However, Zermelo did not publish the idea, which remained known only to David Hilbert, Edmund Husserl, and other academics at the University of Göttingen. At the end of the 1890s, Georg Cantor – considered the founder of modern set theory – had already realized that his theory would lead to a contradiction, as he told Hilbert and Richard Dedekind by letter.

In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.

In mathematics, two sets or classes A and B are equinumerous if there exists a one-to-one correspondence (or bijection) between them, that is, if there exists a function from A to B such that for every element y of B, there is exactly one element x of A with f(x) = y. Equinumerous sets are said to have the same cardinality (number of elements). The study of cardinality is often called equinumerosity (equalness-of-number). The terms equipollence (equalness-of-strength) and equipotence (equalness-of-power) are sometimes used instead.

In mathematics, the axiom of dependent choice, denoted by $, is a weak form of the axiom of choice that is still sufficient to develop most of real analysis. It was introduced by Paul Bernays in a 1942 article that explores which set-theoretic axioms are needed to develop analysis.$

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name. Much of this entry discusses NF with urelements (NFU), an important variant of NF due to Jensen and clarified by Holmes. In 1940 and in a revision in 1951, Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included proper classes as well as sets.

In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005).

In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory. Similarly, a non-conservative extension is a supertheory which is not conservative, and can prove more theorems than the original.

In set theory, $-induction$ , also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.

In mathematical logic, Heyting arithmetic $is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.$

In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with " $" and " " of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.$

<span class="mw-page-title-main">Axiom of limitation of size</span>

In set theory, the axiom of limitation of size was proposed by John von Neumann in his 1925 axiom system for sets and classes. It formalizes the limitation of size principle, which avoids the paradoxes encountered in earlier formulations of set theory by recognizing that some classes are too big to be sets. Von Neumann realized that the paradoxes are caused by permitting these big classes to be members of a class. A class that is a member of a class is a set; a class that is not a set is a proper class. Every class is a subclass of V, the class of all sets. The axiom of limitation of size says that a class is a set if and only if it is smaller than V—that is, there is no function mapping it onto V. Usually, this axiom is stated in the equivalent form: A class is a proper class if and only if there is a function that maps it onto V.

<span class="mw-page-title-main">Markov's principle</span>

Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below.

In constructive mathematics, Church's thesis $is an axiom stating that all total functions are computable functions.$

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ₀ separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo–Fraenkel set theory. This name Δ₀ stems from the Lévy hierarchy, in analogy with the arithmetic hierarchy.

References

↑ Myhill, John. "Constructive Set Theory." The Journal of Symbolic Logic 40, no. 3 (1975): 347-82. Accessed May 21, 2021. doi:10.2307/2272159.

External links

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

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Myhill, John. "Constructive Set Theory." The Journal of Symbolic Logic 40, no. 3 (1975): 347-82. Accessed May 21, 2021. doi:10.2307/2272159.

[1]