Jean-Louis Krivine - Realizability algebras: a program to well order R

lmcs:1070 - Logical Methods in Computer Science, August 9, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:2)2011
Realizability algebras: a program to well order RArticle

Authors: Jean-Louis Krivine

    The theory of classical realizability is a framework in which we can develop the proof-program correspondence. Using this framework, we show how to transform into programs the proofs in classical analysis with dependent choice and the existence of a well ordering of the real line. The principal tools are: The notion of realizability algebra, which is a three-sorted variant of the well known combinatory algebra of Curry. An adaptation of the method of forcing used in set theory to prove consistency results. Here, it is used in another way, to obtain programs associated with a well ordering of R and the existence of a non trivial ultrafilter on N.


    Volume: Volume 7, Issue 3
    Published on: August 9, 2011
    Imported on: May 15, 2010
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    19 Documents citing this article

    Consultation statistics

    This page has been seen 1043 times.
    This article's PDF has been downloaded 417 times.