Premium
Light monotone Dialectica methods for proof mining
Author(s) -
Hernest MirceaDan
Publication year - 2009
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.200710093
Subject(s) - realizability , mathematical proof , interpretation (philosophy) , monotone polygon , mathematics , realization (probability) , translation (biology) , extensionality , computer science , calculus (dental) , algorithm , discrete mathematics , programming language , chemistry , medicine , biochemistry , statistics , geometry , dentistry , messenger rna , gene
In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof‐theoretic techniques employed by Kohlenbach for the synthesis of new (and better) effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method (developed by the author in his thesis, as an adaptation to Dialectica interpretations of Berger's original technique for modified realizability and A‐translation) of “colouring” some of the quantifiers as “non‐computational” extends well to ε ‐arithmetization, elimination‐of‐extensionality and model‐interpretation (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)