Computable relations and sentences in the language of arithmetic Let $L$ be the language $\{0,1,<,+,\cdot,e,f,g\}$, with $f,g$ unary function symbols and $e$ the binary exponential, which gets interpreted as $e(n,m)=n^m$. Given $x,y\in\omega^\omega$, let $(\mathbb{N},x,y)$ be the $L$-structure which interprets $f$ and $g$ as $x$ and $y$, respectively. 
I'd like to show that, given an $L$-sentence $\phi$, there's a computable relation $P\subset \omega^{<\omega}\times\omega^{<\omega}$ such that:
$$\forall x\in\omega^\omega\exists y\in \omega^\omega (\mathbb{N},x,y)\models \phi$$
if and only if
$$\forall x\in\omega^\omega\exists y\in \omega^\omega\forall n\in\omega \ P(x|n,y|n)$$
I thought about bounding the variables in $\phi$ by $n$ and having $P$ check whether $(\mathbb{N},x,y)\models \phi_n$, where $\phi_n$ is the formula $\phi$ in which every $\forall i$ is replaced by $\forall i<n$ and every $\exists i$ is replaced by $\exists i<n$. While this is computable, we won't necessarily have $(\mathbb{N},x,y)\models \phi \iff \forall n P(x|n,y|n)$, considering for example the sentence $\exists i \forall j (j\le i)$, which is true in each finite segment but false in the whole structure. 
Any hints on how to do this?
 A: We can try to apply induction for the complexity of $\phi$. Before applying the induction, we need to generalize our problem for arbitrary formula $\phi(z)$ with no other free variables: that is, we claim that for each formula $\phi(z)$ and $m\in\omega$ there is $P$ such that
$$\forall x\exists y:(\mathbb{N},x,y)\models \phi(m) \iff \forall x\exists y \forall n\in\omega : P(x|n,y|n).$$
Now we will prove our generalized statement by induction for $\phi(z)$.
For convenience we write $\phi(z)$ as $\phi(x,y,z)$, where $x$ and $y$ are sequence of natural numbers (possibly of finite or infinite length).
If every quantifier appears in $\phi$ is bounded, simply let
$$P_{\phi,m} = \{(s,t) \mid \operatorname{lt}(s)\ge N \land \operatorname{lt}(t)\ge N \to \phi(s,t,m)\}.$$
Where $\operatorname{lt}(s)$ is the length of $s$ and $N$ is the largest number between the value of terms bounding a quantifier of $\phi$. You can see that $P_{\phi,m}$, as a subset of $\omega\times\omega$, is recursive and satisfies our condition.
Moreover, $P_{\phi,m}$ is uniform with respect to $m$ and $\phi$ in sense that the we can effectively compute the index of $P_{\phi,m}$ from $\phi$ and $m$. (This fact will be used in later.)
The inductive step is not difficult if we do not consider any unbounded quantifier. Now assume that $\phi(x,y,z,w)$ satisfies our statement. We will prove $\exists w \phi(x,y,z,w)$ also satisfy our statement.
Assume that we have recursive $P_{\phi,m,k}$ for each $\phi$ and $m,k\in\omega$. We tempt to take $P_{\exists w\phi, m} = \bigcup_k P_{\phi,m,k}$. The problem is the result need not be recursive. So we will make a trick: we will code an information of $k$ into $y$!
To motivate the proof, observe that $\forall x\exists y : \mathbb{N}\models \exists w \phi(x,y,m,w)$ iff 
$$\forall x\exists y \exists k\in\omega\forall n\in\omega : P_{\phi,m,k}(x|n,y'|n).$$
If we take $y'$ as $y'(0)=k$ and $y'(j+1)=y(j)$ then we can see
$$\forall n\in\omega P_{\phi,m,k}(x|n,y|n) \iff \forall n\in\omega P_{\phi',m,y'(0)}(x|n,y|n).$$
Here $\phi'$ is obtained by replacing all occurrence of $y(v)$ by $y(Sv)$.
From this, we can guess the set 
$$P_{\exists w\phi(w),m}:= \{(s,t) \mid (s,t_0) \in P_{\phi',m,t(0)}\}$$
may work for $t_0(i):= t(i+1)$.
