PARTIAL IMPREDICATIVITY IN REVERSE MATHEMATICS

In reverse mathematics, it is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on how to weaken the assumption while preserving the conclusion (other than reducing all the way to the tautology of assuming the conclusion). A main cause of this phenomenon is the proof of a Pi(1)(2) sentence from the theory Pi(1)(1)-CA(0). Using methods based on the functional interpretation, we introduce a family of weakenings of Pi(1)(1)-CA(0) and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Monger's Theorem for countable graphs.