# Designation of a term in a sequence in Second-order Logic

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''?

-

See Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001), page 282 :

Predicate variables: For each positive integer $n$ we have the $n$-place predicate variables $X_1^n, X_2^n, ...$

Function variables: For each positive integer $n$, we have the $n$-place function variables $F_1^n, FX_2^n, ...$

The usual variables $v_1, v_2,...$ will now be called individual variables, to avoid confusion.

The terms are as before defined as the expressions that can be built up from the constant symbols and the individual variables by applying the function symbols (both the function parameters and the function variables).

Atomic formulas are again expressions $Pt_1...t_n$ where $t_1,..., t_n$ are terms and $P$ is an $n$-place predicate symbol (parameter or variable).

The definition of wff is augmented by new formula-building operations: If $\varphi$ is a wff, then so also are $\forall X_i^n \varphi$ and $\forall F_i^n \varphi$.

The concept of a variable occurring free in $\varphi$ is defined just as before.

A sentence is a wff a in which no variable (individual, predicate, or function) occurs free.

We must extend the definition of satisfaction in the natural way. Let $Var$ now be the set of all variables, individual, predicate, or function. Let $s$ be a function on $Var$ that assigns to each variable the suitable type of object. Thus $s(v_1)$ is a member of the universe, $s(X^n)$ is an $n$-ary relation on the universe, and $s(F^n)$ is an $n$-ary operation.

For a term $t$, $\overline s(t)$ is defined in the natural way. In particular, if $F$ is a function variable, then $\overline s(Ft_1 ... t_n)$ is the result of applying the function $s(F)$ to $(\overline s(t_1),..., \overline s(t_n))$.

Satisfaction of atomic formulas is also defined essentially as before.

For a predicate variable $X$,

$\mathcal M \vDash Xt_1 ... t_n[s]$ iff $\langle \overline s(t_1),..., \overline s(t_n) \rangle \in s(X)$.

The only new features in the definition of satisfaction arise from our new quantifiers.

$\mathcal M \vDash \forall X_i^n \varphi[s]$ iff for every $n$-ary relation $R$ on $|\mathcal M|$, we have $\mathcal M \vDash \varphi[s(X_i^n|R)]$.

$\mathcal M \vDash \forall F_i^n \varphi[s]$ iff for every function $f : |\mathcal M|^n \rightarrow |\mathcal M|$, we have $\mathcal M \vDash \varphi[s(F_i^n|f)]$.

-