The Axiom of Choice in Constructive Set Theory
The axiom of choice does not have an unambiguous status in constructive mathematics. On the one hand it is said to be an immediate consequence of the constructive interpretation of the quantifiers. Any proof of $\forall x\in a\,\exists y\in b\,\phi(x,y)$ must yield a function $f:a\rightarrow b$ such that $\forall x\in a\,\exists y\in b\,\phi(x,f(x))$. This is certainly the case in Martin-L\"of's intuitionistic theory of types. On the other hand, from the very earliest days, the axiom of choice has been criticised as an excessively non-constructive principle even for classical set theory. Moreover, it has been observed that the full axiom of choice cannot be added to systems of constructive set theory without yielding constructively unacceptable cases of excluded middle. On the other hand, it has been shown by Peter Aczel that constructive set theory has a canonical interpretation in Martin-L\"of's type theory and that this interpretation also validates several choice principles, e.g., the axiom of countable choice and the axiom of dependent choices.
The main aim of my talk will be to draw a line between choice principles that are constructively acceptible and those that are not.