To First-order Logic, like in Hodges "A Shorter Model Theory", we can designate a $L$-term $t$ in a structure $\mathfrak{A}$ considering a sequence $\bar{a}$ of elements of the domain $A$ of $\mathfrak{A}$, by complexity on the terms:
- if $t$ is a variable $x_i$, then $t^{\mathfrak{A}}[\bar{a}]$ is $a_i$;
- if $t$ is a constant symbol $c$ of $L$, then $t^{\mathfrak{A}}[\bar{a}]$ is a element $c^{\mathfrak{A}}$ of $A$;
- if $t$ is $ft_1...t_n$, where $f$ is a $n$-ary function symbol of $L$, then $t^{\mathfrak{A}}[\bar{a}]$ is $f^{\mathfrak{A}}t_1^{\mathfrak{A}}[\bar{a}]...t_n^{\mathfrak{A}}[\bar{a}]$ of $A$.
My question is: how can I extends this definition to evaluate Second-Order Terms too? That is, supose now that $L$ is a Second-Order Language; so, there is a function variable $F$ such that $Ft_1...t_n$ is a term $t$.
Then I suppose that $\bar{a}$ is a ''twested'' sequence of elements of $A$, a sequence of relations and function on $\mathfrak{A}$ and $t^{\mathfrak{A}}[\bar{a}]$ is $F^{\mathfrak{A}}[\bar{a}]t_1^{\mathfrak{A}}[\bar{a}]...t^{\mathfrak{A}}[\bar{a}]_n$, where $F^{\mathfrak{A}}[\bar{a}]$ is some $n$-function on $\mathfrak{A}$ or the ideas involved need be more ``sofisticated''?
