A program for the full axiom of choice
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 depen...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6549/pdf |
| Summary: | 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. |
|---|---|
| ISSN: | 1860-5974 |