First-order term

A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.

A subterm of a first-order term is a term appearing at a node of its syntactic tree, including the whole term. Recursively, a variable or constant has only itself as a subterm; the subterms of $f(t_1,\dots ,t_n)$ are the full term together with every subterm of every $t_i$. A proper subterm excludes the full term.

For $t=f(g(x),g(x))$, the distinct subterms are $t$, $g(x)$ and $x$. The subterm $g(x)$ occurs twice, so a subterm value and a subterm occurrence are different notions. Replacing a particular occurrence requires its position in the tree, not only its text.

The subterm relation organizes structural induction, recursive evaluation and term rewriting. Every proper subterm has smaller syntactic size in the usual finite term grammar, so recursive definitions can terminate by descending through the tree. A substring of printed notation is not automatically a subterm: the tree structure determines which expressions are complete terms.

A first-order structure and an assignment determine the value of every term recursively: a variable has its assigned value, a constant has its interpreted value, and a compound function term is evaluated by applying the interpreted function to the recursively evaluated arguments. This operation supplies the input values for the satisfaction clauses of atomic formulas.

After replacing functions by graph predicates and constants by singleton predicates, $E_t(z)$ says that $z$ is the value of a term $t$. For a unary function graph $P$ and constant predicate $Q$, use $E_x(z)=(z=x)$, $E_c(z)=Q(z)$ and $E_{f(t)}(z)=\exists y(E_t(y)\wedge P(y,z))$. Fresh witnesses avoid variable capture. Totality and uniqueness axioms make each value formula have exactly one witness under every assignment.

A closed term contains no variables, so its value in a first-order structure does not depend on an assignment. In a language containing only relations and the constant zero, zero is the only closed term. A term-generated model has every element denoted by such a term.

A first-order term containing no variables. Constant symbols are ground terms; applying a function symbol to ground terms produces another ground term.