\begin{definition}[Definition:Language of Predicate Logic/Formal Grammar/Term]
Part of specifying the language of predicate logic $\LL_1$ is the introduction of '''terms'''.
The '''terms''' of $\LL_1$ are identified by the following bottom-up grammar:
{{begin-axiom}}
{{axiom | n = \mathbf T \ \textrm {VAR}
        | t = Any variable of $\LL_1$ is a '''term''';
}}
{{axiom | n = \mathbf T \ \FF_n
        | t = Given an $n$-ary function symbol $f \in \FF_n$ and '''terms''' $\tau_1, \ldots, \tau_n$:
:$\map f {\tau_1, \ldots, \tau_n}$
is also a '''term'''.
}}
{{end-axiom}}
Colloquially, we can think of a '''term''' as an expression signifying an object.
\end{definition}