Gödel functional interpretation and weak compactness
Gödel functional interpretation and weak compactness
复制标题
哥德尔泛函解释和弱紧性
DOI：
10.1016/j.apal.2011.12.009
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Kohlenbach
中科院分区：
文献类型：
--
作者：
Kohlenbach
近年来，基于哥德尔著名泛函（“辩证法”）解释的单调形式扩展的证明理论变换（所谓的证明解释）已被系统地用于从抽象非线性分析的证明中提取新内容。该内容既包括有效的定量范围，也包括定性的均匀性结果。抽象泛函分析中主要的无效工具之一是使用弱紧致性的顺序形式。正如我们最近验证的那样，抽象（不一定可分）希尔伯特空间的有界闭凸子集的弱紧致性的顺序形式可以在适当的形式系统中执行，这些系统由在证明挖掘程序过程中开发的现有元定理所涵盖。特别是，这种弱紧性原理的单调泛函解释可以通过可从最低类型的条递归（在 Spector 意义上）定义的泛函 Ω* 来实现。虽然对基于弱紧性的强收敛结果（分别由 Browder 和 Wittmann 提出）分析的案例研究表明，后者的使用似乎是可以消除的，但对于弱收敛定理（例如著名的 Baillon 非线性遍历定理），情况显然有所不同。对于这个定理，我们最近提取了该定理亚稳态（T.Tao 意义上的）版本的显式界限，该定理相对于 Ω*（某种受限形式）是原始递归的。在本文中，我们首次给出了 Ω* 的构造（以展开 Baillon 定理所需的形式）。作为对这种结构中使用条形递归进行精细分析的推论，我们得到 Ω* 将 Tnat 中的参数最多提升为 Tn+2 中的结果泛函（这里 T 是哥德尔 T 的片段，其原始递归仅限于类型级别 n）。特别是，我们可以由此得出结论，我们对 Baillon 定理的界限至少可以在 T4 中定义。
In recent years, proof theoretic transformations (so-called proof interpretations) that are based on extensions of monotone forms of Gödel’s famous functional (‘Dialectica’) interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness for bounded closed and convex subsets of an abstract (not necessarily separable) Hilbert space can be carried out in suitable formal systems that are covered by existing metatheorems developed in the course of the proof mining program. In particular, it follows that the monotone functional interpretation of this weak compactness principle can be realized by a functional Ω∗definable from bar recursion (in the sense of Spector) of lowest type. While a case study on the analysis of strong convergence results (due to Browder and Wittmann resp.) that are based on weak compactness indicates that the use of the latter seems to be eliminable, things apparently are different for weak convergence theorems such as the famous Baillon nonlinear ergodic theorem. For this theorem we recently extracted an explicit bound on a metastable (in the sense of T. Tao) version of this theorem that is primitive recursive relative to (a somewhat restricted form of) Ω∗. In the current paper we for the first time give the construction of Ω∗(in the form needed for the unwinding of Baillon’s theorem). As a corollary to the fine analysis of the use of bar recursion in this construction we obtain that Ω∗elevates arguments in Tnat most to resulting functionals in Tn+2(here Tnis the fragment of Gödel’s T with primitive recursion restricted to the type level n). In particular, one can conclude from this that our bound on Baillon’s theorem is at least definable in T4.
登录
查看更多内容
库尔特·哥德尔和数学基础
DOI：
--
发表时间：
2011
期刊：
影响因子：
--
作者：
Denys Turner
通讯作者：
Denys Turner
有限类型的强可大化泛函：包含不连续泛函的条递归模型
影响因子：
0.6
作者：
M. Bezem
通讯作者：
M. Bezem
遍历平均值的局部稳定性
DOI：
--
发表时间：
2007
期刊：
影响因子：
--
作者：
J. Avigad;P. Gerhardy;H. Towsner
通讯作者：
H. Towsner
DOI：
10.1090/s0002-9947-04-03515-9
发表时间：
2005-01-01
影响因子：
1.3
作者：
Kohlenbach, U
通讯作者：
Kohlenbach, U
DOI：
10.1090/s0002-9904-1976-14233-4
发表时间：
1976-11
影响因子：
1.3
作者：
H. Brezis;F. Browder
通讯作者：
H. Brezis;F. Browder