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

TL;DR

This paper explores the connection between well ordering principles and $oldsymbol{ ext{Pi}}^1_4$-statements, extending previous work on $oldsymbol{ ext{Pi}}^1_1$-induction and dilators to higher levels using $2$-ptykes.

Contribution

It introduces the concept of $2$-ptykes and establishes their fixed points as equivalent to $oldsymbol{ ext{Pi}}^1_2$-induction, advancing the analysis of higher-level $oldsymbol{ ext{Pi}}^1_4$-statements.

Findings

$oldsymbol{ ext{Pi}}^1_2$-induction is equivalent to fixed points of $2$-ptykes.

Introduces $2$-ptykes as a generalization of dilators.

Lays groundwork for analyzing $oldsymbol{ ext{Pi}}^1_4$-statements via well ordering principles.

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^1_2$-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^1_4$-statements in terms of well ordering principles.