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 ATR₀ is known as the limit of predicativity, and ¹₁ - CA₀ is known as an impredicative system. In this thesis, we study the complexity of some theorems that are stronger than ATR₀ and weaker than ¹₁ - CA₀ 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^ has a least fixed point. Avigad introduced a weaker variant, FP, which asserts the existence of a fixed point instead of the least fixed point, and proved that FP for arithmetical operators is equivalent to ATR₀ over RCA₀. In this thesis, we show that FP for ⁰₂ -operators is strictly stronger than ATR₂, a Weihrauch degree corresponding to ATR₀, 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 ₁ -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 ATR₀ over ACA₀, it is stronger than C ^ 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 ATR₀ and ¹₁ - CA₀ by this principle. We show that this principle also makes a hierarchy between ATR₂ and C ^ in Weihrauch degrees. We also show that the relative leftmost path principle is, not the same as, but very close to a variant of -model reflection. In Chapter 6, we introduce a hierarchy dividing \ ¹₂: ¹₁ {- CA₀ \}. Then, we give some characterizations of this hierarchy using some principles equivalent to ¹₁ - CA₀: leftmost path principle, Ramsey’s theorem for ⁰ₙ classes of N^ {N} and the determinacy of Gale–Stewart game for (⁰₁) ₙ classes. As an application, our hierarchy explicitly shows that the number of applications of the hyperjump operator needed to prove ⁰ₙ Ramsey’s theorem or (⁰₁) ₙ determinacy increases when the subscript n increases. Abstract prepared by Yudai Suzuki. E-mail: yudai. suzuki. research@gmail. com.
Yasuto Suzuki (Sun,) studied this question.