Editing Choice function (section)

==Bourbaki tau function==
[[Nicolas Bourbaki]] used [[epsilon calculus]] for their foundations that had a <math> \tau </math> symbol that could be interpreted as choosing an object (if one existed) that satisfies a given proposition. So if <math> P(x) </math> is a predicate, then <math>\tau_{x}(P)</math> is one particular object that satisfies <math>P</math> (if one exists, otherwise it returns an arbitrary object). Hence we may obtain quantifiers from the choice function, for example <math> P( \tau_{x}(P))</math> was equivalent to <math> (\exists x)(P(x))</math>.<ref>{{cite book|last=Bourbaki|first=Nicolas|title=Elements of Mathematics: Theory of Sets|date=1968 |publisher=Hermann |isbn=0-201-00634-0}}</ref>

However, Bourbaki's choice operator is stronger than usual: it's a ''global'' choice operator. That is, it implies the [[axiom of global choice]].<ref>John Harrison, "The Bourbaki View" [http://www.rbjones.com/rbjpub/logic/jrh0105.htm eprint].</ref> Hilbert realized this when introducing epsilon calculus.<ref>"Here, moreover, we come upon a very remarkable circumstance, namely, that all of these transfinite axioms are derivable from a single axiom, one that also contains the core of one of the most attacked axioms in the literature of mathematics, namely, the axiom of choice: <math>A(a)\to A(\varepsilon(A))</math>, where <math>\varepsilon</math> is the transfinite logical choice function." Hilbert (1925), “On the Infinite”, excerpted in Jean van Heijenoort, ''From Frege to Gödel'', p. 382. From [http://ncatlab.org/nlab/show/choice+operator nCatLab].</ref>