Factorization of the Shoenfield-like bounded functional interpretation

TL;DR

This paper proves a new factorization theorem for a Shoenfield-like bounded functional interpretation, extending previous work on the classical Shoenfield translation and its variants.

Contribution

It establishes a novel factorization of Ferreira's Shoenfield-like bounded functional interpretation in terms of known translations and interpretations.

Findings

Proves the factorization U = KB for the bounded interpretation U.

Extends classical factorization results to bounded functional interpretations.

Provides a new proof technique for the factorization involving bounded translations.

Abstract

We adapt Streicher and Kohlenbach's proof of the factorization S = KD of the Shoenfield translation S in terms of Krivine's negative translation K and the G\"odel functional interpretation D, obtaining a proof of the factorization U = KB of Ferreira's Shoenfield-like bounded functional interpretation U in terms of K and Ferreira and Oliva's bounded functional interpretation B.