权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Extraction of effective uniform bounds from proofs based on sequential compactness via logical analysis

通过逻辑分析从基于顺序紧致性的证明中提取有效的统一边界

基本信息

批准号：
108728300
负责人：
Professor Dr. Ulrich Kohlenbach
金额：
--
依托单位：
Arbeitsgruppe Logik
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2009
资助国家：
德国
起止时间：
2008-12-31 至 2018-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/108728300?language=en
关键词：
Extraction effective uniform bounds proofs

项目摘要

During the last 20 years an applied form of proof theory (``proof mining'') has emerged as a new area of mathematical logic. Here the focus is to use proof-theoretic transformations to extract new data such as effective bounds from concrete i(typically neffective) proofs in various areas of mathematics. Most systematically, this has resulted in many applications in nonlinear analysis (e.g. in metric fixed point theory as well as in ergodic theory). During the project KO 1737/5-1 the focus has been on the analysis of proofs that use strong as well as weak sequential compactness. In this application for a continuation of this project we will treat strong convergence results that have been established also with the use of principles such as Banach limits, ultraproducts, ultralimits and the Loeb measure, i.e. principles which involve the axiom of choice. W.r.t. Banach limits first surprising results have been established already during the past months. Many questions, however, are left open. In particular, this is the case for the extraction of a rate of metastability (in the sense of Tao) for the strong convergence of the resolvent of nonexpansive and - more generally - accretive operators in uniformly smooth Banach spaces from a proof due to Bruck and Reich which uses both weak compactness as well as Banach limits. Taken together with results obtained already during this project this would immediately yield rates of metastability for a nonlinear ergodic theorem due to Shioji and Takahashi as well for an iteration scheme due to Bruck for pseudocontrations proved to converge by Chidume and Zegeye). It is known that mos of the convergence results treated so far in this project, full effective rates of convergence do not exist and so one usually aims at weaker effective bounds on metastability (which - ineffectively - is equivalent to convergence) which are guaranteed to exist by proof-theoretic results of the applicant. Very recently, Avigad and Rute observed that in a particular case treated by us, a stronger effective and uniform bound on the number of so-called epsilon-fluctuations is possible. We intend to investigate whether this is a more general phenomenon which can be accounted for in logical terms.During the project so far new methods have been developed for extracting uniform bounds from proofs that make use of a nonprincipal ultrafilter U. However, these methods need to be incorporated into the general logical machinery of the logical metatheorems to apply to proofs using the ultrapower X/U of sbtract spaces X (frequently used in nonlinear analysis).Such extensions are also needed for new methods developed in the course of the project which guarantee the extractability of primitive recursive bounds from proof that use the Bolzano-Weierstrass principle in the form sating the existence of a Cauchy-subsequence without a rate of convergence (which is known to be impossible when such a rate is used).

在过去的20年里，证明理论的一种应用形式(“证据挖掘”)已经成为数理逻辑的一个新领域。这里的重点是使用证明论转换来提取新的数据，例如从数学的各个领域的具体I(通常是无效的)证明中提取有效界。最系统地，这导致了在非线性分析中的许多应用(例如，在度量不动点理论以及遍历理论中)。在项目KO 1737/5-1期间，重点分析了使用强序列紧性和弱序列紧性的证明。在这个项目的继续申请中，我们将处理已经建立的强收敛结果，这些结果也是使用诸如Banach极限、超积、超极限和Loeb测度的原理建立的，即涉及选择公理的原理。W.r.t.巴纳赫限制首先在过去的几个月里已经确定了令人惊讶的结果。然而，许多问题仍然悬而未决。特别地，这是从Bruck和Reich的同时使用弱紧性和Banach极限的证明中提取一致光滑Banach空间中非扩张和-更一般-增生算子的预解式的强收敛的亚稳率(在陶氏意义下)的情况。与在这个项目中已经得到的结果相结合，这将立即给出由Shioji和Takahashi得到的非线性遍历定理的亚稳率，以及由Chidume和Zegye证明收敛的伪压缩的Bruck迭代格式的亚稳率。众所周知，到目前为止在本项目中处理的收敛结果中，不存在完全有效的收敛速度，因此通常针对申请人的证明理论结果保证存在的亚稳性(无效地等价于收敛)的较弱的有效界。最近，阿维加德和鲁特观察到，在我们处理的一个特殊情况下，对所谓的epsilon涨落的数量进行更有效和统一的约束是可能的。我们打算调查这是否是一种更普遍的现象，可以从逻辑上解释。在这个项目中，到目前为止，已经开发了新的方法来从利用非主要超滤U的证明中提取一致的界。然而，这些方法需要结合到逻辑元定理的一般逻辑机器中，以应用于使用空间空间X的超幂X/U的证明(在非线性分析中经常使用)。在项目过程中发展的新方法也需要这样的扩展，这些方法保证从使用Bolzano-Weerstrass原理的证明中提取本原递归界的可提取形式，该形式满足没有收敛速度的柯西子序列的存在(当使用这样的速度时，已知这是不可能的)。