Well ordering principles and ${\Pi }_4^1$-statements: a pilot study

Abstract

In previous work, the author has shown that ${\Pi }_1^1$-induction along $\mathbb{N}$ is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of J.-Y. Girard's dilators, which are particularly uniform transformations of well orders. The present paper works on the next type level and considers uniform transformations of dilators, which are called $2$-ptykes. We show that ${\Pi }_2^1$-induction along $\mathbb{N}$ is equivalent to the existence of fixed points for all $2$-ptykes that satisfy a certain normality condition. Beyond this specific result, the paper paves the way for the analysis of further ${\Pi }_4^1$-statements in terms of well ordering principles.