Factorisation of the Classical Nonstandard Bounded Functional Interpretation
摘要
Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such a way 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 \({\mathrm {U}_{\text{st}}} = {\mathrm {K}_{\text{st}}}\, {\mathrm {B}_{\text{st}}}\) of Jaime Gaspar and Fernando Ferreira’s classical nonstandard bounded functional interpretation \({\mathrm {U}_{\text{st}}}\) in terms of an extension of Jean-Louis Krivine’s negative translation \({\mathrm {K}_{\text{st}}}\) and Bruno Dinis and Jaime Gaspar’s intuitionistic nonstandard bounded functional interpretation \({\mathrm {B}_{\text{st}}}\) . We also give some applications of the factorisation.