Reverse Mathematics of WQO’s of Transfinite Sequences with Finite Range

In this talk I will present the result about the provability in ATR_0 of the theorem of Nash-Williams that sequences with finite range over a wqo form a wqo. For this we develop a framework where we work with α-wqo’s over primitive recursive set theory extended with a global enumeration function and then transfer the results obtained there to ATR_0.

The talk is based on a research project joint with Giovanni Soldà.