In constructive/intuitionistic mathematics, it is common to reject the axiom of choice, because it is highly nonconstructive and implies the law of the excluded middle by Diaconescu's theorem/Bishop's freshman exercise.

However, what about the *double negation* of the axiom of choice? I.e. the statement that any surjective function does *not not* have a section. Or more generally, use of the axiom of choice could be governed by a Tierney operator that does not have to be double negation.

4more comments