ダイアレクティカ解釈
dialectica interpretation
$ \varphi^D = \exists x\ \forall y\ \varphi_D(x, y)
$ \varphi_Dは開．
定義
（パラメータを持ちうる）論理式$ \varphiについて，$ \varphi^D = \exists x\ \forall y\ \varphi_D(x, y)を次のように定める．
$ \varphi_i^D = \exists x^{\alpha_i}_i\, \forall y^{\beta_i}_i\, {\varphi_i}_D(x_i, y_i)とする．
$ (\varphi)^D\ (\text{atomic}) \coloneqq \varphi
$ (\varphi_1 \land \varphi_2)^D \coloneqq \exists x_1x_2^{}\, \forall y_1 y_2\, [\varphi_1 \land \varphi_2]
$ (\varphi_1 \lor \varphi_2)^D \coloneqq \exists z^0 x_1 x_2\, \forall y_1 y_2\, [(z = 0 \land \varphi_1) \lor (z = 1 \land \varphi_2)]
$ (\varphi_1 \to \varphi_2)^D \coloneqq \exists U^{\alpha_1 \to \alpha_2} Y^{\alpha_1 \times \beta_2 \to \beta_1}\, \forall x_1 y_2\, [{\varphi_1}_D(x_1, Y(x_1, y_2)) \to {\varphi_2}_D(U(x_1), y_2)]
$ (\forall z\, \varphi_1)^D \coloneqq \exists X^{0 \to \alpha_1}\, \forall z y\,[{\varphi_1}_D(X(z), y)]
$ (\exists z\, \varphi_1)^D \coloneqq \exists z x\, \forall y\,[{\varphi_1}_D(z, y)]
$ (\lnot \varphi_1)^D \coloneqq \exists Y^{\alpha_1 \to \beta_1}\, \forall x\, \lnot {\varphi_1}_D(x, Y(x))