In constructive set theory, the axiom of non-choice[1] is a version of the axiom of choice limiting the choice to just one.
Formal statement
If for each element x of set A there is exactly one y such that a property holds, then there exists a function f with domain A that maps each element x of A to an element f(x) such that the given property holds. Formally, the axiom can be stated as follows:
\( {\displaystyle \forall x\in A\;\exists !y\;\psi (x,y)\;\to \;\exists f\;(\operatorname {Function} (f)\land \operatorname {Domain} (f)=A{\text{ and }}\forall x\in A\;\psi (x,f(x)))} \)
Discussion
In ZF (classical Zermelo–Fraenkel set theory without the axiom of choice), this is a theorem derivable from the axiom of replacement.
In intuitionistic Zermelo–Fraenkel set theory, IZF, this statement is derivable from other axioms, since functions are defined as graphs in IZF. In this case f can be defined as \( {\displaystyle f=\{(x,y)\mid \psi (x,y)\}} \) and it follows from the definition that it is actually a function.
The difference from the regular axiom of choice is that the choice of y is unique for each x.
References
Myhill, "Some properties of Intuitionistic Zermelo–Fraenkel set theory", Proceedings of the 1971 Cambridge Summer School in Mathematical Logic (Lecture Notes in Mathematics 337) (1973) pp 206–231
External links
Michael J. Beeson, Foundations of Constructive Mathematics, Springer, 1985
Undergraduate Texts in Mathematics
Graduate Studies in Mathematics
Hellenica World - Scientific Library
Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License
