Uniform Functional Interpretations
摘要
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.