A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem

TL;DR

This paper provides a direct, explicit construction proof of Schwichtenberg's bar recursion closure theorem, simplifying the conversion of bar recursive definitions into System T and sharpening the definability results.

Contribution

It introduces a more straightforward proof method using an explicit construction and logical relations, replacing the original indirect proof via infinitary terms.

Findings

The explicit construction allows direct conversion of bar recursive definitions into System T.

The proof simplifies understanding and computation of System T definable functionals.

A sharper result states the definability in fragments T_i with explicit bounds.

Abstract

In 1979 Schwichtenberg showed that the System $\text{T}$ definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$. More precisely, if the functional $Y$ which controls the stopping condition of Spector's bar recursor is $\text{T}$-definable, then the corresponding bar recursion of type levels $0$ and $1$ is already $\text{T}$-definable. Schwichtenberg's original proof, however, relies on a detour through Tait's infinitary terms and the correspondence between ordinal recursion for $\alpha < \varepsilon_0$ and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system $\text{T}$ input, what the corresponding system $\text{T}$ output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into $\text{T}$-definitions under the conditions of Schwichtenberg's theorem. Finally, with the explicit construction we can also easily state a sharper result: if $Y$ is in the fragment $\text{T}_i$ then terms built from $\text{BR}^{\mathbb{N}, \sigma}$ for this particular $Y$ are definable in the fragment $\text{T}_{i + \max \{ 1, \text{level}{\sigma} \} + 2}$.