Hyperations, Veblen progressions and transfinite iterations of ordinal functions

TL;DR

This paper introduces hyperations and cohyperations as transfinite iterations of ordinal functions, refining Veblen progressions and offering new tools for analyzing ordinal sequences in proof theory.

Contribution

It systematically develops hyperations and cohyperations, providing a natural refinement of Veblen progressions and new methods for analyzing ordinal functions.

Findings

Hyperations preserve normality and refine Veblen progressions.

Cohyperations are left-additive and define left inverses to hyperations.

Hyperations are useful for algebraic manipulation and fine-grained analysis.

Abstract

In this paper we introduce hyperations and cohyperations, which are forms of transfinite iteration of ordinal functions. Hyperations are iterations of normal functions. Unlike iteration by pointwise convergence, hyperation preserves normality. The hyperation of a normal function f is a sequence of normal functions so that f^0= id, f^1 = f and for all ordinals \alpha, \beta we have that f^(\alpha + \beta) = f^\alpha f^\beta. These conditions do not determine f^\alpha uniquely; in addition, we require that the functions be minimal in an appropriate sense. We study hyperations systematically and show that they are a natural refinement of Veblen progressions. Next, we define cohyperations, very similar to hyperations except that they are left-additive: given \alpha, \beta, f^(\alpha + \beta)= f^\beta f^\alpha. Cohyperations iterate initial functions which are functions that map initial segments to initial segments. We systematically study cohyperations and see how they can be employed to define left inverses to hyperations. Hyperations provide an alternative presentation of Veblen progressions and can be useful where a more fine-grained analysis of such sequences is called for. They are very amenable to algebraic manipulation and hence are convenient to work with. Cohyperations, meanwhile, give a novel way to describe slowly increasing functions as often appear, for example, in proof theory.