A program for the full axiom of choice

TL;DR

This paper introduces the first explicit program for the full axiom of choice within the framework of classical realizability, bridging a gap between proof theory and practical applications in analysis.

Contribution

It provides the first known program for the full axiom of choice, extending the Curry-Howard correspondence to encompass this fundamental set-theoretic principle.

Findings

First program for the axiom of choice

Bridges proof theory and analysis applications

Extends classical realizability framework

Abstract

The theory of classical realizability is a framework for the Curry-Howard correspondence which enables to associate a program with each proof in Zermelo-Fraenkel set theory. But, almost all the applications of mathematics in physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent choice (DC) or even the (full) axiom of choice (AC). It is therefore important to find explicit programs for these axioms. Various solutions have been found for DC, for instance the lambda-term called "bar recursion" or the instruction "quote" of LISP. We present here the first program for AC.