I've been recently reading the Gödel's functional interpretation (or Dialectica). It is generally defined inductively, as could be found here: http://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf page 10 (or any book covering this topic). My question is: why this definition is valid? The left hand side the $D$ is superscripted while the right is subscripted. Naively it does not seem to tell how to unwrap a complicated formula with D being subscripted. Do they carry the same rule? If this is the case the following would be my attempt to translate an ordinary formula: $A(x,y)$ is atomic
$(\exists x \forall y A(x,y))^D= \exists x,z \forall t (\forall y A(y))_D(z,t,x)= \exists x,z \forall t \exists X \forall a,y A_D (X(y),a,z,t,x)=\exists x,z \forall t \exists X \forall a,y A (X(y),a,z,t,x)$.
And it looks wrong. This should be really simple so I might have cracked my head. I appreciate examples also! Thanks!
$\phi_D$ is just $\phi^D$ with the leading quantifiers removed. The result will always be quantifier free.
For example, if $\phi^D = (\forall x)(\exists y)\phi_D(x,y)$ and $\psi^D = (\forall u)(\exists v)\psi_D(u,v)$ then $$ (\phi \land \psi)^D = (\forall x)(\forall u)(\exists x)(\exists v)(\phi_D(x,y)\land(\psi_D(u,v)) $$
For your other example, it is easier not to start with $x,y$ as the free variables. Say we have $(\exists m)(\forall n)A(m,n)$, where $A(m,n)$ is atomic. Then $A^D = A_D = A$, and the lists $x$ and $y$ are empty in $A^D$.
Next, we want to convert $(\forall n)A(m,n)$. Because the lists $x$ and $y$ are empty in $A^D$, we have $$ ((\forall n) A(m,n))^D \equiv (\forall n)A_D \equiv (\forall n) A_D(n,m) \equiv (\forall n) A(m,n) $$
In $(\forall n) A(m,n))^D$ the list $x$ is still empty and the list $y$ now contains $n$.
Finally $((\exists m)(\forall n) A(m,n))^D$ will be $(\exists m)(\forall n)A(m,n)$.
The translation is more interesting for formulas in which the quantifiers appear in the other order, or which contain the connectives $\lor$ or $\to$. For example, $(\forall m)(\exists n)A(m,n)$ becomes $(\exists N)(\forall m)A(m,N(m))$.
The original matrix $A$ never gains new variables; it's just that sometimes more complicated terms are substituted for the original variables. Except when there are disjunctions in the original matrix; then the new matrix gains one more free variable that tells which side of the disjunction is supposed to hold.
The general idea of the translation is that, to convert $\psi$ to $\psi^D$, you first convert all the subformulas. Then:
If $\psi$ is a conjunction, just bring all the quantifiers to the front in the order $\exists \forall$
If $\psi$ is a disjunction, you bring to the front all the quantifiers that already exist, in the order $\exists \forall$, and then add one new existential quantifier in front.
If $\psi$ is $(\exists x)\phi$ then $\psi^D$ is $(\exists x)\phi^D$
If $\psi$ is $(\forall x)\phi$ then you start with $(\forall x)\phi^D$ and Skolemize to put the quantifiers into the order $\exists \forall$
If $\psi$ is a negation $\lnot \phi$, first convert $\phi$ to $\phi^D$, then push the negation all the way across the quantifiers of $\phi^D$, then Skolemize to bring the quantifiers back to $\exists \forall$ order.
The rule for $\to$ is more complicated, but it does not add any new free variables. Instead it converts two previous quantifiers to higher types.
The only rule that adds new free variables is the one for disjunction.