Editing Axiom of choice (section)

==In constructive mathematics==

As discussed above, in the classical theory of ZFC, the axiom of choice enables [[nonconstructive proof]]s in which the existence of a type of object is proved without an explicit instance being constructed. In fact, in set theory and [[topos theory]], [[Diaconescu's theorem]] shows that the axiom of choice implies the [[law of excluded middle]]. The principle is thus not available in [[constructive set theory]], where non-classical logic is employed.

The situation is different when the principle is formulated in [[Martin-Löf type theory]]. There and higher-order [[Heyting arithmetic]], the appropriate statement of the axiom of choice is (depending on approach) included as an axiom or provable as a theorem.<ref>[[Per Martin-Löf]], ''[https://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf Intuitionistic type theory]'', 1980.
[[Anne Sjerp Troelstra]], ''Metamathematical investigation of intuitionistic arithmetic and analysis'', Springer, 1973.</ref> A cause for this difference is that the axiom of choice in type theory does not have the [[extensionality]] properties that the axiom of choice in constructive set theory does.<ref>{{cite journal | last1 = Martin-Löf | first1 = Per | author-link = Per Martin-Löf | year = 2006 | title = 100 Years of Zermelo's Axiom of Choice: What was the Problem with It? | journal = The Computer Journal | volume = 49 | issue = 3| pages = 345–350 | doi = 10.1093/comjnl/bxh162 | bibcode = 1980CompJ..23..262L }}</ref> The type theoretical context is discussed further below.

Different choice principles have been thoroughly studied in the constructive contexts and the principles' status varies between different school and varieties of the constructive mathematics.
Some results in constructive set theory use the [[axiom of countable choice]] or the [[axiom of dependent choice]], which do not imply the law of the excluded middle. [[Errett Bishop]], who is notable for developing a framework for constructive analysis, argued that an axiom of choice was constructively acceptable, saying

{{blockquote|A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence.<ref>[[Errett Bishop]] and [[Douglas S. Bridges]], ''Constructive analysis'', Springer-Verlag, 1985.</ref>}}

Although the axiom of countable choice in particular is commonly used in constructive mathematics, its use has also been questioned.<ref>Fred Richman, "Constructive mathematics without choice", in: Reuniting the Antipodes—Constructive and Nonstandard Views of the Continuum (P. Schuster et al., eds), Synthèse Library 306, 199–205, Kluwer Academic Publishers, Amsterdam, 2001.</ref>