Factorisation of the Classical Nonstandard Bounded Functional Interpretation

Abstract

Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such away that provability is preserved, proofs are (essentially) translated into proofs, and information about the proofs is gathered. Functional interpretations have many uses, such as: relative consistency results, conservation results and the extraction of computational content from proofs. We prove the factorisation Ust = Kst Bst of Jaime Gaspar and Fernando Ferreira’s classical nonstandard bounded functional interpretation Ust in terms of an extension of Jean-Louis Krivine’s negative translation Kst and Bruno Dinis and Jaime Gaspar’s intuitionistic nonstandard bounded functional interpretation Bst. We also give some applications of the factorisation.