Given $x, y \in \omega^\omega$, we may define an expanded structure $(\mathbb{N}, x, y)$ where $x,y$ are treated as interpretations of function symbols. I want to show that there is a computable set $P \subseteq \omega^{<\omega} \times \omega^{<\omega} \times \omega^{<\omega}$ such that
$\forall x \in \omega^{\omega} \exists y \in \omega^{\omega} (\mathbb{N}, x, y) \vDash \sigma \iff \forall x \in \omega^{\omega} \exists y \in \omega^{\omega} \forall n \in \omega P(x_{|n}, y_{|n})$
This is an important intermediary step in proving (a version of) the Schoenfield Absoluteness theorem. To be clear, I don't want a proof of the Schoenfield absoluteness theorem. I'm curious about this in particular.
I imagine $P$ has to do with the recursive definition of the $\vDash$ relation, but I'm not sure I can completely see it. I would appreciate the help.
To clarify, the actual structure in question - per the comments below - is $\mathcal{N}_{x,y}:=(\mathbb{N};+,\times,<,x,y)$ or something "morally equivalent" to that (e.g. it's fine if we drop "$<$"). Weakening the language doesn't make the left-to-right direction any harder of course, but it may make the right-to-left direction false.
The right-to-left direction is vastly easier: it basically amounts to the fact that computable relations are definable in $(\mathbb{N};+,\times,<)$. So I'll ignore it here and focus on the interesting part, the left-to-right direction.
The left-to-right direction is rather tedious to write out in full, but the key ideas aren't too hard. This answer is really just a hint for the left-to-right direction but I think it does extract those key ideas, and will make the full solution much simpler to understand. Specifically, I'll indicate how to solve a "toy version" of the actual problem which, while substantially simpler, still in my opinion will clarify the idea.
Below I've written out my rationale for the choice of problem; if you just want to dive in, skip to the subsequent section.
First, I'm going to make a seemingly-trivial change to the desired property of $P$ in question: $$\forall x \in \omega^{\omega} \exists y \in \omega^{\omega} \mathcal{N}_{x,y} \vDash \sigma \iff \forall x \in \omega^{\omega} \exists \color{red}{z} \in \omega^{\omega} \forall n \in \omega P(x_{|n}, z_{|n}).$$ I want to change the variable name because this $z$ should not be thought of as serving the role of $y$ in the left hand side. Instead, $z$ contains a lot more information. Specifically, and this is the absolutely key idea, we'll think of the desired $z$ as being the "join" of two reals $a,b\in\omega^\omega$ where $a$ is a real such that $\mathcal{N}_{x,a}\models \sigma$ and $b$ is a real witnessing that fact in a precise sense to be developed below.
Second, I want to replace computability with topology. This is often a useful simplifying step, under the slogan "computable = effectively tame" for tame $\in\{$ continuous, closed, ...$\}$ - in this case, tame=closed. (The converse is also often useful, e.g. in the proof of the Harrington-Kechris-Louveau theorem, but not relevant right now.)
Finally, I want to fix a specific $\sigma$ which will be easier to work with - I'll use the sentence $$\sigma\equiv\forall m\exists n>n(x_n<y_n),$$ often abbreviated as "$y$ escapes $x$." This is just a very simple sentence to think about, while not being totally trivial.
So with all that, here's the "toy version" of the original problem:
The point of looking at this toy version first is that it lets us focus on the actually "deep" part of the problem: witnessing satisfaction by reals. Fixing reals $x$ and $y$, what does it mean for one real $w$ to witness the fact that $\mathcal{N}_{x,y}\models \forall m\exists n>m(x_n<y_n)$?
Well, think of a witness as a way of convincing me that the given statement holds. The way you'd do this is provide me with a rule giving an appropriate $n$ for each $m$. Now it's too much to hope for an actual rule-rule, but we can "bundle up" all the individual $m$-cases into a single real: for appropriate $x$ and $y$, we'll say $w$ witnesses $\mathcal{N}_{x,y}\models\sigma$ iff for each $i\in\omega$ we have $w_i>i$ and $x_{w_i}<y_{w_i}$.
Taking the idea from the start of this answer, this suggests looking at the following set. First, let $p_0,p_1$ be the projection maps coming from the Cantor pairing function, so that for all $l\in\omega$ we have $l=\langle p_{left}(l), p_{right}(l)\rangle$. Next, let $\mathbb{p}_{left},\mathbb{p}_{right}:\omega^\omega\rightarrow\omega^\omega$ be their "bitwise" analogues for reals, so that for each $c\in\omega^\omega$ we have $c_i=\langle \mathbb{p}_{left}(c)_i, \mathbb{p}_{right}(c)_i \rangle$. We then want to look at: $$\mathfrak{Q}=\{\langle x,z\rangle: (\mathbb{p}_{right}(z)\mbox{ witnesses }\mathcal{N}_{x,\mathbb{p}_{left}(z)}\models\forall m\exists n>m(x_n<\mathbb{p}_{left}(z)_n))\}.$$
Now on the face of things that doesn't look like a closed set, but you can rewrite it:
Using this rewriting, it's not hard to show that $\mathfrak{Q}$ is closed. (HINT: supposing $\langle x,z\rangle\not\in\mathfrak{Q}$, find some $j$ such that there is no pair of reals $x', z'$ extending $x_{\vert j}, z_{\vert j}$ respectively with $\langle x',z'\rangle\in\mathfrak{Q}$; this will say that $\mathfrak{Q}$'s complement is open.)
We now have to switch from topology back to computability, and generalize to arbitrary $\sigma$.
The computability/topology shift is pretty easy to undo, and goes the same for every $\sigma$: you just have to show that there is some computable relation $Q\subseteq(\omega^{<\omega})^2$ corresponding to our closed set $\mathfrak{Q}$, that is, some computable relation $Q$ such that for all $u,v$ we have $$\langle u,v\rangle\in\mathfrak{Q}\quad\iff\quad\forall n(Q(u_{\vert n}, v_{\vert n})).$$
Generalizing to arbitrary sentences $\sigma$ by contrast is meaningfully difficult, so I'd focus on that first. Think about coding up families of Skolem functions for an arbitrary $\sigma$ by individual reals. For example, suppose $\sigma$ is of the form $\forall q_1\exists q_2\forall q_3\exists q_4\tau$ with $\tau$ quantifier-free and think about $(i)$ what a family of Skolem functions for such a sentence is and how it must behave and $(ii)$ how to "bundle up" such a family of functions into a single real; this case has all the complexity of the general situation already.