2008/09/14 by Jean-Louis Krivine, Krivine, Jean-Louis · 1 citation
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #Logic, programming, and type systems #Mathematical and Theoretical Analysis #cs.LO
paper · pdf · doi:10.48550/arxiv.0809.2394
34 p
arxiv created 2008/09/14 · arxiv updated 2009/12/01
We show how to transform into programs the proofs in classical Analysis which use the existence of an ultrafilter on the integers. The method mixes the classical realizability introduced by the author, with the "forcing" of P. Cohen. The programs we obtain, use read and write instructions in random access memory.