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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Factorisation of the Classical Nonstandard Bounded Functional Interpretation

  • Bruno Dinis,
  • Jaime Gaspar

摘要

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.