Open AccessStrongly Uniform Bounds from Semi-Constructive Proofs
Author(s) -
Philipp Gerhardy,
Ulrich Kohlenbach
Publication year - 2004
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v11i31.21856
Subject(s) - mathematical proof , constructive , mathematics , bounded function , discrete mathematics , constructive proof , metric space , theory of computation , pure mathematics , calculus (dental) , algebra over a field , computer science , algorithm , mathematical analysis , medicine , geometry , dentistry , process (computing) , operating system
In 2003, the second author obtained metatheorems for the extraction of effective (uniform) bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT(0) and normed linear spaces and guarantee the independence of the bounds from parameters raging over metrically bounded (not necessarily compact!) spaces. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by (ineffective) straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proofs. Finally, we illustrate our main metatheorem by an example from metric fixed point theory.