Extracting Algorithms from Intuitionistic Proofs
Fernando A.F. Ferreira, António Marques · Mathematical logic quarterly · 1998
Abstract This paper presents a new method ‐ which does not rely on the cut‐elimination theorem ‐ for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory S , and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1.