Pure patterns of order 2

TL;DR

This paper establishes a correspondence between classical ordinal notations and elementary patterns of order 2, characterizing the proof-theoretic strength of certain second-order theories and linking well-quasi ordering to transfinite induction.

Contribution

It introduces mutual elementary recursive isomorphisms between ordinal notations and elementary patterns of order 2, advancing the analysis of proof-theoretic ordinals and well-quasi orderings.

Findings

Characterizes the proof-theoretic ordinal of $ ext{KPl}_0$.

Shows Carlson's result implies transfinite induction up to this ordinal.

Provides a framework for analyzing more complex pattern systems.

Abstract

We provide mutual elementary recursive order isomorphisms between classical ordinal notations, based on Skolem hulling, and notations from pure elementary patterns of resemblance of order $2$, showing that the latter characterize the proof-theoretic ordinal of the fragment $\Pi^1_1$-$\mathrm{CA}_0$ of second order number theory, or equivalently the set theory $\mathrm{KPl}_0$. As a corollary, we prove that Carlson's result on the well-quasi orderedness of respecting forests of order $2$ implies transfinite induction up to the ordinal of $\mathrm{KPl}_0$. We expect that our approach will facilitate analysis of more powerful systems of patterns.