First-order term
= 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>.