A PROGRAM FOR THE FULL AXIOM OF CHOICE

被引：1
|
作者：
Krivine, Jean-Louis [1 ]
机构：
[1] Univ Paris, CNRS, Paris, France
来源：
LOGICAL METHODS IN COMPUTER SCIENCE | 2021年 / 17卷 / 03期
关键词：
Curry-Howard correspondence; set theory; combinatory logic; lambda-calculus; axiom of choice;
D O I：
10.46298/LMCS-17(3:21)2021
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：1 / 21
页数：22
相关论文
共 50 条
12345