Mathematical Logic Quarterly 55 (5):551-561 (2009)

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 effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method of “colouring” some of the quantifiers as “non-computational” extends well to ε-arithmetization, elimination-of-extensionality and model-interpretation
Keywords uniform quantifiers  Program extraction from proofs  monotone functional interpretation
Categories (categorize this paper)
DOI 10.1002/malq.200710093
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 65,683
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Pointwise Hereditary Majorization and Some Applications.Ulrich Kohlenbach - 1992 - Archive for Mathematical Logic 31 (4):227-241.
Note on the Fan Theorem.A. S. Troelstra - 1974 - Journal of Symbolic Logic 39 (3):584-596.

View all 9 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

A Note on the Monotone Functional Interpretation.Ulrich Kohlenbach - 2011 - Mathematical Logic Quarterly 57 (6):611-614.
Unifying Functional Interpretations.Paulo Oliva - 2006 - Notre Dame Journal of Formal Logic 47 (2):263-290.
Proofs with Monotone Cuts.Emil Jeřábek - 2012 - Mathematical Logic Quarterly 58 (3):177-187.
Monotone Proofs of the Pigeon Hole Principle.R. Gavalda, A. Atserias & N. Galesi - 2001 - Mathematical Logic Quarterly 47 (4):461-474.
Proof Mining in Topological Dynamics.Philipp Gerhardy - 2008 - Notre Dame Journal of Formal Logic 49 (4):431-446.
Unary Quantifiers on Finite Models.Jouko Väänänen - 1997 - Journal of Logic, Language and Information 6 (3):275-304.
Monotone Majorizable Functionals.Helmut Schwichtenberg - 1999 - Studia Logica 62 (2):283-289.
Scope Dominance with Upward Monotone Quantifiers.Alon Altman, Ya'Acov Peterzil & Yoad Winter - 2005 - Journal of Logic, Language and Information 14 (4):445-455.
Cardinal Invariants of Monotone and Porous Sets.Michael Hrušák & Ondřej Zindulka - 2012 - Journal of Symbolic Logic 77 (1):159-173.


Added to PP index

Total views
11 ( #835,928 of 2,462,427 )

Recent downloads (6 months)
1 ( #449,313 of 2,462,427 )

How can I increase my downloads?


My notes