Dialectica interpretation

Definition

Let $\mathrm{T}$ be Gödel's system of primitive recursive functionals of finite type. To each formula $A$ of Heyting arithmetic, the Dialectica interpretation assigns a formula $A^D = \exists x\, \forall y\, A_D(x, y)$. Here $x$ and $y$ are finite tuples of variables of finite type, and $A_D$ is quantifier-free. Write $A^D = \exists x\, \forall y\, A_D(x, y)$ and $B^D = \exists u\, \forall v\, B_D(u, v)$. The clauses are these.

1. If $A$ is atomic, then $A^D = A_D = A$, with empty tuples $x$ and $y$.
2. $(A \wedge B)^D = \exists x, u\, \forall y, v\, \bigl( A_D(x, y) \wedge B_D(u, v) \bigr)$.
3. $(A \vee B)^D = \exists z, x, u\, \forall y, v\, \bigl( (z = 0 \to A_D(x, y)) \wedge (z \ne 0 \to B_D(u, v)) \bigr)$, where $z$ is a number variable.
4. $(A \to B)^D = \exists f, g\, \forall x, v\, \bigl( A_D(x, f x v) \to B_D(g x, v) \bigr)$.
5. $(\exists z\, A(z))^D = \exists z, x\, \forall y\, A_D(x, y, z)$.
6. $(\forall z\, A(z))^D = \exists f\, \forall z, y\, A_D(f z, y, z)$.

Negation $\neg A$ is read as $A \to (0 = 1)$.