My question concerns a definition of an evaluation function with respect to some assignment between the variable set (which let us say is just $V = \{x_1,x_2,...\}$) of some specified first order language $L$ with equality and the domain of some $L$ structure with the same signature as $L$. Call it $\beta : V \rightarrow A$ where $A = dom(\Sigma)$, $\Sigma$ being the before mentioned $L$ structure.
Assume that $A$ is countably infinite, and suppose the set of $L$ terms, $Term(L)$ is built in the standard way from the symbols of $L$ and the set of well formed expressions, $Form(L)$ is also built in the standard way. Both these sets are countably infinite given $L$ is. We may extend $\beta : V \rightarrow A$ in a natural way to $\beta : Term(L) \rightarrow A$ and we will be referring to the extension as $\beta$ from here on. Note also that for any $a \in A$, $\beta(\frac{a}{x_i})$ is a map $Term(L) \rightarrow A$ agreeing with $\beta$ everywhere besides possibly $x_i$, which it sends to $a \in A$.
Define $eval_{\beta} : Form(L) \rightarrow \{0,1\}$ as follows:
(0) $eval_{\beta}(\bot) = 0$
(1) $eval_{\beta}( (t_1 = t_2))$, where $t_1,t_2 \in Term(L)$ is $1$ when $\beta(t_1) = \beta(t_2)$ and $0$ otherwise
(2) $eval_{\beta}( (\phi \square \psi) )$ is defined recursively in terms of $eval_{\beta}(\phi)$ and $eval_{\beta}(\psi)$ for any $\square$ a connective of propositional logic (if, and, or)
(3) $eval_{\beta}( (\neg \phi) ) = 1 - eval_{\beta}( \phi )$
(4) $eval_{\beta}( r_i ( t_1 , t_2 , ... , t_{m_i} ) ) = 1$ iff $ (\beta(t_1), ... \beta(t_{m_i})) \in str(r_i) \subset A^{m_i}$, otherwise it is $0$
(5) $eval_{\beta}(\forall x_i \phi) = 1 $ iff $eval_{\beta(\frac{a}{x_i})}(\phi) = 1 $ for all $a \in A$ and $0$ otherwise
(6) $eval_{\beta}(\exists x_i \phi) = 1$ iff $eval_{\beta(\frac{a}{x_i})}(\phi)= 1$ for some $a \in A$ and $0$ otherwise
I can see, by an inductive argument on the length of $\phi \in Form(L)$, that this associates to each $\phi$ some member of $\{0,1\}$ but I am somewhat troubled at looking at (5) and (6), because although I can 'imagine' that this can be computed for some expressions, in theory it would seem that since $A$ is countably infinite, some sort of machine that cannot appeal to 'meta theory' as we can, may never terminate when trying to compute $eval_{\beta}(\forall x_i \phi)$ for some $\phi$. To reconcile this I might make some statement like $P(n) = $ 'All well formed expressions of length $\leq n$ have an associated value in $\{0,1\}$ under $eval_{\beta(\frac{a}{x_i})}$ for any $a \in A$' , and I seem to be able to show that everything has an associated value like this, but I have to make some sort of 'philosophical leap of faith' when I try to do the inductive step for cases (5) or (6)..
My question now is how do we 'know' $eval_{\beta}$ 'exists', and in what sense are we talking when we say a function 'exists' in first order logic. It seems clear to me that (5) and (6) and even (4) are different to the other definitions, because they involve searching the set $A$.
The $eval$ function is not computable in general and need not be. Consider a first-order language that allows us to describe the behaviour of Turing machines and let $A(x)$ be a formula that expresses that $x$ is an accepting computation of machine $M$ on input $w$. Clearly the truth-value of $\exists x. A(x)$ is not computable.