Metric fixed point theory and partial impredicativity
Metric fixed point theory and partial impredicativity
复制标题
DOI：
10.1098/rsta.2022.0012
复制
发表时间：
2023-05-29
期刊：
影响因子：
5
通讯作者：
Yokoyama, K.
中科院分区：
文献类型：
--
作者：
Fernandez-Duque, D.;Shafer, P.;Yokoyama, K.
我们证明了Priess-Crampe & Ribenboim不动点定理在RCA 0中是可证的。此外，我们证明了Caristi的不动点定理的Baire和Borel函数是等价的超限最左路径原则，其中福尔斯下降严格ATR 0和p11-CA 0之间。我们还展示了Caristi定理的几个等价于WKL 0和ACA 0的弱化。这篇文章是主题“证明理论的现代观点”的一部分。
We show that the Priess-Crampe & Ribenboim fixed point theorem is provable in RCA0. Furthermore, we show that Caristi's fixed point theorem for both Baire and Borel functions is equivalent to the transfinite leftmost path principle, which falls strictly between ATR0 and p11-CA0. We also exhibit several weakenings of Caristi's theorem that are equivalent to WKL0 and to ACA0.This article is part of the theme issue 'Modern perspectives in Proof Theory'.