We study a variant of Gödel’s dialectica (functional) interpretation whereby quantifiers are treated uniformly, while atomic formulas are assumed to carry computational content. We argue that this leads to a more flexible approach to functional interpretations, aligning the dialectica interpretation with Cohen’s method of forcing – following recent work of Alexander Miquel on implicative structures. We also discuss how this could lead to an alternative way of dealing with abstract spaces in proof mining. The interpretation is first presented in the setting of classical first-order logic, but is subsequently factorised as a composition of Krivine’s negative translation and a uniform intuitionistic interpretation. For any (multi-sorted) first-order theory, a concrete functional interpretation can be obtained once a choice of base interpretation for the predicate symbols is fixed.

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

Uniform Functional Interpretations

  • Paulo Oliva

摘要

We study a variant of Gödel’s dialectica (functional) interpretation whereby quantifiers are treated uniformly, while atomic formulas are assumed to carry computational content. We argue that this leads to a more flexible approach to functional interpretations, aligning the dialectica interpretation with Cohen’s method of forcing – following recent work of Alexander Miquel on implicative structures. We also discuss how this could lead to an alternative way of dealing with abstract spaces in proof mining. The interpretation is first presented in the setting of classical first-order logic, but is subsequently factorised as a composition of Krivine’s negative translation and a uniform intuitionistic interpretation. For any (multi-sorted) first-order theory, a concrete functional interpretation can be obtained once a choice of base interpretation for the predicate symbols is fixed.