Factorization of the Shoenfield-like bounded functional interpretation
Logic
2010-09-10 v1
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.
Cite
@article{arxiv.1009.1868,
title = {Factorization of the Shoenfield-like bounded functional interpretation},
author = {Jaime Gaspar},
journal= {arXiv preprint arXiv:1009.1868},
year = {2010}
}