Y udai S uzuki . Studies on Partial Impredicativity in Formal Systems of Arithmetic and Computability Theory . Tohoku University. 6-3, Aza-Aoba, Aramaki, Aoba-ku, Sndai, Miyagi, Japan. 2024. Supervised by Keita Yokoyama. MSC: 03F35, 03D30. Keywords: reverse mathematics, Weihrauch degrees, predicativity
Yasuto Suzuki · Bulletin of Symbolic Logic · 2025
Abstract In this thesis, we study the complexity of theorems that may be considered partially impredicative from the point of view of reverse mathematics and Weihrauch degrees. From the perspective of reverse mathematics and ordinal analysis, the axiomatic system $\mathsf {ATR}_0$ is known as the limit of predicativity, and $\Pi ^1_{1}\text {-}\mathsf {CA}_0$ is known as an impredicative system. In this thesis, we study the complexity of some theorems that are stronger than $\mathsf {ATR}_0$ and weaker than $\Pi ^1_{1}\text {-}\mathsf {CA}_0$ from the point of view of reverse mathematics and Weihrauch degrees. In Chapter 3, we study some problems related to Knaster–Tarski’s theorem. Knaster–Tarski’s theorem states that any monotone operator on $2^{\omega }$ has a least fixed point. Avigad introduced a weaker variant, $\mathsf {FP}$ , which asserts the existence of a fixed point instead of the least fixed point, and proved that $\mathsf {FP}$ for arithmetical operators is equivalent to $\mathsf {ATR}_0$ over $\mathsf {RCA}_0$ . In this thesis, we show that $\mathsf {FP}$ for $\Sigma ^0_2$ -operators is strictly stronger than $\mathsf {ATR}_2$ , a Weihrauch degree corresponding to $\mathsf {ATR}_0$ , in terms of Weihrauch reduction. In addition, we study the bottom-up proof of Knaster–Tarski’s theorem. It is known that the least fixed point of a monotone operator is given by the $\omega _1$ -times iteration of the operator at the empty set. This implies that any monotone operator involves a hierarchy formed by the iterative applications of the operator, starting with the empty set and reaching the least fixed point. We prove that although the existence of a hierarchy is equivalent to $\mathsf {ATR}_0$ over $\mathsf {ACA}_0$ , it is stronger than $\mathsf {C}_{\omega ^{\omega }}$ in the terms of Weirhauch reduction. In Chapter 5, we study the relative leftmost path principle in Weihrauch degrees. This principle was introduced by Towsner to study partial impredicativity in reverse mathematics. He gave a hierarchy between $\mathsf {ATR}_0$ and $\Pi ^1_1\text {-}\mathsf {CA}_0$ by this principle. We show that this principle also makes a hierarchy between