Record Details

Strongly Uniform Bounds from Semi-Constructive Proofs

BRICS Report Series

View Archive Info
 
 
Field Value
 
Title Strongly Uniform Bounds from Semi-Constructive Proofs
 
Creator Gerhardy, Philipp
Kohlenbach, Ulrich
 
Description 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.
 
Publisher Aarhus University
 
Contributor —
 
Date 2004-12-11
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
—
 
Format application/pdf
 
Identifier https://tidsskrift.dk/brics/article/view/21856
10.7146/brics.v11i31.21856
 
Source BRICS Report Series; No 31 (2004): RS-31 Strongly Uniform Bounds from Semi-Constructive Proofs
BRICS Report Series; No 31 (2004): RS-31 Strongly Uniform Bounds from Semi-Constructive Proofs
1601-5355
0909-0878
 
Language eng
 
Relation https://tidsskrift.dk/brics/article/view/21856/19283
 
Rights Copyright (c) 2015 BRICS Report Series