Extracting Algorithms from Intuitionistic Proofs

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 S1 2 , and we briefly sketch it for the other levels of bounded

• Type: Journal
• Year: 1998
• Where: MLQ
• Authors: Fernando Ferreira, António Marques
• Keywords: Certain Intuitionistic Subsystems, Intuitionistic Counterpart, MLQ 1998, Realizability Argument