Michele Contente: The Axiom of Choice in Constructive Foundations

Invitation pdf

Michele Contente (Scuola Normale Superiore, Pisa):  
The Axiom of Choice in Constructive Foundations

Abstract
The Axiom of Choice (AC) has been much discussed since its first appearance, but nowadays it is accepted as unproblematic, at least in classical mathematics. The early criticisms of AC were focused on its alleged non-constructive character. Results like Diaconescu's Theorem in topos theory or the Goodman–Myhill Theorem in constructive set theory seem to confirm the unacceptability of AC from a constructive point of view. On the other hand, sometimes it is claimed that the axiom is a simple consequence of the intuitionistic reading of logical constants. Per Martin-Löf formalized this insight and was able to give a proof of AC in the context of his Intuitionistic Type Theory. In a subsequent publication, he analyzed the relationship between the type-theoretic AC and the set-theoretic one. The aim of this talk is to reassess Martin-Löf's analysis in the context of a two-level minimalist type theory introduced by Milly Maietti.

The main outcomes of our analysis are the following:

– We discriminate between different versions of AC, thanks to the availability of the distinction between functions and operations.
– We analyze the logical relationships between these different formulations of AC as well as the link with the corresponding choice rules.
– We stress some foundational points related to the status of AC.

Hopefully, the final result will be a more fine-grained analysis of the status of choice principles in constructive mathematics. This is based on joint work with Milly Maietti.