Alg\`ebres de r\'ealisabilit\'e: un programme pour bien ordonner R
Logic in Computer Science
2010-06-01 v2 Logic
Abstract
We give a method to transform into programs, classical proofs using a well ordering of the reals. The technics uses a generalization of Cohen's forcing and the theory of classical realizability introduced by the author.
Keywords
Cite
@article{arxiv.1002.3438,
title = {Alg\`ebres de r\'ealisabilit\'e: un programme pour bien ordonner R},
author = {Jean-Louis Krivine},
journal= {arXiv preprint arXiv:1002.3438},
year = {2010}
}
Comments
45 pages