Alg\`ebres de r\'ealisabilit\'e: un programme pour bien ordonner R

TL;DR

This paper presents a method to convert classical proofs involving a well-ordering of the reals into programs, utilizing a generalized forcing technique and classical realizability theory.

Contribution

It introduces a novel approach combining generalized Cohen forcing with classical realizability to transform proofs into executable programs.

Findings

Successful transformation of classical proofs into programs

Extension of Cohen's forcing to real numbers

Integration of realizability theory with forcing techniques

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.