Realizability algebras: a program to well order R

TL;DR

This paper develops a framework using realizability algebras and forcing techniques to extract programs from classical proofs involving the well-ordering of the real line and ultrafilters, bridging proof theory and computation.

Contribution

It introduces realizability algebras and adapts forcing methods to produce programs from classical analysis proofs involving the real line's well-ordering.

Findings

Constructs programs from proofs with dependent choice.

Establishes a method to realize the existence of a well-ordering of R.

Links realizability, forcing, and proof-program correspondence.

Abstract

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.