Taking a Detour to Zero: An Alternative Formalization of Functions Beyond PR

TL;DR

This paper introduces a new formalism for fast-growing functions indexed by natural number sets, offering an alternative to traditional systems like T and F, with potential applications in proof theory.

Contribution

It presents a novel recursion formalism indexed by natural number sets, expanding the tools for expressing fast-growing functions beyond existing typed systems.

Findings

Formalism expresses functions comparable to system T

Highlights relationship with Wainer hierarchy

Potential applications in CERES cut-elimination

Abstract

There are two well known systems formalizing total recursion beyond primitive recursion (\textbf{PR}), system \textbf{T} by G\"odel and system \textbf{F} by Girard and Reynolds. system \textbf{T} defines recursion on typed objects and can construct every function of Heyting arithmetic (\textbf{HA}). System \textbf{F} introduces type variables which can define the recursion of system \textbf{T}. The result is a system as expressive as second-order Heyting arithmetic (\textbf{HA}$_{2}$). Though, both are able to express unimaginably fast growing functions, in some applications a more flexible formalism is needed. One such application is CERES cut-elimination for schematic \textbf{LK}-proofs ($CERES_{s}$) where the shape of the recursion is important. In this paper we introduce a formalism for fast growing functions without a type theory foundation. The recursion is indexed by ordered sets of natural numbers. We highlight the relationship between our recursion and the Wainer hierarchy to provide an comparison to existing systems. We can show that our formalism expresses the functions expressible using system \textbf{T}. We leave comparison to system \textbf{F} and beyond to future work.