Some logical metatheorems with applications in functional analysis
Some logical metatheorems with applications in functional analysis
复制标题
DOI：
10.1090/s0002-9947-04-03515-9
复制
发表时间：
2005-01-01
影响因子：
1.3
通讯作者：
Kohlenbach, U
中科院分区：
文献类型：
--
作者：
Kohlenbach, U
在以前的论文中，我们发展了从泛函分析中大量无效存在性证明中提取有效一致界的证明理论技术。这里的“一致”是指与紧空间中的参数无关。最近的一个不动点理论的实例研究系统地给出了在度量有界（但非紧化）子集中w.r.t.参数的均匀性，这在以前只在特殊情况下才知道。在本文中，我们证明了一般的逻辑元定理，它涵盖了不动点理论的这些特殊应用，但根本不局限于这个领域。我们的定理在一般逻辑条件下保证了非一致存在命题的这种强一致版本。此外，他们还提供了实际提取有效一致界的算法，并将原始证明转化为更强的均匀性结果。我们的元定理处理一般类型的空间，如度量空间，双曲空间，CAT(0)-空间，赋范线性空间，一致凸空间，以及内积空间。
In previous papers we have developed proof-theoretic techniques for extracting effective uniform bounds from large classes of ineffective existence proofs in functional analysis. Here 'uniform' means independence from parameters in compact spaces. A recent case study in fixed point theory systematically yielded uniformity even w. r. t. parameters in metrically bounded ( but noncompact) subsets which had been known before only in special cases. In the present paper we prove general logical metatheorems which cover these applications to fixed point theory as special cases but are not restricted to this area at all. Our theorems guarantee under general logical conditions such strong uniform versions of non-uniform existence statements. Moreover, they provide algorithms for actually extracting effective uniform bounds and transforming the original proof into one for the stronger uniformity result. Our metatheorems deal with general classes of spaces like metric spaces, hyperbolic spaces, CAT(0)-spaces, normed linear spaces, uniformly convex spaces, as well as inner product spaces.