On the computational content of the Axiom of Choice

Abstract

We present a possible computational content of the negative translation of classical analysis with the Axiom of Choice. Our interpretation seems computationally more direct than the one based on Gödel's Dialectica interpretation [10,18]. Interestingly, this interpretation uses a refinement of the realizibility semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis, and how to interpret the axiom of Dependent Choice and Spector's Double Negation Shift.