Partial Impredicativity in Reverse Mathematics

TL;DR

This paper explores partial impredicativity in reverse mathematics, introducing weakenings of a key system to better understand implications and establish new bounds for theorems like Nash-Williams and Menger's.

Contribution

It introduces a family of weakenings of { ext{ extPi}}^1_2 and applies them to derive new upper bounds for important combinatorial theorems.

Findings

New upper bounds for Nash-Williams Theorem

New upper bounds for Menger's Theorem

Insights into impredicativity in reverse mathematics

Abstract

In reverse mathematics, is is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on on how to weaken the assumption while preserving the conclusion. A main cause of this phenomenon is the proof of a $\Pi^1_2$ sentence from the theory {\Pioo}. Using methods based on the functional interpretation, we introduce a family of weakenings of {\Pioo} and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs.