Metric fixed point theory and partial impredicativity

We show that the Priess-Crampe & Ribenboim fixed point theorem is provable in ${\mathsf{R}\mathsf{C}\mathsf{A}}_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{A}\mathsf{T}\mathsf{R}}_0$ and ${\mathrm{\Pi }}_1^1-{\mathsf{C}\mathsf{A}}_0$. We also exhibit several weakenings of Caristi’s theorem that are equivalent to ${\mathsf{W}\mathsf{K}\mathsf{L}}_0$ and to ${\mathsf{A}\mathsf{C}\mathsf{A}}_0$.