Normal functions and maximal order types

TL;DR

This paper explores the conditions under which transformations of well partial orders induce normal functions, revealing that strong normality in $ extsf{WPO}$-dilators characterizes this phenomenon and relates to foundational logical principles.

Contribution

It establishes a precise link between strong normality in $ extsf{WPO}$-dilators and the induction principles in ordinal analysis, clarifying when such transformations produce normal functions.

Findings

Strong normality in $ extsf{WPO}$-dilators characterizes when they induce normal functions.

The reverse implication holds for well-behaved $ extsf{WPO}$-dilators.

The uniform Kruskal theorem for strongly normal $ extsf{WPO}$-dilators is equivalent to $oldsymbol{ ext{Pi}}^1_1$-induction.

Abstract

Transformations of well partial orders induce functions on the ordinals, via the notion of maximal order type. In most examples from the literature, these functions are not normal, in marked contrast with the central role that normal functions play in ordinal analysis and related work from computability theory. The present paper aims to explain this phenomenon. In order to do so, we investigate a rich class of order transformations that are known as $\mathsf{WPO}$-dilators. According to a first main result of this paper, $\mathsf{WPO}$-dilators induce normal functions when they satisfy a rather restrictive condition, which we call strong normality. Moreover, the reverse implication holds as well, for reasonably well behaved $\mathsf{WPO}$-dilators. Strong normality also allows us to explain another phenomenon: by previous work of Freund, Rathjen and Weiermann, a uniform Kruskal theorem for $\mathsf{WPO}$-dilators is as strong as $\Pi^1_1$-comprehension, while the corresponding result for normal dilators on linear orders is equivalent to the much weaker principle of $\Pi^1_1$-induction. As our second main result, we show~that $\Pi^1_1$-induction is equivalent to the uniform Kruskal theorem for $\mathsf{WPO}$-dilators that are strongly normal.