Metric fixed point theory and partial impredicativity

TL;DR

This paper explores the logical strength of various fixed point theorems within reverse mathematics, establishing their equivalences to well-known subsystems and principles, and analyzing their proof-theoretic implications.

Contribution

It proves the Priess-Crampe & Ribenboim fixed point theorem in RCA_0 and characterizes Caristi's fixed point theorem's strength via the transfinite leftmost path principle.

Findings

Priess-Crampe & Ribenboim fixed point theorem is provable in RCA_0.

Caristi's fixed point theorem is equivalent to the transfinite leftmost path principle.

Weakenings of Caristi's theorem relate to WKL_0 and ACA_0.

Abstract

We show that the Priess-Crampe & Ribenboim fixed point theorem is provable in $\mathsf{RCA}_0$. 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 $\mathsf{ATR}_0$ and $\Pi^1_1\mbox{-}\mathsf{CA}_0$. We also exhibit several weakenings of Caristi's theorem that are equivalent to $\mathsf{WKL}_0$ and to $\mathsf{ACA}_0$.