Premium
Extracting Algorithms from Intuitionistic Proofs
Author(s) -
Ferreira Fernando,
Marques António
Publication year - 1998
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19980440202
Subject(s) - realizability , mathematical proof , sketch , mathematics , argument (complex analysis) , algebra over a field , bounded function , intuitionistic logic , discrete mathematics , calculus (dental) , algorithm , arithmetic , pure mathematics , linear logic , medicine , mathematical analysis , biochemistry , chemistry , geometry , dentistry
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 2 1 , and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ 1 .