KTH/SU Mathematics Colloquium

05-04-06

Per Martin-Löf, Stockholm University

Zermelo's axiom of choice: what was the problem with it?

An analysis of Zermelo's axiom of choice in constructive type theory reveals that the problem with it is not the existence of the choice function but the extensionality of it, which is not visible in an extensional framework where all functions are by definition extensional.