Unifying functional interpretations (Q867407)

The author shows how different functional interpretations can be integrated in one formal framework with two parameters: The ``bounded'' quantifications \(\forall\;{\mathbf x} \sqsubset {\mathbf t} A({\mathbf x})\) and \(\exists\;{\mathbf x} \prec {\mathbf t} A({\mathbf x})\). The different instantiations are summarized in Table 3 (p.~287) as follows (using the author's notations): \[ \begin{alignedat}{3} &\forall\;{\mathbf x} \sqsubset {\mathbf t} w &\quad &\exists\;{\mathbf x} \prec {\mathbf t} A({\mathbf x}) &\quad &\mathbf{Functional interpretations} \\ \\ &A({\mathbf t})& &A({\mathbf t})& &\text{Dialectica interpretation (1958)} \\ &\forall\;{\mathbf x} A({\mathbf x})& &A({\mathbf t})& &\text{Modified realizability (1962)} \\ &\forall\;{\mathbf x} \in {\mathbf t} A({\mathbf x})& &A({\mathbf t})& &\text{Diller-Nahm interpretationi (1962)} \\ &\forall\;\underline{{\mathbf x}} \in \text{rng}({\mathbf t}) \forall\;\overline{{\mathbf x}} A({\mathbf x})& &A({\mathbf t})& &\text{Stein's family of interpretations (1979)} \\ &A({\mathbf t})& &\exists\;{\mathbf x} \leq^* {\mathbf t} A({\mathbf x})& &\text{Monotone Dialectica interpretation (1996)} \\ &\forall\;{\mathbf x} A({\mathbf x})& &\exists\;{\mathbf x} \leq^* {\mathbf t} A({\mathbf x})& &\text{Monotone modified realizability (1998)} \\ &\tilde{\forall} \leq^* {\mathbf t} A({\mathbf x})& &A({\mathbf t})& &\text{Bounded functional interpretation (2005).} \end{alignedat} \]